You must complete this assignment with a new partner. This must be your third distinct partner for the course. You and your partner must each understand the answers to both problems, so don't just do one each.

Written: Type Inference

Problem 1

Consider the program:
(+ 1 (first (cons true empty)))
This program has a type error.

Generate constraints for this program. Isolate the smallest set of these constraints that, solved together, identify the type error.

Feel free to label the sub-expressions above with superscripts for use when writing and solving constraints.

Problem 2

Consider the following typed expression:

{fun {f : B1 } : B2
  {fun {x : B3 } : B4
    {fun {y : B5 } : B6
      {cons x {f {f y}}}}}}

We have left the types unspecified (Bn) to be filled in by the type inference process. Derive type constraints from the above program. Then solve these constraints. From these solutions, fill in the values of the boxes. Be sure to show all the steps specified by the algorithms (i.e., writing the answer based on intuition or knowledge is insufficient). You should use type variables where necessary. To save writing, you can annotate each expression with an appropriate type variable, and present the rest of the algorithm in terms of these type variables alone (to avoid having to copy the corresponding expressions). If you do this, be sure to annotate every sub-expression with a type variable. Be sure the annotations are clearly readable!


Turn in your answer to each problem in a separate text or PDF file.