Advanced Functional Programming [COMP4132]

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.