Homework 5: Fun With System F

• Out: November 10
• Due: November 17, classtime

Programming with types

One objective of this assignment is to get across the idea that the types you are using can guide the programs you are writing. For this first part of this assignment, any System F term that has the correct type is a correct solution. For instance, any term with the type...

      ∀α. α -> α
    

... is the polymorphic identity function! The simplest example is this one:

      Λα. λx:α. x
    

QUESTION 1: Give a term for each of the following types:

• ∀α. ∀β. ∀γ. (α -> β -> γ) -> (β -> α -> &gamma) (Reversing the arguments to a function)
• ∀α. ∀β. ∀γ. (α -> β) -> (β -> γ) -> (α -> &gamma) (Composition of two functions)

QUESTION 2: Assuming that sums and products are introduced as in Lecture 10 are introduced into the language (as opposed to being defined in System F), give a term for each of the following types.

• ∀α. ∀β. ∀γ. (α -> γ) -> (β -> γ) -> (α + β -> γ)
• ∀α. ∀β. ∀γ. (α + β -> γ) -> (&alpha -> γ)
• ∀α. ∀β. ∀γ. (α × β -> γ) -> (α -> β -> γ) (Currying)
• ∀α. ∀β. ∀γ. (α -> β -> γ) -> (α × β -> γ) (Un-Currying)

QUESTION 3: Show the typing derivation for one of the previous six terms (your choice).

Lists

Lists of natural numbers can be described by this grammar: l ::= cons n l | nil. They can also be described by this System F type:

      list := ∀α. (nat -> α -> α) -> α -> α
    

      
      nil : list := Λα. λf:nat->α->α. λb:α. b
      cons : nat -> list -> list := λn:nat. λl:list. Λα. λf:nat->α->α. λb:α. f n (l[α] f b)
    

QUESTION 4: Give a System F term singleton with type nat -> list using nil and cons that creates a list with one element.

QUESTION 5: This is an inductive description of list appending (you should note the similarity to the description of plus in the appendix below).

• append l1 l2, the appending of two lists, is defined by induction on l1. If l1 = nil, then append l1 l2 = l2, and if l1 = cons n' ll' and append l1' l2 = l, then append l1 l2 = cons n' l.

Trees

Trees with natural numbers at the nodes can be described by this grammar: t ::= node n t t | leaf.

The term node 5 leaf (node 1 (node 2 leaf leaf) leaf) describes this tree:

      5
     / \
    *   1
       / \
      2   *
     / \
    *   *
    

       2
      / \
     *   1
        / \
       6   *
      / \
     /   \
    5     2
   / \   / \
  *   * 3   *
       / \
      *   *
    

      tree := ∀α. (nat -> α -> α -> α) -> α -> α
    

QUESTION 6: Give System F terms for node with type nat -> tree -> tree -> tree and leaf with type tree (analogous to the definitions of nil and cons above and the definitions of n0, n1, ... and succ below).

QUESTION 7: Give a System F term for flip with type tree -> tree that takes in a tree and returns its mirror image. An example of what flip should do is below.

       2                2
      / \              / \
     *   1            1   *
        / \          / \
       6   *        *   6
      / \     ----\    / \
     /   \    ----/   /   \
    5     2          2     5
   / \   / \        / \   / \
  *   * 3   *      *   3 *   *
       / \            / \
      *   *          *   *
    

QUESTION 8: Give a System F term infix with type tree -> list that flattens a tree into a list in infix order. For instance, the tree below applied to infix should be the list [2,5,6,3,2,1]. Hint: you may want to use the append function you wrote before.

       2
      / \
     *   1
        / \
       6   *
      / \
     /   \
    5     2
   / \   / \
  *   * 3   *
       / \
      *   *
    

Appendix: Natural Numbers

(Note: there are no questions in this section, and other than discussing a notion of inductive description, includes nothing that wasn't presented in lecture.) We have some examples of programming with System F from Lecture 16. For instance, we have a type of natural numbers...

      nat := ∀α. (α -> α) -> α -> α
    

...which we can use to define several natural numbers, as well as the general successor function.

      n0 : nat          := Λα. λf:α->α. λb:α. b
      n1 : nat          := Λα. λf:α->α. λb:α. f b
      n2 : nat          := Λα. λf:α->α. λb:α. f (f b)
      n3 : nat          := Λα. λf:α->α. λb:α. f (f (f b))
      succ : nat -> nat := λn:nat. Λα. λf:α->α. λb:α. f(n[α] f b)
    

We can then define addition, multiplication, and exponentiation, and the factorial function.

      plus :  nat -> nat -> nat := λn:nat. λm:nat. n[nat] (λp:nat. succ p) m
      times : nat -> nat -> nat := λn:nat. λm:nat. n[nat] (λp:nat. plus m p) n0
      pow :   nat -> nat -> nat := λn:nat. λm:nat. m[nat] (λp:nat. times n p) n1
    

Think about what this means in terms of an inductive description of addition, multiplication, and exponentiation:

• n+m is defined by induction on n. If n = 0 then n+m = m, and if n = n'+1 and n'+m = p, then n+m = p+1
• n×m is defined by induction on n. If n = 0, then n×m = 0, and if n = n'+1 and n'×m = p, then n×m = m+p.
• n^m is defined by induction on m (not n). If m = 0, then n^m = 1, and if m = m'+1 and n^m' = p, then n^m = n*p.