Homework # 7
due October 21

Reading

Please read Chapter 11 in your textbook.

Problems

Please do the following problems

  1. Enums can be seen as a variation on ``variants''. Write new typing rules (on paper, not SASyLF) for a type T written like [red,green,blue] with new syntax:

    \begin{displaymath}
\begin{array}{ccl}
t &\mathtt{::=}& \ldots \\
&\mid&
\tex...
...$\ -> $t_1$\ \vert \ldots\ \vert
$n_m$\ -> $t_m$}.
\end{array}\end{displaymath}

  2. Use fullsimple (using fix, NOT letrec) to implement infinite lists similarly to tables (see page 137). An infinite list will map a natural number to a natural number. In particular, we do not need options. Implement the following functions: In particular:
    sumN 3 (filter iseven (cons 7 nats))
    should evaluate to 6. Your code should run correctly; you will need to write definitions of plus (obvious) and iseven (in book) as well. Don't worry about efficiency.

    Leave your whole program in list.f in your AFS volume for Homework #6.

Proofs

Modify the proofs of type soundness of the simply-typed lambda calculus with ``unit'' types to add sums (See Figure 11-9). A skeleton file is available which gives the syntax (slightly modified from that in the textbook to avoid the keyword case and reserved operator |). You will need to define evaluation and type rules. You should follow the book as closely as possible.

About this document



John Tang Boyland 2008-10-14