CS 4536 Homework 5: Type Inference

Due: Thursday, March 2, 5pm via turnin (assignment name hwk5)
Collaboration Policy: Pairs Permitted

Note: You may opt to do the easier assignment on type checking instead, but that will cap your course grade at B.

The Assignment: Write a Type Inferencer

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>}
            | {rec {<id> <expr>} <expr>}
            | {fun {<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 arbitrary data (numbers, booleans, etc).

Note: The right hand side of the rec binding does not have to be a syntactic function. However, you may assume that the rec-bound identifier only appears under a {fun ...} in the right hand side of the binding. In other words, the following expressions are legal:

     {rec {f {fun {x} {f x}}}
       ...}

     {rec {f {with {y 4}
               {fun {x} {f y}}}}
       ...}
    

while the following are not legal:

     {rec {f f}
       ...}

     {rec {f {+ 1 f}}
       ...}
    

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. The general structure of constraints is defined in Part II. The specific instances of constraints for the language in this assignment is as follows:

• The constants are the base types: they should contain either the symbol 'number or 'boolean.
• The variables correspond to the expressions and identifiers whose types you wish to learn. Thus, they should contain either an expression (in abstract syntax), 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.

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 constant, which contains a symbol,
• 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.

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 an escape continuation that takes a string as input. If your unifier detects one of the following errors, it should invoke the escape continuation with your error message. Otherwise, it should produce a list of substitutions. The error cases to catch are

• 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 (ie, pointer equality, like Java's == comparison). Using eq?, for example, you can compare expressions in abstract syntax for identity. The constraint solving approach in Part III relies on identical variables being deemed equivalent by eq?.

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>)
            | <string>

  

where strings are used to represent type variables. 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.

What to Turn In

Submit a single Scheme file called infer.ss containing your code and test cases.

FAQ

Nothing yet ...