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.