Assignment #5: Datastructures & Recursive Types

This assignment has 15 points. 

1.  [2 points] Write the function map in the typed lambda calculus with unit, booleans, sum types, pairs, recursive functions and recursive types. The function map should apply its function argument to every element of its list argument. If the argument list is the empty list, the result should be the empty list.  When writing the function, let list be an abbreviation for the following type:

mu a. unit + int * a

Let ulist be an abbreviation for the “unrolled” list type:  

unit + int * (mu a. unit + int * a)

The function map that you define should have this type:

map :  (int -> int) -> list -> list

Be sure to use all the appropriate coercions in your program (inl, inr, roll, unroll, etc.) Show that your function is well-typed by writing out the complete derivation for it using the typing rules for recursive types, sums and pairs covered in class.  You may use Bill's derivation server.

2.  [3 points]  Write a non-terminating program in a typed lambda calculus that only has unit, non-recursive functions (ie:  \x:t.e) and recursive types.  Hint: this is probably a pretty hard problem but the answer is quite short (one solution uses 2 functions and some roll/unroll coercions) Hint:  look back in your notes on the untyped lambda calculus.  We wrote some non-terminating programs in the untyped lambda calculus.  Is there a way to make one of those programs type check by adding some typing annotations and roll/unroll coercions?

3.  [10 points] Let language L1 be the typed lambda calculus with only unit, recursive functions and list types:

L1 types

t ::= unit | t1 -> t2 | t list

L1 expressions

e ::= x | () | fun f(x:t1):t2 = e | e1 e2 | nil[t] | e1 :: e2 | case e of (nil => e1 | x::y => e2)

Let L2 be the typed lambda calculus with unit, sum types, pairs, recursive functions and recursive types. 

L2 types (use meta-variable u)

u ::= unit | u1 -> u2 | u1 + u2 |  u1 * u2 |  mu a. u 

L2 expressions (use meta-variable d)

d ::= x | () | fun f(x:u1):u2 = d | d1 d2

       | inl[u] d | inr[u] d | case d of (inl x => d1 | inr y => d2)

       | (d1, d2) | let (x,y) = d1 in d2 | roll[u] e | unroll e

Your job is to rigorously define a well-typed translation from language L1 into language L2.  (We defined this translation relatively "informally" in class by example.) Here are the steps:

a) define the type translation formally using a judgement with the form

|- trans t = u

You will have one rule for each sort of L1 type t. eg:

---------------------

|- trans unit = unit

 

...

--------------------------

|- trans (t1 -> t2) = ....

 

...

------------------------

|- trans (t list) = ...

 

b) define the expression translation formally using a judgement with the form

 

|- trans e = d

 

You will have one rule for each sort of L1 expression e. eg:

 

---------------

|- trans x = x

 

---------------

|- trans () = ()

 

...

 

c) (I'm doing this step for you below) Define a typing context translation formally using a judgement with the form

 

|- trans GL1 = GL2

 

Here are the two rules you need:

 

--------------

|- trans . = .

 

|- trans G = G'      |- trans t = u

------------------------------------

|- trans (G,x:t) = (G',x:u)

 

d) Prove that your translation is type-preserving.  In other words, assuming that

G |-L1 e : t

is our notation for the typing judgement for language L1 and

G |-L2 d : u

is our notation for the typing judgement for language L2 prove that: 

If:

 

1.            G |-L1 e : t and

2.            |- trans G = G' and

3.            |- trans e = d and

4.            |- trans t = u

 

then:

 G' |-L2 d : u