# Natural Deduction, Curry Howard Correspondence and Parametricity

## Curry Howard Correspondence

The **CH correspondence** is the direct relationship between computer programs and mathematical proofs.

Programming | Logic |
---|---|

Types | Propositions |

Programs | Proofs |

Evaluation | Proof simplification |

In particular, logical connectives can be converted to Haskell types and back

Type | Logical Connective |
---|---|

Tuples | Conjunction (∧) |

Either | Disjunction (∨) |

Functions | Implication |

() | True |

Void | False |

We can hence prove a logical result by constructing a valid Haskell program:

```
// This proves that conjunction is commutative.
andCommutativity :: (A -> B) -> (B -> A)
andCommutativity p = (snd p, fst p)
```

```
// This proves that implication is transitive.
transitive :: (A -> B) -> (B -> C) -> (A -> C)
transitive f g x = g (f x)
```

### More Examples of Programs and Proofs with Natural Deduction

**Prove A implies A**

```
prop_id :: a -> a
prop_id = \x -> x
```

**Prove A implies (A OR True)**

```
prop_or_true :: a -> (Either a ())
prop_or_true a = Right ()
```

**Prove A implies (A AND True)**

```
prop_and_true :: a -> (a, ())
prop_and_true a = (a, ())
```

**Prove A implies (A implies False) implies False**

```
prop_double_neg_intro :: a -> (a -> Void) -> Void
prop_double_neg_intro a f = f a
```

## Type Isomorphism

Two types A and B are **isomorphic** if there exists a **bijection** between them. That is, for each value in A we can find a unique correponding value in B and vice versa.

### Examples of Type Isomorphism

```
data Switch1 = On Name Int
| Off Name
data Switch2 = (Name, Maybe Int)
```

## Polynmorphism and Parametricity

### Type Quantifiers

```
fst :: (a, b) -> a
-- or more verbosely:
fst :: forall a b. (a, b) -> a
```

This quantification over type variables is known as **parametric polymorphism**.

## Generality and Ordering

A function of type *Int -> Int* can be substituted with a polymorphic function of type *forall a -> a* by instantiating the type variable to *Int*. The reverse is not true however.

We hence have a notion of ordering. The type *A* is more general than *B* if type variables in *A* can be instantiated to give the type *B*.

## Constraining Implementations

Polymorphic type signatures constrain implementations as the implementations must not rely on the type variable being any specific type. The more general a type, the more restricted the implementations. For example:

```
id :: a -> a
id = \x -> x
```

is the only possible implementation of a function with type *a -> a*. We cannot assume the type is numeric and perform arithmetic. We cannot assume the type is boolean and do logical negation. And so on….

This has practical benefits, as the more general a type signature, the less possible mistakes that can be made when implementing the function.

## Principle of Parametricity

**Parametricity** states that the result of polymorphic functions cannot depend on **values** of an abstracted type.

More formally, let *g* be a polymorphic function on type *a* and have an abitrary function *f :: a -> a*. Then running *f* on all the *a* values in the input of *g* will give the same result as running *g* first, then *f* on all the *a* values of the output. Essentially **transforming inputs is equivalent to translating outputs**.

### Examples of Parametricity

```
foo :: forall a. [a] -> [a]
-- Guaranteed property for any f.
foo . (map f) == (map f) . foo
```

```
head :: forall a. [a] -> a
-- Guaranteed property for any f.
f (head ls) == head (map f ls)
```

```
(++) :: forall a. [a] -> [a] -> [a]
-- Guaranteed property for any f.
(map f xs) ++ (map f ys) == map f (xs ++ ys)
```

```
concat :: forall a. [[a]] -> [a]
-- Guaranteed property for any f.
concat ( map (map f) xs ) == map f (concat xs)
```