Summer school 2008:Exercises 3
From The Twelf Project
[edit] Polymorphic MinML (solution)
Add explicit polymorphism to MinML and prove type safety:
- Add a type
- Add terms Λα.e and e[τ], with the appropriate typing rules and dynamic semantics
- Extend the type safety proof to cover the new cases.
You can start from either encoding:
- The intrinsic encoding will be easier, because it takes full advantage of dependent types.
- The extrinsic encoding is closer to what people usually write on paper.
[edit] Monadic Effects (solution)
Add monadically encapsulated effects (i.e., an IO monad) to MinML, following PFPL Chapter 39.
If you're feeling ambitious, add the following specific effects (solution):
- getn ; x.m reads a natural number from an input buffer (i.e., stdin). x stands for the number in m.
- putn(e) ; m writes a natural number, the value of e to an output buffer (i.e., stdout).
These primitives are simpler than full mutable references because their dynamic semantics can be given as a labeled transition system with labels read n and write n---you do not need a store as part of the judgement form.
[edit] Determinacy of Evaluation
Prove that the dynamic semantics of MinML are deterministic (every expression steps to at most one other expression). Hint: you will need to use equality to state the theorem. See the discussion of uniqueness lemmas for a proof of determinacy for the simply-typed λ-calculus.
