G7400 F'11
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".


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 2011generated with Racket