Path induction: a GADT perspective

-- These types aren't actually imported to improve CI performance :(
-- It doesn't matter what they are, just that they exist
data Int : Set where
postulate
    String : Set
{-# BUILTIN STRING String #-}

data _≡_ {l} {A : Set l} : (a b : A) → Set l where
  instance refl : {x : A} → x ≡ x

An important concept in Martin-Löf Type Theory is the internal equality¹ type $\mathrm{Id}$. Like all inductive types, it comes with the typical rules used to introduce types:

• Formation rule
• Term introduction rule
• Term elimination rule
• Computation rule

There’s something quite peculiar about the elimination rule for $\mathrm{Id}$ in particular (commonly known as “path induction”, or just $J$). Let’s take a look at its definition, in Agda syntax:

J : {A : Set}
  → (C : (x y : A) → x ≡ y → Set)
  → (c : (x : A) → C x x refl)
  → (x y : A) → (p : x ≡ y) → C x y p
J C c x x refl = c x

There’s something odd about this: the $c$ case only defines what happens in the case of $C(x, x, \mathrm{refl})$, but the final $J$ definition extends to arbitrary $C(x, y, p)$. How can this be the case?

A good way to think about this is using generalized algebraic data types, or GADTs. A GADT is similar to a normal inductive data type, but it can be indexed by a type. This is similar to polymorphism on data types, but much more powerful. Consider the following non-generalized data type:

data List (A : Set) : Set where
  Nil : List A
  Cons : A → List A → List A

I could write functions with this, but either polymorphically (accepts A : Set as a parameter, with no knowledge of what the type is) or monomorphically (as a specific List Int or List Bool or something). What I couldn’t do would be something like this:

sum : (A : Set) → List A → A
sum Int Nil = 0
sum Int (Cons hd tl) = hd + (sum tl)
sum A Nil = {!   !}
sum A (Cons hd tl) = {!   !}

Once I’ve chosen to go polymorphic, there’s no option to know anything about the type, and I can only operate generally on it².

With GADTs, this changes. The key here is that different constructors of the data type can return different types of the same type family.

data Message : Set → Set₁ where
  S : String → Message String
  I : Int → Message Int
  F : {T : Set} → (f : String → T) → Message T

Note that in the definition, I’ve moved the parameter from the left side to an index on the right of the colon. This means I’m no longer committing to a fully polymorphic A, which is now allowed to be assigned anything freely. In particular, it’s able to take different values for different constructors.

This allows me to write functions that are polymorphic over all types, while still having the ability to refer to specific types.

extract : {A : Set} → Message A → A
extract (S s) = s
extract (I i) = i
extract (F f) = f "hello"

Note that the type signature of extract remains fully polymorphic, while each of the cases has full type information. This is sound because we know exactly what indexes Message could take, and the fact that there are no other ways to construct a Message means we won’t ever run into a case where we would be stuck on a case we don’t know how to handle.

In a sense, each of the pattern match “arms” is giving more information about the polymorphic return type. In the S case, it can only return Message String, and in the I case, it can only return Message Int. We can even have a polymorphic constructor case, as seen in the F constructor.

The same thing applies to the $\mathrm{Id}$ type, since $\mathrm{Id}$ is pretty much just a generalized and dependent data type. The singular constructor refl is only defined on the index Id A x x, but the type has a more general Id A x y. So the eliminator only needs to handle the case of an element of $A$ equal to itself, because that’s the “only” constructor for $\mathrm{Id}$ in the first place³.

Hopefully now the path induction type doesn’t seem as “magical” to you anymore!