# 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``````
1. 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 ≡ _____``````
2. 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.

1. `∀X. ∀Y. (X → X → Y) → Y`
2. `∀X. ∀Y. (X → X → Y) → X → Y`
3. `∀X. ∀Y. (X → X → Y) → X → X → Y`
4. `∀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``````
1. 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`.

2. Write a definition for a function `reverse : NatList → NatList` that reverses a list. Hint: Use `append`.