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
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
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
Replying to
I'll watch the video when I get the chance! I'm planning to follow either QTT or GrTT in this - IIUC, QTT doesn't count usages in types towards term usages, and GrTT has a separate count for type usages.