Equality is a (useless) transmutation machine

Even since I heard about the Curry-Howard isomorphism, I've been wondering: to which computational principle corresponds equality? and the axiom of choice? and all those other mathematical concepts which would probably be much more intuitive to me in computational form? Unfortunately, there is no Curry-Howard dictionary translating concepts from one domain to the other, much like a French-English dictionary would translate words from one language to the other.

A few of the correspondances are well-known. A proposition corresponds to a type, and the proofs of this proposition correspond to the inhabitants of this type. A theorem using the hypothesis A to prove proposition B corresponds to a function from type A to type B.

A number N corresponds to a type with exactly N inhabitants. The multiplication A × B corresponds to the tuple type (A, B). The addition A + B corresponds to the algebraic type Either A B, whose set of inhabitants is the disjoint union of the inhabitants of A and the inhabitants of B. The exponentiation B^A corresponds to the function type A → B. But what is equality?

In Agda, a programming language / theorem prover exploiting the Curry-Howard isomorphism, (propositional) equality is defined as follows.

agda data _≡_ {X} : X → X → Set where agda refl : (x : X) → x ≡ x

I must admit that this doesn't help much. This states that the only valid proof for x ≡ y is refl x, and even then, it only proves that x ≡ x. In other words, the only inhabitants of the type x ≡ y are values of the form refl x, which actually have type x ≡ x.

A more inspiring piece of Agda code is an example showing how to make use of an equality proof.

agda subst : {X : Set} agda → (P : X → Set) agda → (x y : X) agda → x ≡ y agda → P x agda → P y agda subst P .v .v (refl v) p = p

This code takes some arbitrary proposition P(x), say, "x is prime", a proof that x equals y, a proof that P(x) is true, and concludes that P(y) is also true. For example since 7 is prime and 3 + 4 equals 7, it follows that 3 + 4 is also prime. The code does this by pattern-matching on the proof that x ≡ y, obtaining refl v for some value v. Since refl v has both type v ≡ v and type x ≡ y, Agda concludes that x and y are both v. This changes the type of p from P x to P v and the type of the goal from P y to P v, making it possible for subst to return p.

The feat is more impressive if we use counter-factual equalities. If P(x) says that "x is pink", and you have a proof that Leonardo the Flamingo is pink, and also a counter-factual proof that Leonardo the flamingo is "equal" to Bob the Filthy Frog, then you can convince anyone that Bob is pink, thereby gaining him access to all those cool pink-only bars in town. An x ≡ y equality instance is like a machine you can use to transmute x's access cards into access cards for y.

For this reason, it is in the interest of all the cool pink kids that equality instances should be hard to forge.

And equality instance really are hard to forge. refl x has type x ≡ x, remember? The only transmuter you can build is the one which doesn't actually perform any transmutation. Hence my title: equality is a (useless) transmutation machine.

Oh! One last thing. The bird's-eye view of this post is that equality is a transmutation machine because by using subst, equality instances can be used to transmute things. Couldn't it be that using functions other than subst, equality instances could be used to do even more incredible (yet useless) things?

It turns out the answer is no: an equality instance is no stronger than a substitution machine. The proof of this is that from a substituting machine, we can obtain an equality instance, as follows.

agda unsubst : {X : Set} agda → (x y : X) agda → (subst : (P : X → Set) → P x → P y) agda → x ≡ y agda unsubst x y subst = subst (λ – → x ≡ –) (refl x)

We simply use our substitution machine to transmute the trivial equality instance refl x of type x ≡ x into an equality instance of type x ≡ y. Tada! Equality is (as strong as) a transmutation machine.

Samuel's Really Straightforward Proof of the Parametricity Result, extended (trivially) to dependent types.

[I'll eventually write a version which begins by explaining free theorems, but for now here's a proof for the cognoscenti]

Consider an agda expression, any typed agda expression whose type is a Set1. Here are two examples, including one using dependent types.

id : {a : Set}
   → a
   → a
id x = x

ff : {a : Set}
   → {s : a → a}
   → (F : a → Set)
   → (f : {x : a}
        → F x
        → F (s x))
   → {x : a}
   → (y : F x)
   → F (s (s x))
ff F f y = f (f y)

It is very straightforward to obtain a term, ff₁, which has the same type except that Set has been upgraded to a Set1. In fact, the expression ff already has the desired type, we just need to change its type annotation.

id₁ : {a : Set1}
    → a
    → a
id₁ x = x

