CS 4536 Homework 7: Type Inference

Due: Friday, February 29, 5pm via turnin (assignment name hwk7)
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

This assignment handles the following 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>}

This starter file contains all of the datatype definitions needed for this assignment.

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

Part I: Parse the language

Adapt your parser to handle this language.

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}}
       ...}

Part II: Generate Type Constraints

Write a function called generate-constraints which consumes a parsed expression of this language and returns a list of constraints.

Write a function called generate-constraints that accepts an expression and returns a list of constraints. You have the freedom to determine the precise contract of this function, including the representation of your constraints. However, we strongly recommend that you use the Type data structures as defined in the starter file as part of your representation of constraints.

During constraint generation, you will need to generate fresh identifiers. The function gensym returns a unique symbol each time it is applied. (gensym accepts an optional symbol as an argument; the result of (gensym 'x) is then a unique symbol that "looks like " 'x.)

Part III: Unification

Implement the unification algorithm from the lecture notes. Call the function unify. The unify function should accept a list of constraints and return a substitution. However, unify should signal an error if two types cannot be unified or if the occurs check fails. Use "unify" or "occurs" in your error messages for these, respectively. Again, the precise contract of unify is up to you to define.

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 IV: Inferring Types

To infer the type of a program, parse it, generate constraints, and unify the constraints to get a substitution. From the substitution, you can determine the type of the program.

In particular, define the function 

infer-type :: Expr -> Type

Part V: Testing and Jousting

infer-type returns a Type, so you will need to test types for equality. This can be tricky due to type variables, particularly if generate-constraints calls (gensym) to generate unique type variables. The support code defines a function ((type=? t1) t2) that returns true if t1 and t2 are equal, modulo renaming of variables. We've included a few examples that show you how to use type=? with test/pred and test/exn. You are free to modify this function as you see fit or to not use it at all.

You should write unit tests for all functions that you write. However, for the purpose of jousting, ensure that your test suites just use parse :: S-exp -> Expr and infer-type :: Expr -> Type. If you chose to use the type=? function we have provided, include it with your test suite.

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 Scheme file called infer.ss containing your code and a second file called tests.ss containing your test cases.

FAQ

Nothing yet ...