School of Computer Science and Engineering, UNSW  
CRICOS Provider No. 00098G 
Session 1, 2004
The following exercise should help you understand how type inference in the Hindley/Milner system works. For the definition of the rules for unification and type inference, please see the lecture notes. However, to simplify the exercise a bit, we ignore qualified types (i.e., type classes) for this exercise. We assume the following representation of variables, type constructors, types, type schemes, and expressions:
type Var = String type Con = String data Type = ConT Con  type constructor  VarT Var  type variables  AppT Type Type  type application data Scheme = Scheme [Var] Type  universally quantified type variables data Exp = VarE Var  term variables  AppE Exp Exp  application  LamE Var Exp  lambda abstraction  LetE Var Exp Exp  (nonrecursive) let binding
Given the following type for representing type substitutions
type Subst = Type > Type
define a function
(>) :: Var > Type > Subst
that lifts mappings from variables to types. Then, define type term unification as function with the following signature:
unify :: Type > Type > Maybe Subst
It should return Nothing
if unification fails;
otherwise, it should return the most general unifier
for the two type terms.
To define the actual type inference algorithm, use the inference rules from the lecture notes as a basis for implementing the following function:
type Gamma = [(Var, Scheme)] tyinf :: Gamma > Exp > (Subst, Type)
Given a type assignment and expression, tyinf
returns a type substitution and the principal type of the
expression. The type assignment maps term variables to types
schemes and must include mappings for all free variables
occuring in the expression.
