On this page:
9.1 Type Systems
9.2 Proof by Induction/  Type Safety
7.5.0.17

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

Extend your model from HW1 with a type system. This should include:
  • 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

Prove the following cases of progress and preservation:
  • 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:

Lemma 3 (Canonical Forms): If · ⊢ v : A then either
  • 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.