In this assignment you will implement type inference for the variant of Paret
type-checker. The only difference is that there are no longer type
annotations, since you will be inferring them.
Refer to the specification in
type-checker for the
precise behavior and typing rules of the language. The only difference in the
grammar is that
empty no longer take type annotations (and as a
empty is no longer wrapped in parentheses). Here is the complete
<expr> ::= <num> | <id> | true | false | (+ <expr> <expr>) | (num= <expr> <expr>) | (link <expr> <expr>) | (if <expr> <expr> <expr>) | (lam (<id>) <expr>) | (let ((<id> <expr>)) <expr>) | (<expr> <expr>) | (first <expr>) | (rest <expr>) | (is-empty <expr>) | empty
type-checker, we can now have types with type variables in them,
when the type of an expression is not fully constrained.
The type inference algorithm isn't particularly dependent on what kind of
types you have in your language, so it makes sense to pick a generic
representation that can easily be extended later. Thus the
definition has just two forms:
data Constructor: | c-num # No fields | c-bool # No fields | c-fun # Two fields: arg-type and return-type | c-list # One field: element-type end data Type: | t-var(name :: String) | t-con(con :: Constructor, fields :: List<Type>) end
We also defined helper functions
work like the constructors for the
type-checker, so you can more
easily port your test cases. For example,
t-fun(t-num, t-bool) evaluates to
t-con(c-fun, [list: t-con(c-num, empty), t-con(c-bool, empty)]). (Keep in
mind you can't pattern match with these functions using
cases since they are
not real constructors.)
The first step in type inference is to generate a set of constraints for all
the expressions in the program. In order to enumerate the relationships between
the types of the expressions, you will associate a unique type variable with
each expression. New type variables can be generated with
You will also need to associate identifiers with type variables. For this
purpose, you can use a
TEnv during constraint generation to map from
identifier names (e.g.
x) to type variables (made using
type TEnv = List<TypeCell> data TypeCell: | type-cell(id-name :: String, var-type :: TypeVar) end
A constraint equates a type variable with a type (possibly containing type variables associated with other expressions):
type TypeVar = String data Constraint: | constraint(ty-var :: TypeVar, ty :: Type) end
We are providing this type to you just for convenience. You can make your own and use that instead if you want a different representation. (For instance, if you want to follow the book's definitions more closely, you're free to do so, though it may make a couple cases trickier.)
Once you have generated a set of constraints, you need to unify them to get a coherent mapping from type variables to (possibly generic) types. The exact way you go about this is up to you.
Your job is to write a function
type-infer that takes in the source of a
Paret program and returns its inferred type.
You don't need to write an interpreter for the language. You also don't need to implement let polymorphism.
For fun, see if you can write a program that has the type
There are a few errors you can encounter during type inference:
data TypeInferenceError: | unification-err(type1 :: Type, type2 :: Type) | occurs-check-err(tvar :: String, ty :: Type) | unbound-id-err(name :: String) end
unification-errif two types can't unify.
occurs-check-errif a constraint fails the occurs check.
unbound-id-errif you encounter an unbound identifier during constraint generation.
You will write test cases for the
type-infer function. Your test file should
not test constraint generation or unification directly, since these functions
may be implementation specific. (It is, however, a good idea to test constraint
generation and unification for yourself in your code file.)
type-infer returns a
Type, so you will need to test types for
equality. This can be tricky due to type variables. We provided a function
normalize-type which takes a type, and renames all type variables to
be lowercase letters in alphabetical order that they appear in the type. So for
check: normalize-type(t-fun(t-var("foo"), t-fun(t-var("bar"), t-var("foo")))) is t-fun(t-var("a"), t-fun(t-var("b"), t-var("a"))) end
type-infer should call
normalize-type on its result. Then you can
either write tests that expect an exact type, or you can simply call normalize
your expected type to compare two types up to renaming. For example, both
tests are fine:
check: type-infer("empty") is t-list(t-var("a")) type-infer("empty") is normalize-type(t-list(t-var("foo"))) end
Because the order of constraint generation and unification is implementation specific, you shouldn't write test cases that have more than one error.
data Expr: | e-op(op :: Operator, left :: Expr, right :: Expr) | e-un-op(op :: UnaryOperator, expr :: Expr) | e-if(cond :: Expr, consq :: Expr, altern :: Expr) | e-let(name :: String, expr :: Expr, body :: Expr) | e-lam(param :: String, body :: Expr) | e-app(func :: Expr, arg :: Expr) | e-id(name :: String) | e-num(value :: Number) | e-bool(value :: Boolean) | e-empty() end data Operator: | op-plus | op-num-eq | op-link end data UnaryOperator: | op-first | op-rest | op-is-empty end
To get started, open the code stencil and test stencil. You can see the full types and all the helper functions we mentioned in the definitions.
First submit your test cases (named "type-inference-tests.arr") in Captain Teach.
Finally, submit a zip file containing both your test and code files for
type-inference. Call the files