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. (NatRR)  R  R
    nil ≡ λR. λc:NatRR. λn:R. n
   cons ≡ λh:Nat. λt:NatList. λR. λc:NatRR. λ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.