Homework # 6
due October 18
Please read Chapter 11 in your textbook.
Please do the following problems
- 11.5.1 (Explain your code!)
- 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.
- 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
,..., name
],
and case t of name
->
...
name
-> 
- 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
John Tang Boyland
2005-10-11