Still unclear how to integrate it with effects and regions though - one of my bigger worries. 😬
Conversation
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?
1
1
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
...and still end up with something useful in the mean time, while I wait. Hard to resist the temptation to jump in to try filling the holes myself! 😬
(one useful limiting factor is that I'm just not smart enough!)
1
Smarts are overrated honestly... as you can see there are a ton of fairly practical problems that nobody has gotten around to yet. More a function of time and having someone around who understands the literature (much more than I do) that you can ask questions.
2