ml-w-0.1.1: Minimal ML language to to demonstrate the W type infererence algorithm.

Portabilityportable (GHC, Hugs)
Safe HaskellSafe-Infered




This module implements the W algorithm for the small language we are using.

There is one minor annoyance: The Type datatype distinguishes between free type variables and quantified type variable, but the exposed functions of this module should produce types completely free of free type variables. This could be checked statically having a separate datatype without free type variables, but I compromised for clarity and brevity.

Partly inspired by the paper "Typing Haskell in Haskell" by Mark P. Jones,


Data types

type TyVar = IntSource

A type variable. We use integers for easy generation of new variables.

data Type Source

A data type to represent types. Note that the functions of this module should return Types without TyVars (we want the schemes to have no free variables).


TyVar TyVar

A type variable.

TyArr Type Type

The arrow type (A -> B)

TyGen Int

A quantified variable. We use a different constructor (separated from TyVar) so that there can be no clash between the two, and we immediately know what is what.


Eq Type 
Show Type 
Types Type 

data Scheme Source

A type scheme. The Int represents the number of quantified variables (must be >= 0).

Invariants: all the TyGen in the scheme must be < of the Int. If this is not the case the program crashes badly (see freshen).


Scheme Int Type 


data Assump Source

An assumption about the type of a (value) variable.


Id :>: Scheme 


Types Assump 

Type inference

data TypeError Source

What can go wrong when inferring the types.


UnificationFail Type Type

Unification failed (e.g. when trying to unify a quantified variable with an arrow type).

InfiniteType TyVar Type

The user is trying to construct an infinite type, e.g. 'a = a -> b'.

UnboundVariable Id

Unbound variable (value, not type variable).


Generic error, needed for the Error instances.


typeExpr :: [Assump] -> Expr -> Either TypeError SchemeSource

Types an Expr given a list of Assump. Returns either a TypeError if the algorithm failed or a Scheme if it succeeded.

typeProgram :: Program -> Either TypeError ([(Id, Scheme)], Scheme)Source

Types a list of declarations (a Program) returning the principal type for each declaration and the type of the final expression.

Pretty printing