Homework # 6
due October 18

Reading

Please read Chapter 11 in your textbook.

Problems

Please do the following problems

1. 11.5.1 (Explain your code!)
2. Prove progress and preservation for the simply-typed lambda-calculus with pairs (see Figure 11-5). You may refer to the book's proof for sections of the proof that are identical to the corresponding proof for the simply-typed language calculus.
3. Enums can be seen as a varation on ``variants''. Write new typing rules for a type T written like [red,green,blue] with new syntax name as [ name$_1$,..., name$_n$], and case t of name$_1$ -> $t_1$ ... name$_n$ -> $t_n$
4. 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:
   • nats: a list of all natural numbers, in order starting from zero.
   • cons: to add a new element on the front of the list.
   • tail: to remove the front element from the list.
   • head: to return the first element of the list.
   • sumN: to add the first ``n'' elements of a list (this function takes two parameters).
   • filter: taking a predicate (function of type Nat -> Bool) and a list, return a list with all elements that are true for the predicate, in their original order.
   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, and turn in on paper the definition of the six functions listed above.

About this document