MiniML Type Inferencer

Due Monday, October 27, at 6:30pm.

In this assignment, you will build a type inferencer for MiniML. Your type inferencer should handle the full MiniML language, including recursive functions, polymorphic functions, nested polymorphic functions, and equality types, except for the following restrictions:

• We have simplified the language by removing the overloaded <, <=, >=, and > operators on strings. These operators now only work on ints.
• You need not implement the value restriction. (It's unnecessary in the absence of refs and exceptions.)

You can start the assignment from the version of MiniML in /cse/courses/csep505/03au/hw2; it also is available as a zip file for download. This is the same interpreter as used in the previous assignment, with the following extensions:

• There is no eval.sml file included yet.  Until everyone has turned in their eval.sml file and the sample solution has been publicized, use your own eval.sml file from homework 1. Once our eval.sml file is available, you can either start using it, or continue to use your own eval.sml file.
• env.sml contains the Environment type and associated functionality, as before. However, it now also contains a type TypeEnvironment and associated functionality. Type environments map variables in the current scope to their types and will play an analogous role in typechecking that environments play in evaluation. Both environments are implemented simply as instances of an underlying ProtoEnvironment type.
• typecheck.sml contains the MiniML typechecker. It is currently quite incomplete; your job is to finish it. We have provided some helper functions for typechecking calls to unary and binary operators, and we've implemented type inference for patterns and function cases.  You need to build on these to implement type inference for declarations and expressions. The read-eval-print loop has been extended to perform type inference on all declarations and expressions entered before evaluating them.
• To allow representing polymorphic types, we've added a new case to the Type datatype in ast.sml: ForallType. This type has a list of type variables and then a type that can reference those type variables. E.g. the type 'a*'b -> 'b*'a would be represented by ForallType{typevars=["a","b"], typ=FunctionType{argType=TupleType[TypeVar "a", TypeVar "b"], resType=TupleType[TypeVar "b", TypeVar "a"]}}. ForallTypes are introduced internally by the typechecker to represent the types of polymorphic identifiers.
• We have added a file, unify.sml, that defines a module named Unify. Unify supports a bunch of operations to support unification-based type inference. Among other things, it allows fresh type variables to be created (fresh_type_var), it allows two types to be unified (unify), and it allows taking a type and replacing any type variables in it with the types (if any) that they've been constrained to be (resolve). It also supports generating a fresh instantiation of a possibly quantified type (instantiateType), and it supports taking a list of bindings and introducing explicit quantifiers for any polymorphic types (generalizeTypeEnv). These tools are just what you need to implement type inference.  Unify does its work using two additional helper modules:
  • Type_Quant, in type_quant.sml, defines some helper functions for manipulating explicitly quantified types.
  • Type_Subst, in type_subst.sml, defines a type TypeSubstitution, which is a mapping from type variables to types, and associated functionality.
  You don't need to modify any of these modules, nor even know about Type_Quant or Type_Subst.

Your job is to provide implementations of the stubbed-out functions in typecheck.sml. You should carefully read the unify.sml and typecheck.sml files to understand how the unification data structures work and how to use them in the typecheck functions.  Of course, feel free to ask questions, the earlier the better.

As with the previous assignment, we have produced executables of our sample solution for Linux, Solaris, and Windows systems.

• MiniML.x86-linux is a Linux binary of the sample solution for this homework -- a complete MiniML evaluator and type inferencer. You can play around with this version to get a feel for how your evaluator and type inferencer should behave and to compare with your solution. To use it, invoke SML from a Linux machine as follows:

  sml @SMLload=MiniML.x86-linux

  This will automatically start up the read-eval-print loop.
• There are similar sample solutions available for Solaris (MiniML.sparc-solaris) and Windows (MiniML.x86-win32).

How and what to turn in