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.

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.

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.

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.

## 1 comment:

That was a great explanation, thank you. (And Agda is fun.)

Post a Comment