Curry-Howard Tutorial in Literate Haskell

CurryHoward.lhs

This is a tutorial on the Curry-Howard correspondence, or the correspondence
between logic and type theory, written by Keith Pinson, who is still a learner
on this subject. If you find an error, please let me know.

This is a Bird-style literate Haskell file. Everything is a comment by default.
Lines of actual code start with `>`. I recommend that you view it in an editor
that understands such things (e.g. Emacs with `haskell-mode`). References will
also be made to Scala, for programmers less familiar with Haskell.

We will need to turn on some language extensions. This is not an essay on good
Haskell, but on conceptual ideas.

> {-# LANGUAGE FlexibleInstances #-}

In our demonstrations of type-level false, we will need

> {-# LANGUAGE EmptyCase #-}

In our demonstrations of universal quantification or "for all", we will need

> {-# LANGUAGE RankNTypes #-}

In our demonstrates of existential quantification or "there exists", we will
need

> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE GADTs #-}
> module CurryHoward where

We'll be defining our own primitives in several cases for clarity of comparison;
 to avoid a naming conflict, we hide the default ones:

> import Prelude hiding (True, False, and, or)

Let our reasoning be fast and loose, for after all, it is morally correct.
 http://www.cse.chalmers.se/~nad/publications/danielsson-et-al-popl2006.pdf
i.e. we will ignore `undefined`, `unsafePerformIO`, &c: we will pretend we are
working in a strictly total, pure language. This type of reasoning will give us
strong guarantees; e.g. there will only be one correct definition of:

> identity :: a -> a

Can you see what it is? It is a trivial definition, but if you are not used to
reasoning this way, it may not be obvious (trivial is a mathematical concept,
obviousness a human one).

> identity x = x

(See "Theorems for Free" by Wadler et. al.)

Now let's get started with value-level logic. Note, our value level logic will
be classical, and our type-level logic is intuitionistic, so there will be a
bit of sloppiness in the comparison, but we will not belabor that here.

A straightforward way to begin is with the ideas of true and false. We'll use
short names both for convenience and to avoid collisions with Prelude.

> data B = F | T

At the type level we have, first of all, true:

> data True = True

This is isomorphic, or nominal typing aside equal to, the unit type `()` and its
value `()` from Prelude. Secondly we have false:

> data False

This is a type that cannot be constructed and is therefore uninhabited. It is
analogous to the empty set, zero, and false. It comes out of the box in
`Data.Void` as `Void`, but let's do everything ourselves here. Also, this is not
the full story, since in intuitionistic logic not all true (or false) propositions
are in all senses equal. We will deal with this later by introducing an idea of
truthiness and falsiness.

Now that we have true and false, we can proceed to conjunction, by way of truth
tables:

> and :: B -> B -> B
> and F F = F
> and F T = F
> and T F = F
> and T T = T

The analog in types is pairs, or (Cartesian) product types:

> type And a b = (a, b)
> andFalseFalse :: And False False -> False
> andFalseTrue  :: And False True  -> False
> andTrueFalse  :: And True  False -> False
> andTrueTrue   :: And True  True  -> True

However, one of the cool things about doing our logic at the type level (i.e.
about intuitionistic logic) is that we can't just make claims; we have to prove
them; i.e. we have to implement the functions we declared. The proofs are
deceptively simple, and bear some explaining. The first can be read, "You cannot
have a value of type `False`, but if you did, you could use it to prove
`False`." It could be as well implemented with the second as with the first:

> andFalseFalse (x, _) = x

The second proof amounts to the same thing, except for this time we couldn't
implement it with the second, since a value of type `True` exists:

> andFalseTrue  (x, _) = x

The third works off the same principle:

> andTrueFalse  (_, x) = x

This one is the easiest to understand, because you _can_ have a value of type
`True`, and therefore you just need to use one of the ones you've got in the
pair:

> andTrueTrue   (_, x) = x

In the last case we could have as easily used the first as the second.

For reasons that will become obvious as we go along, we choose to look at
implication, or "if/then", next. At the value level:

> ifThen :: B -> B -> B
> ifThen F F = T
> ifThen T F = F
> ifThen F T = T
> ifThen T T = T

At the type level this is analogous to functions:

> type IfThen a b = a -> b
> ifFalseThenFalse :: IfThen False False -> True
> ifTrueThenFalse  :: IfThen True  False -> False
> ifFalseThenTrue  :: IfThen False True  -> True
> ifTrueThenTrue   :: IfThen True  True  -> True

Our proofs are again deceptively simple. The first one can be read, "Sure, you
can construct a function `False -> False`!"

> ifFalseThenFalse _ = True

However, you cannot construct a function `True -> False`, and so we reason by
contradiction, i.e. "if you could, we could construct a contradiction with it".

> ifTrueThenFalse toFalse = toFalse True

If you understand those two, the last should make sense as well:

> ifFalseThenTrue _ = True
> ifTrueThenTrue _ = True

Now we can define negation, but this time instead of using a truth table, we
will use implication. It is true that from false follows false, but it is not
true that from true follows false; thus the following suffices as a definition
of negation at the value level:

> not :: B -> B
> not x = ifThen x F

The reason we picked this approach should become clear when you compare it to
the type-level encoding of negation:

> type Not a = IfThen a False

To satisfy those who would still like to see a truth table, we can demonstrate at
the type level that this approach works as you would expect:

> notFalse :: Not False -> True
> notTrue  :: Not True  -> False

And the proofs:

> notFalse _ = True
> notTrue toFalse = toFalse True

Now that we have seen both false and implication, we should look at the
type-level encoding of the logical principle of _ex falso quodlibet_ "out of
false, comes anything":

> exFalsoQuodlibet :: False -> a

Before we show the proof, recall that all predicates hold true for the empty
case. In other words, just as the "greater than" predicate holds for a list of
positive integers:

scala> List(1, 2, 3).forall(_ > 0)
res0: Boolean = true

It also holds true for an empty list of integers:

scala> (List(): List[Int]).forall(_ > 0)
res1: Boolean = true

Not only that, but even the constantly false predicative holds true for an empty
list (there are no counterexamples!):

scala> List() forall { _ => false }
res2: Boolean = true

Based on this observation, you should be prepared to grapple with an empty
pattern match (this is why we turned on the `EmptyCase` pragma):

> exFalsoQuodlibet x = case x of {}

When you pattern match on a type for which there are no values, you do not have
to match anything. Thus, you can attribute any output type to the case
expression.

We are finally ready to look at disjunction:

> or :: B -> B -> B
> or F F = F
> or T F = T
> or F T = T
> or T T = T

This corresponds to the binary sum type, isomorphic to `Either` from Prelude:

> data Or a b = Former a | Latter b
> orTrueFalse  :: Or True  False -> True
> orFalseTrue  :: Or False True  -> True
> orFalseFalse :: Or False False -> False
> orTrueTrue   :: Or True  True  -> True

The proofs are as follows:

> orTrueFalse (Former x) = x
> orTrueFalse (Latter x) = exFalsoQuodlibet x

> orFalseTrue (Former x) = exFalsoQuodlibet x
> orFalseTrue (Latter x) = x

> orFalseFalse (Former x) = x
> orFalseFalse (Latter x) = x

> orTrueTrue (Former x) = x
> orTrueTrue (Latter x) = x

Next let's formalize that strictly `True` is not the only true proposition, nor
`False` the only false one. In category-theoretic terms, `True` is the terminal
object (= type in the category we are dealing with, Hask), and `False` is the
initial object, and we are trying to grab the class of types that are
isomorphic to them. Because `True` is the terminal object, there are morphisms
(= functions in Hask) from all objects (types) to it:

> trueIsInitial :: IfThen a True
> trueIsInitial _ = True

Because `False` is the initial object, there are morphisms (functions) from it
to all objects (types):

> falseIsTerminal :: IfThen False a
> falseIsTerminal = exFalsoQuodlibet

Because an isomorphism requires a morphism in both directions, but for each of
these types we already have a morphism in one direction, our classes simply
capture the morphism in the other direction. Truthy first (w00t JavaScript):

> class Truthy a where
>   yep :: IfThen True a

As an example, consider that if false is analogous to 0 and true to 1, then
boolean is to 2 and therefore, `B` is truthy:

> instance Truthy B where
>   yep True = T

It would be equally valid to have used `F` to prove this.

Importantly, the propositions we've been proving are also truthy:

> instance Truthy (Or True True -> True) where
>  yep True = orTrueTrue

Falsiness is dual to truthiness:

> class Falsey a where
>   nope :: IfThen a False

As an example of this, we can define a second empty type:

> data Empty

> instance Falsey Empty where
>   nope x = case x of {}

"That's a boring example," you say. Wait a little bit and I'll show you a more
interesting example.

Universal quantification corresponds to parametric polymorphism, and explicit
`forall` annotations in Haskell help to see this, as illustrated by the K
combinator from SKI calculus:

> kcomb :: forall a b. a -> b -> a
> kcomb x _ = x

Let's have some fun with this by writing down the famous Aristotelian AAA
syllogism about Socrates. We'll make it vacuously true because we are focused on
the types, though it is rather satisfying that the theorem is proved via
function composition.

> data Man s
> data Mortal s
> data Socrates s

The fact that those types are uninhabited is not important for this example;
just see them as type-level predicates.

> all_men_are_mortal :: forall a. Man a -> Mortal a
> all_men_are_mortal x = case x of {}

> socrates_is_a_man :: forall a. Socrates a -> Man a
> socrates_is_a_man x = case x of {}

> socrates_is_mortal :: forall a. Socrates a -> Mortal a
> socrates_is_mortal = all_men_are_mortal . socrates_is_a_man

Finally we must consider existential quantification, i.e. statements like "some
balls are red", but in the Boolean sense, not the Aristotelian. A relatively
straightforward of this is generalized algebraic data types (GADTs). Again we
will use uninhabited types, not to place any emphasis on them being uninhabited,
but simply so that we don't get distracted with implementations not relevant to
type-level logic:

> data Date
> data Name
> data Color

A rather silly example of an algebraic data type, but usable as an effect in a
tagged initial system would be:

> data Question a where

The first constructor can be read as "there exists a question such that the
answer will be a date".

>   WhatIsYourBirthday :: Question Date

Similarly, the second constructor can be read "there exist a question such that
the answer will be a name."

>   WhatIsYourName :: Question Name

The third constructor can be read "there exist questions such that the answer
will be a color."

>   PickAColor :: [Color] -> Question Color

For those not as familiar with Haskell, this can also be easily encoded in
Scala:

sealed trait Question[A]
final case object WhatsYourBirthday extends Question[Date]
final case object WhatsYourName extends Question[Name]
final case class PickAColor(available: List[Date]) extends Question[Color]

Here is the critical observation. A type like `Maybe a` is inhabited no matter
what `a` you pick; even `Maybe Void` is inhabited by `Nothing`. Thus, `Maybe a`
 is a "for all" or universal claim. However, there are only three `a`s for which
`Question a` is inhabited. For example, the more interesting example of `Falsey`
that I promised earlier is:

> instance Falsey (Question String) where
>  nope x = case x of {}

This shows that `Question` is an existential type.

This is not the only kind of existential type we can represent in Haskell (or in
Scala). With type families (see also Rust and Swift), we can do something like
(silly example):

> class Animal a where
>   data Food a :: *
>   eat :: Food a -> IO ()

Which reads as "for all animals, there exists some type of food which they can
eat". Two example instances to show how this sort of typeclass works:

> data Cow = InTheField

> instance Animal Cow where
>   data Food Cow = Grass | Hay
>   eat Grass = putStrLn "Happy cow"
>   eat Hay = putStrLn "Also happy cow"

> data TRex = ArmsHahaMouthWow

> instance Animal TRex where
>   data Food TRex = You
>   eat You = putStrLn "'Chomp, chomp, chomp!' Sad."

I don't know if it's the T-Rex or the existential types, but this is getting
dangerous for the reader. Let's call it a day, but first, here is a summary,
using the more usual names for types rather than our home-grown ones, and
tacking on just a dusting of category theory (this has mostly been about the
Curry-Howard correspondence, but actually the correspondence is three-way):

|-------—————----|---------------|-----------------------|
| Curry          | Howard        | Lambek                |
|------—————-----|---------------|-----------------------|
| Logic          | Types         | Category Theory       |
|-—————----------|---------------|-----------------------|
| False ⊥        | Void          | Initial object        |
| True ⊤         | Unit          | Terminal object       |
| Not ¬          | a -> Void     | Morphism to initial   |
| And ∧          | (a, b)        | Product               |
| Or ∨           | Either a b    | Coproduct             |
| If/Then →      | a -> b        | Exponentials          |
| For All ∀      | forall a. a   | ...                   |
| There Exists ∃ | GADTS, &c     | ...                   |
|--------————--—-|---------------|-----------------------|