#+title: Curry-Howard correspondence and Dependent types
#+date: <2022-01-20>

What is Curry-Howard correspondence?

Roughly speaking, it says there is a one-one correspondence between
world of propositions (proofs) and world of types (programs).

A simple illustration:

For any two propositions P and Q, the proposition that P implying Q,
i.e. P -> Q, corresponds to: for any two types T and S, the functional
type T -> S.

Finding a proof of P -> Q corresponds to finding an element in T -> S.

In a more simplified setting, proving a proposition P corresponds to
finding an element of T.

In coq, one can write:

#+begin_src coq
Theorem p_implies_q : P -> Q.
#+end_src

Which looks exactly the same as, except the keywords =Theorem= and
=Definition=,

#+begin_src coq
Definition some_function : T -> S.
#+end_src

To show the pun is genuine, if you want, you can prove a definition
and define a theorem:

#+begin_src coq
Definition add_one : nat -> nat.
Proof.
  intro n.                      (* introduce the argument of the function to the context and call it n. *)
  apply succ.                   (* apply succ to the "goal" *)
  apply n.
Defined.

Definition imp_refl : forall P : Prop, P -> P := fun P p : P => p.
#+end_src

It may still feel rather forced, as the proof of the definition is way
less readable than a direct definition, and the definition of the
theorem is just plain silly (Logical Foundations has a more reasonable
example - the evenness of a number).

How about an actual example, where one cannot do without the
correspondence?  Well, look no further than dependent types!

Say you want to work with vectors, which are lists of a certain
length, which is encoded as a pair (the list, the length) with a
condition:

#+begin_src coq
Definition vector (X : Type) :=
  { '(xs, n) : list X * nat | length xs = n }.
#+end_src

This is called a dependent sum type, or sigma type, where the vertical
bar =|= serves the same role as in set theory, meaning "such that".

The full definition is a bit more involved which we will skip.

Now, how do you define a concat function that takes two vectors of
length m and n and returns a concatenated vector of length m + n?  You
will have to do two things in such a definition:

- *Define* the resulting pair.
- *Prove* the length of the resulting list is m + n.

Now there's no escaping the pun!

To learn more about this, check out [[https://softwarefoundations.cis.upenn.edu/lf-current/index.html][Logical Foundations]] and [[https://softwarefoundations.cis.upenn.edu/vfa-current/index.html][Verified
Functional Algorithms]].  More specifically, [[https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html][ProofObjects: The
Curry-Howard Correspondence]] and [[https://softwarefoundations.cis.upenn.edu/vfa-current/ADT.html#lab168][ADT: Abstract Data Types]].