1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
#+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]].
|
