Intensional vs Extensional - Type Theory

If you've spent any time working with dependent types—whether in Coq, Agda, Lean, or even just reading about Martin-Löf's foundational work—you've likely encountered the distinction between intensional and extensional type theories. This isn't just academic hair-splitting; it directly impacts how we reason about equality, write proofs, and extract programs from our formal developments. Today, let's unpack this crucial distinction and explore why it matters for both theoretical understanding and practical implementation.

The Heart of the Matter: Two Faces of Equality

At its core, the difference between intensional and extensional type theory centers on how they treat equality. Let's cut through the jargon with a concrete example:

zero : ℕ → ℕ
zero n = 0

fermat : ℕ → ℕ
fermat n = if exists x y z < n, x³ + y³ ≡ z³ then 0 else 1

Are these functions equal? In extensional type theory, they likely are—after all, Fermat's Last Theorem tells us there are no solutions to xn+yn=znx^n + y^n = z^n for n>2n > 2, so fermat always returns 0. But intensionally, they're clearly different: their definitions compute in entirely distinct ways. This tension between how things are defined (intension) and what they ultimately compute to (extension) lies at the heart of our discussion.

Definitional vs. Propositional Equality

In type theory, we work with two fundamental equality judgments:

  1. Definitional equality (Γ ⊢ M ≡ N : T): Two terms are definitionally equal if they become identical after computation and unfolding definitions. This is built into the type checker itself.

  2. Propositional equality (Γ ⊢ p : Id_T(M, N)): A term witnessing that M and N are equal, treated as just another type within the theory.

Here's where the intensional/extensional split occurs:

  • In intensional type theory (ITT), these two notions remain distinct. Propositional equality is a type like any other, governed by its own introduction and elimination rules (most notably the J eliminator).

  • In extensional type theory (ETT), we add an equality reflection rule:

    Γ ⊢ p : Id_T(M, N)
    -------------------
      Γ ⊢ M ≡ N : T
    

This single rule collapses the boundary: if you can prove two things equal propositionally, they become judgmentally equal. Powerful? Absolutely. But with great expressiveness comes great computational cost...

The Category Theorist's Dilemma

Consider how category theorists use equality. They rarely want an equality on objects (categories are typically "large"), but still need to state when composition is defined—specifically, when the codomain of one morphism matches the domain of another. Careful analysis shows that this "matching" almost always refers to definitional equality. For instance, if G(X) = A × X, we expect to compose a morphism with codomain G(X) with a projection without proving equality first. This practical observation reveals why definitional equality remains "pervasive" in our formal systems—it's the computational backbone that makes everyday reasoning flow naturally.

Intensional Type Theory: Equality as a Rich Type

In intensional MLTT, identity types Id_A(x, y) are defined inductively with just one constructor: refl(x) : Id_A(x, x). This creates a rich structure where equality proofs themselves can be manipulated as computational objects.

The induction principle for identity types (often called the J rule) lets us derive reflexivity, symmetry, and transitivity—but notably not stronger properties like functional extensionality. To understand why, consider two functions f, g : A → B where ∀x, f(x) = g(x). In ITT, there's no built-in way to conclude f = g itself. Similarly, we cannot prove uniqueness of identity proofs (UIP)—the idea that any two proofs of Id_A(x,y) are themselves equal.

This isn't a bug but a feature! Hofmann and Streicher's seminal groupoid model showed that identity types in ITT can model arbitrary groupoids. Here's a quick explanation: a groupoid generalizes the concept of a group by allowing partial operations, where composition is only defined between compatible morphisms. In type-theoretic terms, this means different equality proofs between the same terms can themselves be "inequivalent"—imagine distinct paths between two points that cannot be continuously deformed into one another.

-- In ITT, we might have:
p, q : Id_Bool(true, true)
-- With no way to prove p = q

This higher-dimensional structure is precisely what makes ITT computationally well-behaved. Type checking remains decidable, normalization is guaranteed, and crucially—programs extracted from proofs compute efficiently. The trade-off? Sometimes we need to explicitly manage equality evidence where ETT would let computation work silently.

Extensional Type Theory

Extensional MLTT adds that critical equality reflection rule, making propositional equality computationally potent. This has profound consequences:

  1. Functional extensionality becomes trivial: If ∀x. f(x) = g(x), reflection immediately gives f ≡ g.

  2. UIP holds by construction: Any proof p : Id_A(x,y) reflects to x≡y, so p effectively becomes refl(x).

  3. Proof irrelevance follows: All proofs of the same proposition become definitionally equal.

But this elegance comes at a steep price. Equality reflection makes type checking undecidable because it requires solving arbitrary higher-order unification problems. Strong normalization—the property that all computations terminate—also fails. This is why no mainstream proof assistant (Coq, Agda, Lean) uses "pure" ETT by default.

Interestingly, some practical systems like F* implement derived extensionality by construction. F* achieves UIP not through reflection but by structuring its equality type so that any two proofs are definitionally Reflexivity. This clever engineering gives some extensional benefits while preserving decidable type checking—a pragmatic middle ground that demonstrates why this theoretical divide matters for real-world systems.

Homotopy: The Deeper Picture

You might have heard whispers about homotopy type theory entering this picture. Simply put, homotopy studies continuous deformations between paths—like how you might stretch a rubber band from one shape to another without breaking it. In homotopy type theory (HoTT), this becomes a powerful metaphor: terms are points, equality proofs are paths between points, and higher equality proofs represent homotopies (continuous deformations) between paths.

This perspective brings something: identity types in intensional type theory naturally encode higher-dimensional structures. Where ETT forces all types to behave like sets (with at most one path between points), ITT allows for richer "spaces" where multiple distinct paths (equality proofs) can exist. This is why univalence—a cornerstone of HoTT stating that equivalent types are equal—is inconsistent with UIP and can only thrive in an intensional setting.

Why This Divide Really Matters

This isn't just philosophy. Your choice between intensional and extensional approaches impacts real-world work:

  • Program extraction: ITT preserves computational meaning—extracted programs execute as written. In ETT, reflection can obscure operational behavior.

  • Proof complexity: ETT simplifies some proofs (funext, UIP come for free) but makes others impossible to automate due to undecidability.

  • Modeling: If you need to model higher-dimensional structures (like concurrency or quantum systems), ITT's richer equality is essential.

When Hofmann wrote his seminal thesis, he framed the challenge as reconciling "the two different ways that type theories deal with identity types." Modern developments in HoTT have reoriented this: rather than seeing the divide as a problem to reconcile, we now recognize it as revealing two fundamentally different paradigms with complementary strengths.

As recent conservativity results show, for judgments concerning h-sets (types where all equality proofs are equivalent), reasoning in extensional or propositional type theories becomes equivalent. This means that for many practical purposes—especially when formalizing classical mathematics—we can safely work in intensional type theory while retaining the semantic power of extensionality.

Practical Balance

So where does this leave us? Pure extensional type theory remains theoretically elegant but computationally impractical. Pure intensional type theory preserves nice computational properties but requires extra machinery for everyday mathematics. The modern consensus, as implemented in systems like Lean and Agda, is pragmatic:

  1. Base system: Intensional MLTT with a rich identity type
  2. Strategic axioms: Optional functional extensionality, univalence
  3. Internal translations: Techniques like the setoid interpretation (where types carry explicit equivalence relations) to recover extensional reasoning where needed

This layered approach gives us the best of both worlds: computational solidity when extracting programs, and expressive power when building mathematical libraries. Rather than choosing sides in the intensional-extensional divide, we learn to navigate between them—using each paradigm where it shines.


References