School of Computer Science and Engineering, UNSW

CRICOS Provider No. 00098G

Advanced Functional Programming [COMP4132]

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


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.

Top Of Page

Site maintained by webmistress@cse.unsw.edu.au
Please read the UNSW Copyright & Disclaimer Statement