Exercises in Curry-Howard correspondence
Formal logic seems to have lots of uses in computer science. One of these uses is to provide guidance about creating type systems for new programming languages with static types. Several modern programming languages (Standard ML, OCaml, Haskell, Scala) have put this guidance to good use. In these languages, the allowed types of values strictly follow a particular flavor of formal logic (the intuitionistic propositional logic). This guarantees, in particular, that all functions in our programs will always be called with arguments of correct types, and that no expression will cause a crash when evaluated because by mistake we attempted, say, to add the number "3" to a completely different sort of value for which addition is undefined.

In Haskell, functions can take arguments of unknown types. This is denoted by type signatures that contain type parameters, like this:

f ::  p -> (p->q) -> q

The code that implements the function f is this:

f = \c -> \g -> g c

Here f is a function that takes one argument (c) and returns a function that takes one argument (g) and returns g c. The type of c is unknown and is denoted by p. Since g is applied to c, the argument g must itself be a function that takes an argument of type p. The return type of g is also unknown and is denoted by q. It follows that the type of (f c g) is also q.

If we know that f has type p -> (p->q) -> q, can we write the code of f? We can. According to the Curry-Howard correspondence, this code will be a proof of the theorem p -> (p->q) -> q in the intuitionistic propositional logic, where p and q are arbitrary propositions and -> is the logical implication. The proof goes via modus ponens: if we are given p, and if we are given p->q, we can infer q. The modus ponens corresponds to applying the function g to the argument c. If we have a value c of type p and a function g of type p->q, we can apply g to c and obtain a value of type q.

(If you are lost: I am not explaining everything from the beginning here. This preamble is just to fix my notation. I can certainly explain every step here, but I haven't gotten enough time to write it all out. Feel free to ask.)

Now, I have written down the following exercises but have not yet had time to go through them.

Denote (p->u)->u by Θp for brevity. Here u is another unknown type. The type Θp is used for values of type p that are not available now but will be perhaps available later. If we have a value of type Θp, we can apply it to a function of type p->u, that is, a function that consumes a value of type p. This function will be called later, when the value of type p becomes available. In this way, we model a value that is "computed asynchronously".

The following types are given:

p -> (p->q) -> Θq
Θp -> (p->q) -> Θq
Θp -> Θ(p->q) -> Θq
Θp -> (p->q) -> q  -- obviously impossible
Θp -> (p->Θq) -> Θq
Θp -> Θ(p->Θq) -> Θq
Θp -> (p->Θq) -> Θq
Θp -> Θ(p->Θq) -> Θq

The question is, for each given type, to implement a function having that type, or to show that it is impossible. The answers will influence the design of a function library that has to do with managing asynchronous computations.

For example:

To implement a function of type a -> (b->a). Solution:

\x -> \y -> x

To implement a function of type (a -> b) -> a. Solution: impossible. (Proof omitted.)

To implement a function of type a->Θa. Solution:
\x -> \f -> f x, where f has the type a->u.

To implement a function of type Θa->a. Solution: impossible.

Note that in the language of logic, Θp is essentially a double negation of p, that is, ¬¬p. (Since the proposition u is arbitrary, it could be false. Negation of p is the same as p->false.) In classical logic, a double negation of p is equivalent to p. This is, however, not true in the intuitionistic logic: p does not follow from ¬¬p. And it is precisely the intuitionistic logic that correctly describes what is implementable in a programming language with static types. We can implement a function with type p->Θp but not Θp->p. Indeed, if a value of type p is not available now but will only be available later, we cannot satisfy the requirement that this value should be available now.

The impossibility of implementing Θp->p in a programming language is precisely the same as the lack of derivation for the formula ¬¬p->p. The intuitionistic propositional logic is decidable, i.e. we can have a rigorous proof that a derivation of ¬¬p->p is not possible. This proves that no matter how clever we try to be with our programming language, no function with this type could be implemented.