The accompanying file contains 14 types in need of a program (i.e., an expression) that has this type. Conjure up these expressions (aiming for the simplest ones you can think of).
Hint: all these programs only need to have the shape (fun ... => e), where:
e ::= tt | x | fun (t : T) => e | e e | (e, e) | match e with p => e end
p ::= x | (p, p)
T ::= Type | X | unit | T * T | T -> T
where x and X are ordinary names, and using parentheses to disambiguate.
Anton: This exercise feels like magic.
Alfrothul: Ah, not really, we have the typing rules to guide us.
Anton: The typing rules to guide us?
Alfrothul: Well, yes, you know, for example, the APP-rule about applications:
G |- e0 : t1 -> t2 G |- e1 : t1
APP ----------------------------------
G |- e0 e1 : t2
Dana: Or the UNIT-rule about the unit value:
UNIT --------------
G |- tt : unit
Halcyon: Or the LOOKUP-FOUND-rule about finding names at the top of the environment:
LOOKUP-FOUND -------------------
(x : t), G |- x : t
Pablito: Or the KEEP-LOOKING-rule about peeling a binding off the type environment:
G |- x : t
KEEP-LOOKING -------------------- where x' != x
(x' : t), G |- x : t
Anton: OK – we write G |- e : t to mean that in a type environment G that maps identifiers to types, an expression e has type t.
Dana: Yes. The rule I wrote above is about the unit value: In the type environment G, the unit expression tt has type unit, unconditionally.
Alfrothul: Right. And the rule I wrote above is about applications and it is conditional: If in the type environment G, e0 has type t1 -> t2 and if in the same type environment G, e1 has type t1, then in that type environment G, the application e0 e1 has type t2.
Bong-sun: Likewise, here is the FUN-rule about function abstractions:
(x1 : t1), G |- e2 : t2
FUN : -----------------------------------
G |- fun (x1 : t1) => e2 : t1 -> t2
Anton: Right. And there is a similar FORALL-rule for universal quantification:
(x : Type), G |- e : t
FORALL : ---------------------------------------------
G |- fun (x : Type) => e : forall x : Type, t
Alfrothul: So you see, if we are asked to exhibit an expression of type, ah, let’s say forall A : Type, A -> A -> A, we just follow the structure of the type to construct a proof tree using these inference rules. We start at the bottom of the tree, naming the putative expression e0:
. |- e0 : forall A : Type, A -> A -> A
Dana: And then there is no choice but applying the FORALL-rule, which forces e0 to be fun A : Type => e1, for some e1, look:
(A : Type), . |- e1 : A -> A -> A
FORALL --------------------------------------------------------
. |- fun (A : Type) => e1 : forall A : Type, A -> A -> A
Alfrothul: Right. And then since the arrow associates to the right, A -> A -> A is really A -> (A -> A), and therefore again, we have no choice: we simply apply the FUN-rule, which forces e1 to be fun (a1 : A) => e2, for some e2, look:
(a1 : A), (A : Type), . |- e2 : A -> A
FUN -------------------------------------------------
(A : Type), . |- fun (a1 : A) => e2 : A -> A -> A
FORALL ------------------------------------------------------------------
. |- fun (A : Type) => fun (a1 : A) => e2 : forall A : Type, A -> A -> A
Anton: OK, OK. And now again there is no choice but applying the FUN-rule, which force e2 to be fun (a2 : A) => e3, for some e3, look:
(a2 : A), (a1 : A), (A : Type), . |- e3 : A
FUN ------------------------------------------------------
(a1 : A), (A : Type), . |- fun (a2 : A) => e3 : A -> A
FUN -----------------------------------------------------------------
(A : Type), . |- fun (a1 : A) => fun (a2 : A) => e3 : A -> A -> A
FORALL --------------------------------------------------------------------------------------
. |- fun A : Type => fun (a1 : A) => fun (a2 : A) => e3 : forall A : Type, A -> A -> A
Dana: And now we need to come up with something of type A in the stead of e3, and looking in the environment, we have the choice. For example, let’s use the LOOKUP-FOUND-rule:
LOOKUP-FOUND -------------------
(x : t), G |- x : t
Anton: I see:
LOOKUP-FOUND -------------------------------------------
(a2 : A), (a1 : A), (A : Type), . |- a2 : A
FUN ------------------------------------------------------
(a1 : A), (A : Type), . |- fun (a2 : A) => a2 : A -> A
FUN -----------------------------------------------------------------
(A : Type), . |- fun (a1 : A) => fun (a2 : A) => a2 : A -> A -> A
FORALL --------------------------------------------------------------------------------------
. |- fun A : Type => fun (a1 : A) => fun (a2 : A) => a2 : forall A : Type, A -> A -> A
Bong-sun: But we could just as well write another solution:
fun A : Type => fun (a1 : A) => fun (a2 : A) => a1 : forall A : Type, A -> A -> A
Pablito (naively): Do we really need to construct a proof tree to solve each exercise?
Dana (comfortingly): In our mind, yes, of course, but in practice we can shortcut the process. Here, since the type reads forall A : Type, A -> A -> A, we just know the shape of the expression: fun A : type => fun (a1 : A) => fun (a2 : A) => ?, picking a1 and a2 as fitting names on the way.
Pablito: OK. And now we need to replace ? with an expression of type A, and we have the choice here: Either a1 or a2 will do.
Dana: Yup. And anyway this proof tree is isomorphic to an abstract-syntax tree with type annotations. The typing rules are just a more convenient format to state these annotations – and to reason about them too.
Alfrothul: And in practice, one needs to type-check an expression with a type, i.e., to verify that a given expression has a given type, so the issue is just to construct the proof tree.
Bong-sun: In OCaml, one infer types, and so given an expression, the OCaml compiler both verifies whether it is both syntactically correct and type correct, and it comes back with a type-annotated abstract-syntax tree and with the type of the given expression if it is both syntactically correct and type correct. It’s quite beautiful.
Halcyon: But here we are asked the converse, right?
Dana: Yes. We are given a type, and we are asked to come up with an expression of that type.
Alfrothul: And that is done methodically, following the structure of the given type.
Mimer: Yup.
Anton: So, no magic?
Mimer: No magic.
The accompanying .v file contains 14 propositions in need of a proof. Conjure up these proofs (aiming for the simplest ones you can think of).
Hint: all these proofs only need to use the following tactics:
intro, intros
destruct (or alternatively, intros [... ...])
split (or alternatively, the conj constructor)
exact
apply
In the line of the epigraph about cursing and recursing, come up with a couple of snappy sentences with the pattern “To X is to reX.” and briefly analyze them. Do they make sense? Or not? Why? For example, does Mimer’s contribution make sense and if it does, why does it?
Changed tt into True in the exercise about propositions [07 Feb 2025]
Added the optional exercises [02 Feb 2025]
Added the mandatory exercises [31 Jan 2025]
Created [31 Jan 2025]