MiniML Type Inferencer

Due Monday, October 28 at 2pm

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/cse505/02au/hw3. This is the same interpreter as used in the second assignment, with the following changes:

• 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. A few of the functions in Unify are left unimplemented, with comments in their place.
• The typecheck.sml file has been replaced with a partial implementation of the type inferencer. Some functions are provided, while for others only case headers and comments extracted from our sample solution are provided.

Your job is to provide implementations of the stubbed-out functions in unify and typecheck. You don't have to use any of our code if you don't want to, but given all the subtleties in performing type inference in the face of nested polymorphic functions and non-generalizable type variables, equality types, circular unification constraints, etc., you'll want to understand things carefully before you launch off in your own direction. Also, 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. Feel free to ask questions of Craig or Todd to clarify your understanding (Craig wrote the code this time).

As with the previous assignment, we have produced an executable of our sample solution, for Linux and Solaris systems:

• MiniML.x86-linux is a Linux binary of the sample solution for this homework -- a complete MiniML type inferencer. To use it, invoke the MiniML interpreter from a Linux machine as follows:

  sml @SMLload=MiniML.x86-linux

  This will start up the MiniML interpreter directly.
• Likewise, MiniML.sparc-solaris is a Sun Solaris binary of the sample solution.

How and what to turn in

The first person who finds a bona fide bug in the type inferencer sample solution wins a $1 prize.