9 Homework 2 – Practice with Type Systems
You should complete this homework on paper and submit as a PDF. You may use Redex to help you, but be sure to translate to on-paper notation.
9.1 Type Systems
A syntactic category for types.
A type for nat, bool, functions, and dictionaries.
A syntactic category for typing environments.
Typing rules.
9.2 Proof by Induction/Type Safety
lambda and application
bool and if
dictionary formation and projection
Note that the formal statements below are somewhat different from what we proved in class. The versions presented in class are the intuitive statements we got to from first principles. The versions below should be sufficient.
If you find you need any additional lemmas, you may state them and use them without proof (as long as they are not substantially similar to the lemma you are trying to prove).
Lemma 1 (Progress): If · ⊢ e : A then either e is an v, or e →+ e’.
That is, either a well-typed expression is a value, or it can take at least one step of reduction.
Lemma 2 (Preservation): If · ⊢ e : A and e →+ e’ then · ⊢ e’ : A.
That is, if a closed well-typed expression takes a step, then it is still of the same type.
The canonical forms lemma is a commonly used lemma that simplifies some reasoning:
A = Nat and v = z, or
A = Nat and v = (s n), or
A = A -> B’ and v = λx.e’, or
A = Bool and v = true, or
A = Bool and v = false
Prove type safety, using the previous lemmas. This will not be an inductive proof; despite the generic meta-variables, we can build derivations by appealing to the previous lemmas.
Theorem (Type Safety): If · ⊢ e then eval(e) = o.
Note that while we only care about type safety for top-level, observable results, we must strengthen the statements of progress and preservation to reason about arbitrary values. This is pretty much exclusively because of functions, which are values that contain a suspended computation, and are not observations.
You’ll also need a lemma about substitution for the function case of one of these lemmas.