Homework 6: Universal types

Due: 03/29 at 11:55pm
Points: 15 (each question 5 points)

Please prepare your solutions as a PDF file (scanned handwriting is okay, but no .doc or .docx, please). Submit your PDF file in Sakai.

1. Options

An option is a simple data structure that either holds a single value (some v) or nothing (none). In the untyped λ-calculus, we can define them as follows:

      some ≡ λx. λs. λn. s x
      none ≡ λs. λn. n
caseoption ≡ λo. λs. λn. o s n

caseoption takes two “callbacks”: if o contains a value v, it calls s v; but if o contains no value, it returns n. These definitions satisfy the following equations:

caseoption (some x) s n = s x
    caseoption none s n = n

Write a definition in pure System F for NatOption, the type of options of Nats, and for some and none. When you erase all the types from your definitions of none and some, they should match the untyped definitions above.
```
 NatOption ≡ _____

      none : NatOption
      none ≡ _____

      some : Nat → NatOption
      some ≡ _____
```
What should the type of caseoption be, and how would you define caseoption? (There’s more than one possible answer.) When you erase all the types from your definition it should match the untyped definition above.
```
      case : _____
      case ≡ _____
```

2. Parametricity

For each of the following types, write how many different (non-observationally equivalent, to be precise) terms there are that have that type. If your answer is nonzero but finite, list out the terms. If your answer is infinity, list out three of them. Hint: I put them in increasing order.

∀X. ∀Y. (X → X → Y) → Y
∀X. ∀Y. (X → X → Y) → X → Y
∀X. ∀Y. (X → X → Y) → X → X → Y
∀X. (X → X → X) → X → X

3. Lists

For this exercise, please use System F with built-in Nat and Bool (i.e., no fix).

In class, we defined lists of numbers as:

NatList ≡ ∀R. (Nat→R→R) → R → R
    nil ≡ λR. λc:Nat→R→R. λn:R. n
   cons ≡ λh:Nat. λt:NatList. λR. λc:Nat→R→R. λn:R. c h (t [R] c n)

    car ≡ λl:NatList. l [Nat]     (λh:Nat. λt:Nat.     h)    0
    cdr ≡ λl:NatList. l [NatList] (λh:Nat. λt:NatList. t)    nil
  isnil ≡ λl:NatList. l [Bool]    (λh:Nat. λt:Bool.    true) false

Write a definition for a function append : NatList → NatList → NatList that concatenates two lists together. Hint: Try writing it in OCaml first, using only fold_right.
Write a definition for a function reverse : NatList → NatList that reverses a list. Hint: Use append.