Teaching G7400 F'11 Assignments Set 1 Set 2 Set 3 Set 4 Set 5 Set 6 Set 7 Set 8 Set 9

### Problem Set 7: Type Checking

 Due date: 11/04 @ at the beginning of class The goal of this problem set is to understand "simple" type systems: its design, its implementation, its (lack of) power. Your solution should import "5provided.rkt". Problem: The goal of this problem is to design and implement a typed variant of ISWIM. The problem consists of four tasks. In principle, tasks 2 through 4 are orthogonal to task 1. That is, you could solve the former tasks first, solve task 1, and then adapt the solutions of tasks 2 through 4. Task 1 Add the `(rec (f x) e)` form to the `ISWIM*` model of problem set 6, problem 1. The form abbreviates `(Y (lambda (f) (lambda (x) e)))`. The resulting language is called `ISWIM*r`. Test ISWIM*r with `sum`, the list processing function that adds up the numbers in a list. Also design the ISWIM*r function `value`, which applies all functions in a list to 0, collecting the results in a list. Finally, generalize the two functions into a `fold`-style function (called `map-reduce` in modern terminology). Task 2 Design `ISWIM*t`, a simply typed version of `ISWIM*r`. Start from `Simply Typed ISWIM` presented in chapter I.10 of the book. The design requires two steps. First, write down a modification of the `ISWIM*r` syntax so that it includes type declarations with all binding occurrences of variables. Explain in comments what the types mean. Second, it calls for type checking rules. Present these rules via a block comment, e.g., ``` #| Typing Rules Ty[x] = t ------------ [x] Ty |- x : t --- ------------- [b] Ty |- b : num |#``` Present each rule on a separate "line", in the above style, that is, with the antecedent(s) above the line, the conclusion below, and a name that refers to the syntactic construction that the rule checks. Your type system should be pragmatic. As you know from the text book, it will rule out some working programs. Make sure that your type system admits "interesting" programs such as `sum` and `value` from task 1. Demonstrate that the `fold`-style function from task 1 does not type-check. State a type soundness theorem for your design. Doing so clarifies the strength and weaknesses of your type system. Do not prove the theorem. Task 3 Implement the type system as a metafunction on `ISWIM*t`. The function should map expressions and type environments to their types. -- Optional: To ensure the correctness of your soundness theorem, you may wish to implement a type standard reduction machine for `ISWIM*r` and use `traces` to check type preservation across reduction sequences. In our experience, `redex-check` doesn't work too well for exploring the state space of this theorem, so you will need to come up with "experiments" on your own. Do not include this part in your submission. Task 4 Finally, define an evaluator for `ISWIM*t`. It accepts typed expressions, checks that they have the base type `num` in the empty type environment, and runs them on the abstract syntax machine for `ISWIM*r`. To do so, you need to design a function that strips type declarations from `ISWIM*t` expressions to obtain plain `ISWIM*r` expressions.

 last updated on Tue Nov 15 15:51:00 EST 2011 generated with Racket