Homework # 12 (v. 1.1)
due Tuesday, November 29

Reading

Please read Chapter 23-25 in your textbook.

Problems

The programming questions should be done using the fullomega type checker, and you should copy in the church-numeral encoding of pairs and lists from test.f in the fullomega checker directory.

• Exercise 23.4.2$1 \over 2$ [$\star$ $\not\rightarrow$]: Write a recursive sum function with type:

  sum : (List Nat) $\to$ Nat

  You will find this helpful when testing problems below.
• Exercise 23.4.3$1 \over 2$ [** $\not\rightarrow$]: Write a recursive filter function with type

  filter : $\forall$X. (X$\to$Bool) $\to$ (List X) $\to$ List X

• Exercise 23.4.11$1 \over 2$ [$\star\star$ $\not\rightarrow$]: Write a non-recursive map using the Church encoding of lists. It should have the same type as on page 346.
• Exercise 23.5.1
  (Use the partial solution to help you write the proof.)
• Exercise 24.2.5$1 \over 2$ [ $\star\star\star$ $\not\rightarrow$]: The List type defined on page 351 exposes the internal representation. For example, we couldn't substitute an implementation using recursive types. The following definition fixes this problem

  
  OOList = lambda X.
             {Some R,{state:R, nil:R,
                      isnil: R->Bool,
                      cons: X->R->R,
                      head: R->X,
                      tail: R->R}};
  

  1. Write a term oonil that has type $\forall$X.OOList X; use the pre-existing List X definition.
  2. Write definitions of ooisnil, oocons, oohead, ootail so that they have the following types:

     ooisnil : $\forall$X. (OOList X) $\to$ Bool oocons : $\forall$X. X $\to$ (OOList X) $\to$ (OOList X) oohead : $\forall$X. (OOList X) $\to$ X ootail : $\forall$X. (OOList X) $\to$ (OOList X)

  3. Write oomap to use these primitives (you may assume fix). Test your program by running

     
     oohead[Bool] 
       (oomap[Int][Bool] iseven 
         (oocons[Nat] 1 (oocons[Nat] 2 (oonil[Nat]))))
     

Leave all your code in list.f, but also attach a printout to your proof of Exercise 23.5.1.

About this document