The Fire Triangle How to Mix Substitution, Dependent Elimination, and Effects
2020
There is a critical tension between substitution, dependent elimination and effects in type theory. In this paper, we crystallize this tension in the form of a no-go theorem that constitutes the fire triangle of type theory. To release this tension, we propose CBPV, an extension of call-by-push-value (CBPV)-a general calculus of effects-to dependent types. Then, by extending to CBPV the well-known decompositions of call-by-name and call-by-value into CBPV, we show why, in presence of effects, dependent elimination must be restricted in call-by-name, and substitution must be restricted in call-by-value. To justify CBPV and show that it is general enough to interpret many kinds of effects, we define various effectful syntactic translations from CBPV to Martin-Lof type theory: the reader, weaning and forcing translations.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
26
References
11
Citations
NaN
KQI