Type Inference

Part I: Generating Type Constraints

Following the lecture notes, derive type constraints for this language:

   <expr> ::= <num>
            | true
            | false
            | {+ <expr> <expr>}
            | {- <expr> <expr>}
            | {* <expr> <expr>}
            | {iszero <expr>}
            | {bif <expr> <expr> <expr>}

            | <id>
            | {with {<id> <expr>} <expr>}
            | {fun <id> {<id>} <expr>}
            | {<expr> <expr>}

            | tempty
            | {tcons <expr> <expr>}
            | {tempty? <expr>}
            | {tfirst <expr>}
            | {trest <expr>}
   

The novelty of this language is that the list operations are now polymorphic; that is, you can create lists of numbers or booleans.

Also, function definitions are now recursive. For example, the following expression is legal:

     {with g {fun f {x} {f x}}
        {g 4}}
    

Adapt your parser to parse this language. Then, write a function called generate-constraints which consumes a parsed expression of this language and returns a list of constraints (of the type defined in Part II). The correspondence between type constraints and the terms in Part II is as follows:

• The variables correspond to the expressions and identifiers whose types you wish to learn. Thus, they should contain either an expression, or a symbol representing an identifier. You may assume all identifiers are bound exactly once; i.e., there are no unbound identifiers, and no name is ever bound more than once.
• The constructors are the type constructors. They should contain either:
  • the symbol '-> and a list of two arguments, or
  • the symbol 'listof and a list of one argument.
  • the symbol 'number and zero arguments.
  • the symbol 'boolean and zero arguments.

In some cases, you may need to a fresh identifier when defining constraints. The Scheme function gensym returns a unique identifier on every call.

Part II: Unification

Implement the unification algorithm from the lecture notes. Call the function unify. The algorithm should work for a generic term representation, in which a term is one of:

• a variable, which can contain any value, or
• a constructor of the form C(t₁, ..., t_n), where C is a symbol and the t_i are a list of sub-terms. (Constructors with no arguments can represent constants such as number and boolean.)

In addition, you will need data types for representing a constraint (a pair of terms) and substitution (a variable and a term). The unification algorithm will consume a list of constraints and produce a list of substitutions. As in the type checker assingment, your unification function must raise an appropriate message if one of the following errors is found:

• The unification of two terms is impossible.
• The occurs check fails.

Finally, when comparing variables for equality, use Scheme’s built-in eq? function. For symbols, it behaves exactly as symbol=?; for other values, it compares them for identity (like Java’s == comparison). We will rely on identical variables being deemed equivalent by equal? when solving the constraints generated in the following section.

Part III: Inferring Types

To infer the type of a program, parse it, generate constraints, and unify the constraints. The result will be a list of substitutions; by looking up the subsitution for the entire expression, you can access its type.

To implement this, your code needs to define a function, infer-type, which consumes a concrete representation of the program (as given above), and produces either an error string or a representation of the inferred type. Represent types concretely as:

   <type> ::= number
            | boolean
            | (listof <type>)
            | (<type> -> <type>)
            | <symbol>
  

where symbols are used to represent type variables. (The Scheme procedure symbol->string may be helpful.) For example, the type of length would be:

   ((listof a) -> number)
  

Extra Credit

For a very small amount of extra credit, write a program in this language for which your algorithm infers the type (“a” -> “b”). You shouldn’t attempt this problem until you’ve fully completed the assignment.

What Not To Do

You do not need to implement an interpreter for this language.

You do not need to implement let-based polymorphism.