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.