1 files changed, 80 insertions, 0 deletions
diff --git a/microposts/dependent-types.org b/microposts/dependent-types.org
new file mode 100644
index 0000000..5c4d70a
--- /dev/null
+++ b/microposts/dependent-types.org
@@ -0,0 +1,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]].