The Curry-Howard isomorphism and the duality of → and ×

To people who are familiar with the Curry-Howard isomorphism, this post will probably be trivial and obvious. However, it just clicked for me, so I’m going to write about it. I had passively heard on #haskell that → and × (functions and tuples) were dual, so I played with types a bit, finding dual types, and it never really came together.

I’m not actually sure what I’m talking about here is exactly the CH isomorphism. I’ve been thinking about dependent types, and converting propositional formulae into that calculus. But if it’s not, it’s close.

Let’s use some sort of type bounded quantification in our logic. I was thinking about the following formula:

\forall n \in \mathbb{N} \, \exists p \in \mathbb{N} \, (p > n \wedge \text{Prime}(p) \wedge \text{Prime}(p+2))

The corresponding type is:

(n : \mathbb{N}) \rightarrow [ (p : \mathbb{N}) \times (p > n) \times \text{Prime}\, p \times \text{Prime} (p+2) ]

In other words, the proposition “for every natural, there is a twin prime greater than it” corresponds to the type “a function which takes a natural and returns a twin prime greater than it”. × corresponds to existentials, because it is the proof: it tells you which thing exists. The first element of the tuple is the thing, the second element is the proof that it has the desired property.

It’s interesting that ∀ corresponds to →, since logical implication also corresponds to →. The difference is that the former is a dependent arrow, the latter is an independent one. Beautifully in the same way ∃ corresponds to ×, and so does ∧.

Oh right, the duality. Knowing this, let’s take the above type and negate it to find its dual.

(n : \mathbb{N}) \times [ (p : \mathbb{N}) \rightarrow (\neg (p > n) + \neg\text{Prime}\,p + \neg\text{Prime}(p + 2)) ]

i didn’t bother expanding the encoding of not on the inner levels, because it doesn’t really make anything clearer.

The dual is a pair: a number n and a function which takes any number and returns one of three things: a proof that it is no greater than n, a proof that it is not prime, or a proof that the number two greater than it is not prime. Intuitively, n is a number above which there are no twin primes. If this pair exists, the twin prime conjecture is indeed false.

So yeah, that’s how → and × are dual. It’s pretty obvious now, actually, but it took a while to make sense.

About these ads

3 thoughts on “The Curry-Howard isomorphism and the duality of → and ×

  1. Hello,

    You are not quite right. What you are saying basically is that

    not (A -> B /\ C) = A /\ (B -> not C)

    (B is p : N and C is (p > n) /\ Prime p /\ Prime (p + 2))

    This is correct. First, however, you could have written the negation of a symmetric formula (B /\ C) as (C -> not B), or as (not B \/ not C), in addition to (B -> not C). The duality between /\ and -> should probably be based on something more unambiguous. Second, negation is not the only way to understand “dual”. For example, according to Wikipedia (Boolean algebra), the dual of (A /\ B) is (A \/ B). Also, for a formula (A -> B), its contrapositive (not B -> not A), which is equivalent to the original formula, is sometimes called “dual”.

    More importantly is that the relationship between negation and the transformations shown above, on the one hand, and Haskell and Curry-Howard isomorphism, on the other hand, is not nearly as direct. Speaking mathematically, the formula ((not (A -> B)) -> A /\ not B), as well as its corollary ((not (A -> B)) -> A), is true only in classical, not constructive logic. “Classical” means using the law of excluded middle (A \/ not A). If we have this law we can prove the second formula. Indeed, if A is true, then we are done. If A is false, then A -> B is true and we get a contradiction with the assumption.

    In constructive logic, on the other hand, proving a formula is the same as writing a program that has this formula as the type (this is Curry-Howard isomorphism). Now, (not A) is understood as (A -> _|_), where _|_ is falsehood. Can we construct a program with the type ((A -> B) -> _|_) -> A? No: if we have an operator that converts a function A -> B into some new type _|_ (or even empty type), then there is no way to construct a value of type A.

    Where were we? The duality of /\ and -> is a constructive thing; it does not require classical logic. Further, Curry-Howard isomorphism is normally considered with constructive logic, because, as shown above, there is no way to write a purely functional program with some types which are valid classical formulas.

    The duality of /\ and -> means simply this: A /\ B -> C is the same thing as A -> (B -> C) (viewed as types, this is of course currying). Why is this important, I don’t know very well, except that this is a special case of what is called “adjunction” in category theory, which has many examples throughout mathematics.

    Finally, I said that there is no *purely* functional program of type ((A -> B) -> _|_) -> A. Let’s consider a similar type ((A -> B) -> A) -> A, which is also derived only in classical logic. The type of the argument (A -> B) -> A is the type of a term t that accepts a *continuation*. Namely, if a place in the big program (whose final type is B)requires an subprogram of type A, t asks for the rest of the computation (A -> B) and returns A. Now, (callcc t) has type A, so it can be this subprogram. When we reach (callcc t), we take the rest of the computation (of type A -> B), plug it in t, and get A, which the current place in the program expects! Therefore, callcc has type ((A -> B) -> A) -> A.

    So, the types of purely functional programs are (via Curry-Howard isomorphism) formulas provable in constructive logic. And the types of programs with callcc are formulas provable in classical logic! (More precisely, classical minimal logic.) That is, callcc extends CHI from constructive to classical logic—isn’t this amazing?

  2. Terminology police: a category theorist would say they are “adjoint”, not dual. “Dual” typically means “what you get when you reverse all the arrows”, so to speak. The dual of products in categories are coproducts. As Evgeny said, the dual of (A /\ B) is (A \/ B), those two being respectively the product and the coproduct of A and B in a Boolean algebra regarded as a category.

    On the other hand, in any cartesian closed category, hom(A, _) is the right adjoint functor of _ × A. In the specific cases you’re concerned with, this gives you what you want, e.g.
    B × A → C is isomorphic to B → (A → C) in categories of types (called currying and uncurrying in functional programming)
    and
    B /\ A → C is equivalent to B → (A → C) in Boolean algebras (which I’ve heard called the “import-export law”).

    Of course, ∃ and ∀ can also be seen as left and right adjoints respectively in an appropriate categorical framework, and the mathematical reason that “∃ corresponds to ×” as you say is that they are both left adjoints and so interact well with each other.

    So I suggest the concept you’re looking for is “Adjoint functors”. Take a look at the Wikipedia article of that name.

  3. Michael: Thanks. I’ve been dipping my toes into category theory for a while, but have had great difficulty learning. This is another concrete example, which is very helpful. As useful as category theory seems to be, I notice a surprising lack of concrete examples in articles meant to teach it…

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s