What is Curry-Howard Correspondence and how does the type system of Coq implement it.

## Curry-Howard Correspondence

Curry-Howard Correspondence draws relationship between the type theory (computer program) and the logics (proof). In short, 'a proof is a program, and the formula it proves is the type of the program'.

One can easily observe the similarity between formalizations in various fields. Take currying as an example:

$((T×U)→V)((T∧U)→V) ⇒(T→U→V)⇒(T→U→V) $The first line is the formalization of currying in type theory, where $×$ produces product / pair / tuple type, or `(T, U)`

, and $→$ denotes a function. The second line is the logic formalization, where $∧$ is the logical and operator and $→$ is the material implication operator. The correspondence is obvious.

The $→$ operation behaves like exponential. So a further and more unified abstraction could be:

$C_{BA}=C_{B}_{A}$Logic | Program |
---|---|

$∧$ (conjunction) | $×$ (product type, `tuple` s) |

$∨$ (disjunction) | $+$ (sum type, `enum` s) |

$→$ (implication) | $→$ (`function` s) |

$∀$ (universal qualification) | $Π$ (generalized product type) |

$∃$ (existential qualification) | $Σ$ (generalized sum type) |

$T$ (true) | (unit type) |

$F$ (false) | $⊥$ (bottom type) |

Generalized product and sum types sound a little bit odd. They are **dependent types**, which allows you to build types out of values. **Generalized product type**s are the type of functions that take *values* and return *types* that varies according to the value, while **generalized sum type**s are the type of tuples that the *type* of the second element varies according to the *value* of the first element (maybe you can treat the first element as an enum discriminant). With an extra order / generalization, the product types behave like functions (exponential-like), and the sum types behave like product ones.

## Coq's Type System

As a logic programming language, Coq (or Galina, to be exact) does incorporate logical propositions into its type system.

```
(value) -> (type) -> `Type`
↑
(proof) -> (prop) -> `Prop`
```

In the graph above, `()`

denotes a kind in general, and `->`

denotes 'has type of'. If something has type of `T`

, then it is annotated with `:`

and `T`

on the righthand side in Coq. `Type`

and `Prop`

are two specific types.

## Types and Values

This is a definition of a type, `nat`

.

```
Inductive nat : Type (*1*) :=
| O (*2*)
| S (*3*) (n : nat (*4*) ).
```

As a type, `nat`

has the type of `Type`

^{(1)}. This `nat`

type has two contructors, `O`

^{(2)} and `S`

^{(3)}. The `O`

constructor take no arguments, so a `O`

constructor *constructs* a value of type `nat`

directly, while the `S`

constructor takes a `nat`

as argument, but the return type does not depend on that argument, just a `nat`

. So you can annotate it with `:`

as follows:

```
Inductive nat : Type :=
| O : nat
| S (n : nat) : nat.
```

## Generics

A generic type, `list`

, can be definined in a similar fashion.

```
Inductive list (X: Type) (*1*) : Type :=
| nil : list X
| cons (head: X) (tail: list X) : list X.
```

The generic type parameter is promoted to the lefthand side of `:`

^{(1)}, which turns the `list`

identifier into a `Type -> Type`

function. This parameter `X`

is now shared between all constructors of `list`

. You have to construct a `list`

like:

`Compute (cons nat 1 (nil nat)). (* [1] *)`

## Propositions and Proofs

Then let's head over to the logics and proofs part. This is the definition of the `True`

proposition.

```
Inductive True : Prop (*1*) :=
| I : True (*2*).
```

Just like the `nat`

case, `True`

has the type of `Prop`

^{(1)}, the type of all propositions, and it has one constructor `I`

that constructs a `True`

proposition with no parameters^{(2)}. **Constructors of propositions build proofs**.

## Binding: Parameters and Indices

A more complex example is the `ev`

property, a `Prop`

dependent on a natural number.

```
Inductive ev : nat -> Prop (*1*) :=
| ev_0 : ev 0 (*2*)
| ev_SS (n : nat) (H : ev n (*3*)) : ev (S (S n)) (*4*).
```

Beware the type annotation of `ev`

. Instead of using `(n: nat) : Prop`

, which moves the natural number to the parameter side, the `nat`

appears on the right side (the **index side**), `nat -> Prop`

^{(1)}. And the `ev_0`

constructor returns the dependent type `ev 0`

^{(2)}, which is a narrowed type from `Prop`

.

What will happen if you use `(n: nat) : Prop`

? Then `n`

will be *bound*, instead of free. Check the following example:

```
Inductive ev (n: nat) : Prop :=
| ev_0 : ev ... (*1*)
(* ... *)
```

Now each `ev`

binds its own, *specific* `n`

provided within parameters, and that `n`

can be a value other than 0. So you cannot call `ev 0`

at mark `(*1*)`

, because this inner `ev`

call now only accepts this specific `n`

as argument, or you will get a type mismatch. In contrary, `: nat -> Prop`

introduces an arbitrary natural number as parameter, so with any specific `n0`

, `ev n0`

is compatible with this arbitrary `ev n`

. The semantics of a `nat`

parameter on `ev`

is weird: we will have an infinite list of incompatible properties, even_2, even_4 and so on.

Thus **constructors can further narrow the type definition index side**. According to the type system, `ev_0`

is a **proof**, just like `I`

, and `ev 0`

is a **proposition**, just like `True`

. The`ev_SS`

constructor has the type of `forall n: nat, ev n -> ev (S (S n))`

. It takes a natural number and *a proof that n is even*

^{(3)}and returns a proof stating the proposition that

`S (S n)`

is even^{(4)}.

We are not defining any concrete calculations (or **functions**) for the proof. Instead, we only describe the **relation**. Everything just happens in the type system. Notice that we are leveraging **dependent types** to narrow the type.

## Binding: Scope

In the `ev`

example, we move `nat`

from the parameter side to the index side to make it a **free** variable instead of a **bound** one. A parameter defined on the type itself^{(1)} has a scope that covers the whole `Inductive`

definition. In Coq, you can introduce bound variables in inner scopes^{(2)}. Take the definition of existence as an example:

```
Inductive ex (A : Type) (P : A -> Prop) : Prop :=
| ex_intro : forall x : A, P x -> ex A P.
```

In the `ex_intro`

constructor, we introduced a binded variable `x`

whose type is `A`

. Its scope is limited to the constructor, the exist proposition itself does not depend on the value of `x`

, but the proof does.

The following definition is equivalent. It moves `x`

from the index side to the parameter side. As the correspondence suggests, the universal qualification `forall (x: A), ...`

is the same thing as the generalized product type `(x: A) -> ...`

.

```
Inductive ex (A : Type) (P : A -> Prop) : Prop :=
| ex_intro (x: A) : P x -> ex A P.
```

The following theorem in first order logic corresponds with the Coq definition of `ex`

. $B$ is a predicate whence $x$ doesn't occur freely. In the case of `ex_intro`

, $B$ is `ex A P`

, while $A$ is `P x`

. The lefthand side is exactly our `ex_intro`

constructor.