The fire triangle is a no-go result about Martin-Löf type theory. It says that a dependent type theory with
true or false)This is a result due to [Pédrot and Tabareau 2020]. It is a generalisation of Herbelin's paradox.
Write for definitional equality. Assume intensional identity types denoted by (if we do not have them we can use Leibniz equality, which is always definable with a universe).
Write for the Boolean constants. Assume you have a term and a context such that
Then by induction on booleans we have that for all . But then
Then by induction on Booleans we can construct an element of the empty type (define by and , and then transport along the equality above.)
Buyer beware: this argument does not apply to all kinds effects!
The condition on being observably effectful means that effect can alter the value that is being returned. This is true for things like
It is not true for many simpler effects
Pedrot and Tabareau say that "In those cases, it is not possible to reason on effects in the type theory," but that seems a bit of a strong statement.
There are five ways to cope with the Fire Triangle:
Pédrot, Pierre-Marie, and Nicolas Tabareau. 2020. ‘The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects’. Proceedings of the ACM on Programming Languages 4 (POPL): 1–28. https://doi.org/10.1145/3371126.
@article{pedrot_2020,
title = {The fire triangle: how to mix substitution, dependent elimination, and effects},
volume = {4},
doi = {10.1145/3371126},
number = {POPL},
journal = {Proceedings of the ACM on Programming Languages},
author = {P\'{e}drot, Pierre-Marie and Tabareau, Nicolas},
year = {2020},
pages = {1--28},
}