School of Computer Science and Engineering, UNSW CRICOS Provider No. 00098G

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.