|
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 -- (non-recursive) 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.
|