The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects
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-Löf type theory: the reader, weaning and forcing translations.
Thu 23 Jan Times are displayed in time zone: Saskatchewan, Central America change
10:30 - 11:35: Types and EffectsResearch Papers at Ile de France II (IDF II) Chair(s): Dominique DevrieseVrije Universiteit Brussel | |||
10:30 - 10:51 Talk | Binders by Day, Labels by Night: Effect Instances via Lexically Scoped Handlers Research Papers Dariusz BiernackiUniversity of Wrocław, Maciej PirógUniversity of Wrocław, Piotr PolesiukUniversity of Wrocław, Filip SieczkowskiUniversity of Wrocław Link to publication DOI Media Attached | ||
10:51 - 11:13 Talk | The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects Research Papers Link to publication DOI Media Attached | ||
11:13 - 11:35 Talk | SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References Research Papers Guilhem JaberLS2N, Université de Nantes Link to publication DOI Media Attached |