I feel like it's really quite tricky because of how big terms usually get... without knowing the size in advance it's hard to put a whole term on the stack without copying. But if most are on the heap, you want fast GC, which usually means no destructors...
Conversation
Usually this is where linearity comes to the rescue, but (AFAIK) the terms you get during conversion generally won't be linear even in most existing linear dependent type theories. So this won't help too much.
1
I was planning on using 's Quantitative TT and Context Constrained Computation for this. Which has the advantage of allowing for linearity for all universes (I think?).
1
1
Still unclear how to integrate it with effects and regions though - one of my bigger worries. 😬
2
Integrating dependent type theory of any sort with effects in a sound way is an active research topic so I wouldn't be too concerned about its interactions with another active research topic yet :) . Making TT work nicely with effects seems mostly about restricting dependency.
1
Hehe, yeah. Interestingly I see stuff about 'fibration' popping up with both generative module functors and DT+effect work. Is this coincidence, or is this due to the connection between functors and DTs?
2
I wish I knew :( . That's beyond my knowledge level. Most of my understanding of this comes from a series of papers by Pierre Pédrot, who has some fairly accessible presentations on his website: pédrot.fr/publications.h. TT is CBN, effects are CBV, effectual TT is both somehow.
1
2
Given that generative vs. applicative functors are sort of similar in spirit to CBV vs. CBN, it wouldn't surprise me if a coherent treatment would require something close (if you want dependency and effects, you want applicative modules that "act" generative). But I have no clue.
1
1
Oh interesting. Thanks for lending me your intuition at any rate! First time I've heard the connection between generative vs. applicative functors and CBV vs. CBN...
1
I don't really know what I'm talking about :P .But I know generativity is treated as a sort of effect in some papers (1ML being the example I remember best--people.mpi-sws.org/~rossberg/1ml/) , and I also know that generally speaking to interpret effects correctly you need to think in CBV.
1
1
Yeah, that's what I was thinking of here:
Quote Tweet
Replying to @brendanzab @awesomeintheory and @bentnib
This stuff pops up because I've been also wanting to use the context constrained stuff to help mark the phase distinction, but this would then interact with generative modules. Maybe I could just ignore generative modules for now?
I know in Coq at least there are handwavey non-rigorous arguments that it could be bad to have generative modules, so that's probably a safe choice for the time being.
1
1
Kind of feel like I'm putting a huge amount of stress on existing research with the my practical demands, and it's exposing me to lots of fun gaps that still need to be filled up! Tricky thing is navigating stuff right so that I can be ready for when those are filled in…
2
1
Show replies