ff₁ : {a : Set1}
    → {s : a → a}
    → (F : a → Set1)
    → (f : {x : a}
         → (F x)
         → (F (s x)))
    → {x : a}
    → (y : (F x))
    → (F (s (s x)))
ff₁ F f y = f (f y)

Now, let's make this change a bit more generic. Instead of fixing Set1, let's use an abstract target, Set#. Now, since agda doesn't know that Set# is a member of the Set hierarchy, the validity of the expression (x : a) does not follow from the fact that (a : Set#), as it would for (a : Set) or (a : Set1). For this reason, it is necessary to introduce the abstract type transformer (value# : Set# -> Set1), which inserts Set# into the type hierarchy.

It is very straightforward to obtain a term, ff#, which has the same type as ff except that Set has been upgraded to a Set# and value# has been inserted at the appropriate places. In fact, the expression ff already has the desired type, we again just need to change its type annotation.

id# : {a : Set#}
    → value# a
    → value# a
id# x = x

ff# : {a : Set#}
    → {s : value# a → value# a}
    → (F : value# a → Set#)
    → (f : {x : value# a}
         → value# (F x)
         → value# (F (s x)))
    → {x : value# a}
    → (y : value# (F x))
    → value# (F (s (s x)))
ff# F f y = f (f y)

And now the punchline is that ff# is precisely the proof of the free theorem for ff, using the following instantiations for Set# and result#.

record Set# : Set1 where
  field
    a  : Set
    a' : Set
    a~ : a → a' → Set

record value# (a# : Set#) : Set where
  open Set# a#
  field
    x  : a
    x' : a'
    x~ : a~ x x'

Even more free theorems can be obtained by using other instantiations. Note that in the usual formulation of the parametricity result, the type of the free theorems are usually given in a much longer, record-free form where each field is expanded into an individual parameter. It is tedious, but straightforward to convert between the two representations.

free-id' : {a : Set}
         → {a' : Set}
         → {a~ : a → a' → Set}
         → {x  : a }
         → {x' : a'}
         → a~ x x'
         → a~ (id x) (id x')
free-id' {a} {a'} {a~} {u} {u'} u~ = value#.x~ r# where
  a# : Set#
  a# = record {a = a; a' = a'; a~ = a~}

  u# : value# a#
  u# = record {x = u; x' = u'; x~ = u~}

  r# : value# a#
  r# = u#

free-ff' : {a : Set}
         → {a' : Set}
         → {a~ : a → a'
               → Set}
         → {s : a → a }
         → {s' : a' → a'}
         → {s~ : ∀ {x x'}
               → a~ x x'
               → a~ (s x) (s' x')}
         → {F : a → Set}
         → {F' : a' → Set}
         → (F~ : ∀ {x x'}
               → a~ x x'
               → F x → F' x'
               → Set)
         → {f : ∀ {x}
              → F x
              → F (s x)}
         → {f' : ∀ {x'}
               → F' x'
               → F' (s' x')}
         → (f~ : ∀ {x x' x~}
               → {y : F x }
               → {y' : F' x'}
               → F~ x~ y y'
               → F~ (s~ x~)
                    (f y) (f' y'))
         → ∀ {u u' u~}
         → {y : F u }
         → {y' : F' u'}
         → F~ u~ y y'
         → F~ (s~ (s~ u~))
              (ff F f y) (ff F' f' y')
free-ff' {a} {a'} {a~}
         {s} {s'} {s~}
         {F} {F'} F~
         {f} {f'} f~
         {u} {u'} {u~}
         {y} {y'} y~
         = value#.x~ r# where
  a# : Set#
  a# = record {a = a; a' = a'; a~ = a~}

  s# : value# a# → value# a#
  s# x# = let open value# x# in record
        { x = s x
        ; x' = s' x'
        ; x~ = s~ x~
        }

  F# : value# a# → Set#
  F# x# = let open value# x# in record
        { a = F x
        ; a' = F' x'
        ; a~ = F~ x~
        }

  f# : {x# : value# a#}
     → value# (F# x#)
     → value# (F# (s# x#))
  f# {x#} y# = let open value# y# in record
             { x = f x
             ; x' = f' x'
             ; x~ = f~ x~
             }

  u# : value# a#
  u# = record {x = u; x' = u'; x~ = u~}

  y# : value# (F# u#)
  y# = record {x = y; x' = y'; x~ = y~}

  r# : value# (F# (s# (s# u#)))
  r# = ff# F# f# y#