Session 1, 2004
Exercises: Type Inference
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
Unification
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.
Inference
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.
