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?).
Conversation
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?
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…
...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! 😬
1
1
(one useful limiting factor is that I'm just not smart enough!)
1
Show replies
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?
1
Show replies