The accompanying file contains 14 types in need of a program that has this type. Conjure up these programs (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
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. The rule you wrote is about applications: if in the type environment G, if e0 has type t1 -> t2 and if in the same type environment, e1 has type t1, then in that type environment the application e0 e1 has type t2.
Alfrothul: Yup. And likewise, there 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 => e2, for some e2, look:
(a1 : A), (A : Type), . |- e2 : A -> A
FUN -------------------------------------------
(A : Type), . |- fun a1 => e2 : A -> A -> A
FORALL ----------------------------------------------------------------
. |- fun A : Type => fun a1 => 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 => e3, for some e3, look:
(a2 : A), (a1 : A), (A : Type), . |- e3 : A
FUN ------------------------------------------------
(a1 : A), (A : Type), . |- fun a2 => e3 : A -> A
FUN -----------------------------------------------------
(A : Type), . |- fun a1 => fun a2 => e3 : A -> A -> A
FORALL --------------------------------------------------------------------------
. |- fun A : Type => fun a1 => fun a2 => 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 => a2 : A -> A
FUN -----------------------------------------------------
(A : Type), . |- fun a1 => fun a2 => a2 : A -> A -> A
FORALL --------------------------------------------------------------------------
. |- fun A : Type => fun a1 => fun a2 => a2 : forall A : Type, A -> A -> A
Bong-sun: But we could just as well write another solution:
fun A : Type => fun a1 => fun a2 => 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, 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 child (naively): Does one really need to floss between all of one’s teeth?The family dentist (comfortingly): Only between the teeth one wants to keep.
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
Added Section Hint for the exercise about types [30 Jan 2024]
Added the precision about supplying all the arguments to all the applied lemmas when solving Exercise 05 [30 Jan 2024]
Completed [27 Jan 2024]
Updated [26 Jan 2024]
Created [25 Jan 2024]