MiniML Type Inferencer

Due Tuesday, February 1, at the start of class

In this assignment, you will build a type inferencer for MiniML. Your type inferencer should handle the full MiniML language, including self-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/cse505/05wi/hw2. This is the same initial version of the interpreter as used in the previous assignment, with the following extensions:

• type.sml contain the Type datatype declaration which represents types computed by the type inferencer.  type_print.sml contains pretty-printing functions for Types.
• 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.
• We have added a file, typecheck.sml, which contains the main code for 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 defined in repl.sml has been extended to perform type inference on all declarations and expressions entered before evaluating them.
• We have added a file, unify.sml, that contains 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 type bindings and introducing explicit quantifiers for any generalizable type variables (generalizeTypeEnv). These operations are just what you need to implement the type inference operations in typecheck.sml.  The unification code does its work using two additional helper modules:
  • Type_Helpers, in type_helpers.sml, defines some helper functions for manipulating types.
  • Type_Subst, in type_subst.sml, defines a type TypeSubstitution, which is a mapping from type variables to types, and associated functionality.
  The unify function is incomplete; your job is to complete it.  You don't need to modify any of the rest of the unification functions, nor these modules, nor even know about Type_Helpers or Type_Subst.

You should make your own local copy of these files, copy over your changes from the first project to make the evaluator fully functional, and then provide implementations of the stubbed-out functions in typecheck.sml and unify.sml that are marked by ImplementMe exceptions.  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.

MiniML.x86-linux is a 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

How and what to turn in

Each student should complete the assignment independently.

You should develop some test cases, as a single file of MiniML code that can be directly fed into the evaluator, to exercise your solution and demonstrate that it works on the features that you had to implement.  I suggest developing this set of test cases early, perhaps before you begin implementing.  You can use the sample executable to see what behavior is expected on your test cases.

Turn in your assignment as follows:

• Email to KEUNWOO ONLY a tarball named firstname-lastname.tar.gz (where firstname and lastname are your last names, in all lowercase, words separated by a dash) of any modified files only, attached to an email with the exact subject line 505-proj2. The tarball must unpack to a directory named firstname-lastname/ whose contents contain any files you written.
• A hard copy, in class, on the due date, of any source files that you changed for your assignment, as well as the test cases and sample output. We suggest you use enscript -2r -DDuplex:true (see man enscript for details) to produce your code listings.

Code formatting guidelines

• No line of code shall be more than 80 characters long. (This makes the output of enscript -2r readable.)
• Every file shall have a banner comment at the top indicating your name and the name of the file.
• All indentation shall be proper, using only spaces (no tabs; these break when people set tab width display to a different number of spaces). In emacs, you can use M-x untabify to convert tabs to spaces (or use Google to find .emacs incantatons that will automatically untabify any file you edit before you save it)