dreaming of a language with dependent records as modules (like in 1ML, but full spectrum dependent types), multistage stage programming, linearity, erasure, and effects+handlers that can be inlined or compiled to capability passing style (could be handy for custom allocators)
Conversation
how would you handle the multiple semantic interpretations of the dependent product in the presence of linearity?
1
Replying to
I dunno! I guess I was hoping that stuff like GrTT might help, but I've not looked too closely into the specifics. Would love to know though!
Replying to
Wait, could you expand on what you mean by 'multiple semantic interpretations of the dependent product'? At first I was reading it as 'dependent sum' - ie. 'dependent pair' - I always get those mixed up in my head!
1
neelk explains the problem with integrating linear and dependent types here. Basically, how do you handle dependent types consuming linear values? AFAIK, all existing solutions, GrTT included, simply avoid this problem by making the situation illegal.
1
Show replies