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
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!
1
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!
Replying to
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
By "multiple semantic interpretations", I basically meant do you allow it or disallow it, and if you allow it, how do you interpret it? Does the value get consumed by the type? Or do you ignore linearity at the type level?
1
Show replies