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

$\frac {\displaystyle\frac{}{A \vdash A}\texttt{x}} {A \rightarrow A} \textrm{$\rightarrow$-I}_{\texttt{x}}$

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

Prove A implies (A OR True)

$\frac {\displaystyle\frac {\displaystyle\frac {} {A \vdash A} \texttt{x} } {A \vdash A \lor \bot} \textrm{$\lor$-I}_{L} } {A \rightarrow (A \lor \bot)} \textrm{$\rightarrow$-I}_{\texttt{x}}$

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

Prove A implies (A AND True)

$\frac {\displaystyle\frac {\displaystyle\frac {} {A \vdash A} \texttt{x} \quad \displaystyle\frac {} {A \vdash \top} \textrm{$\top$-I} } {A \vdash A \land \top} \textrm{$\land$-I} } {A \rightarrow (A \land \top)} \textrm{$\rightarrow$-I}_{\texttt{x}}$

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

Prove A implies (A implies False) implies False

$\frac {\displaystyle\frac {\displaystyle\frac {\displaystyle\frac {} {A, (A \rightarrow \bot) \vdash A \rightarrow \bot} \texttt{f} \quad \displaystyle\frac {} {A, (A \rightarrow \bot) \vdash A} \texttt{x} } {A, (A \rightarrow \bot) \vdash \bot} \textrm{$\rightarrow$-E} } {A \vdash (A \rightarrow \bot) \rightarrow \bot} \textrm{$\rightarrow$-I}_{\texttt{f}} } {A \rightarrow (A \rightarrow \bot) \rightarrow \bot} \textrm{$\rightarrow$-I}_{\texttt{x}}$

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)