On this page:
1.17.1 Constraint Generation and Satisfaction
1.17.2 Type Inference
1.17.3 Application

1.17 Type Inference

Complete this assignment with Team Three.

1.17.1 Constraint Generation and Satisfaction

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.

1.17.2 Type Inference

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!

1.17.3 Application

In 850 words or less, describe if and how your knowledge of type inference will help you in your future programming practice. Good answers might discuss how this concept can be applied in interesting programming environments or how knowledge of its subtleties clarifies or improves existing practices, techniques, tools, etc.