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.
Conversation
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
My best advice for future-proofing would be to produce the weakest (proof theoretically) theory you can, even if it's more complicated. The less you can prove, the less likely it is that your cool core language feature winds up incompatible with some other cool language feature.
1
1
"weakest (proof theoretically) theory you can, even if it's more complicated" - could elaborate on this?
Hm, easy example would be that Cedille turns out to be able to handle induction and tons of other stuff with a very small extension to CoC. But it has non-strictly positive inductives, and other things (e.g. heterogenous equality) that are incompatible with some common axioms.
1
1
For that matter, as I alluded to above, Coq's dependent elimination is too strong in the general case (with effects) and the current version plays so badly with coinduction that it is actually being retroactively removed.
1
1
Show replies