Exciting abstract by Andras Korvacs on staged compilation using two level type theory! This is cool because it could give us predictable control over monomorphisation, inlining, and compile time code generation for dependently typed programs:
Conversation
This is another case where dependent types seem to subsume a whole bunch of different things I've seen in other programming languages (like Rust's generics, constant parameters, const fns, memory layout stuff, and possibly even macros), but in a more general, flexible way.
Replying to
Of course I think people have noticed this for many years - but the devil has been in the details! Getting all of this stuff to work together nicely seems to be an mighty challenging thing when you have something as rich as full-spectrum dependent types.
1
3
One thing I'd love to see is how this interacts with other constraints you might want on variables - stuff like linearity, erasure, and uniqueness. Also effects as well. The tricky thing about systems programming is that those are important to think about as well!