Conversation

Brendan Zabarauskas
@brendanzab
Replying to
@brendanzab
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.
1
5
Brendan Zabarauskas
@brendanzab
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
Brendan Zabarauskas
@brendanzab
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!
Soares Chen
@soareschen
Replying to
@brendanzab
I have been trying to wrap my head around whether it is possible to compile/monomorphise all other type theories into simply typed lambda calculus. So far I can't find any way to monomorphise constructs like existential types and infinite dependent sums.
1
1
András Kovács
@andrasKovacs6
Not possible. If we only look at (Nat -> Nat) functions, some are definable in MLTT and not definable in STT, so there is no translation from MLTT to STT which preserves standard semantics of (Nat -> Nat) functions.
4