Homework 4: Polymorphism

Due: 11/11 at 11:59pm
Points: 30

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

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.
```
      caseoption : _____
      caseoption ≡ _____
```

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 System F, we can define 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)

[Added 2022-10-31:] This encoding (see Exercise 5.2.8 on p. 63 and its solution on p. 500) is known as the Böhm-Berarducci encoding of lists, and is analogous to Church numerals. We can use this encoding to define various functions on lists, for example:

length ≡ λl:NatList. l [Nat] (λh:Nat. λt:Nat. succ t) 0
allzero ≡ λl:NatList. l [Bool] (λh:Nat. λt:Bool. and (iszero h) t) true

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.