## Introductory C-H and Static Typing

Posted on August 15, 2008

We use logic every day. No, I don’t mean just us programmers; I mean all of us. Here is an observation about propositional logic:

I have three propositions P, Q and R.

It doesn’t matter what these three propositions actually are, it will always hold that, “if P then Q implies that if Q then R implies that if P then R”.

I’ve subverted that a little to try to make it read a little better, but perhaps look it at it a bit more formally:

``forall P Q R. (P → Q) → (Q → R) → (P → R)``

You might like to try it out on paper using some example propositions, such as:

• P = Today is Tuesday

• Q = I am going swimming

• R = I have hairy armpits

I won’t bastardise it with English again ;) However, I will give you a hint. Here is the truth table for → (logical implication):

``````A | B | A → B
0 | 0 | 1
0 | 1 | 1
1 | 0 | 0
1 | 1 | 1``````

Here is where it gets a little interesting. This same logical statement `forall P Q R. (P → Q) → (Q → R) → (P → R)` can also be expressed in most programming languages. Here it is in Java as the `z` method:

``````interface F<A, B> { B f(A a); }
static <P, Q, R> F<P, R> z(F<P, Q> f, F<Q, R> g) { ...``````

It gets more interesting; there is only one implementation of this function if we assume a terminating subset of the language (for Java, no `null` or throwing an exception). If you add in a side-effect such as writing to a file or the network, then you have perverted the function signature. Java allows us to do that, so we also have to assume a subset of the language that disallows this unfortunate anomaly. This notion of a type signature having only one implementation is called once inhabited.

Let’s write out the truth table for this. Notice the consistent `1` values in the final column. The statement is a tautology.

``````P | Q | R | P → R | Q → R | P → R | (Q → R) → P → R | (P → Q) → (Q → R) → P → R
0 | 0 | 0 | 1     | 1     | 1     | 1               | 1
0 | 0 | 1 | 1     | 1     | 1     | 1               | 1
0 | 1 | 0 | 1     | 0     | 1     | 1               | 1
0 | 1 | 1 | 1     | 1     | 1     | 1               | 1
1 | 0 | 0 | 0     | 1     | 0     | 0               | 1
1 | 0 | 1 | 0     | 1     | 1     | 1               | 1
1 | 1 | 0 | 1     | 0     | 0     | 1               | 1
1 | 1 | 1 | 1     | 1     | 1     | 1               | 1``````

Under the Curry-Howard Isomorphism, logical implication is represented by a function or in the example above using Java, by the `F` interface. The `z` function is called function composition. It takes the two give functions/propositions and composes them.

In Haskell, function composition is not called `z` as we called it with Java, but instead `(.)`. That’s a full-stop character in parentheses. We can ask for the type of `(.)` in the GHC interpreter:

``````Prelude> :type (.)
(.) :: (b -> c) -> (a -> b) -> a -> c``````

We might even call it by passing in function instances (similar to instances of the Java `F` interface):

``````Prelude> ((+1) . (*7)) 20
141

Prelude> (reverse . map Char.toUpper) "hello there"
"EREHT OLLEH"``````

You could do the same using Java, but it’s a little more verbose, so I’ll omit that ;)

Here is a simple quiz. If we suppose the same `F` interface earlier, how many implementations of this function are there:

``static <a> F<A, A> t() { ...``

``static <A, B> F<A, B> u() { ...``