The Fire Triangle

The fire triangle is a no-go result about Martin-Löf type theory. It says that a dependent type theory with

• unrestricted substitution (arguably part of what it means to be a type theory!)
• a universe (i.e. an MLTT), and
• dependent elimination for booleans, which
• is observably effectful (i.e. there is a term of Boolean type that is not observably equivalent to either true or false)
  is inconsistent.

This is a result due to Pédrot and Tabareau 2020. It is a generalisation of Herbelin's paradox.

Proof

Write \equiv 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 \textsf{true}, \text{false} : \mathbb{B} for the Boolean constants. Assume you have a term M : \mathbb{B} and a context C[-] such that

 C[\textsf{true}] \equiv \textsf{true}
 \qquad
 C[\textsf{false}] \equiv \textsf{true}
 \qquad
 C[t] \equiv \textsf{false}

Then by induction on booleans we have that C[b] = \textsf{true} for all b : \mathbb{B}. But then

\textsf{false} = C[t] = \textsf{true} : \mathbb{B}

Then by induction on Booleans we can construct an element of the empty type \textbf{0} (define P : \textsf{Bool} \to \mathcal{U} by P(\textsf{true}) = \textbf{1} and P(\textsf{false}) = \textbf{0}, and then transport \ast : \mathbf{1} along the equality above.)

When this paradox does not apply

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

• \textsf{call/cc}
• exceptions with handlers
• a store

It is not true for many simpler effects

• printing
• exceptions without handlers
• divergence

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.

Coping with the Fire Triangle

There are five ways to cope with the Fire Triangle:

1. No effects. This is just plain old type theory.
2. Effects, elimination, no substitution. This is the solution adopted by Lepigre 2016.
3. Effects, restricted elimination, substitution. This is Baclofen type theory Pédrot and Tabareau, LICS 2017.
4. Effects, elimination, substitution. This is then inconsistent as a type theory, but a perfectly well-defined programming language with dependent types, like e.g. Idris. See Pédrot and Tabareau, ETAPS 2018.
5. Dependent CBPV. This is technically the only correct solution. It was introduced in Pédrot and Tabareau 2020, and led to many developments in the early 2020s.

References

@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},
}