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

Portabilityportable (GHC, Hugs)
Stabilitystable
Maintainerf@mazzo.li
Safe HaskellSafe-Infered

Language.ML.TypeCheck

Contents

Description

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, http://web.cecs.pdx.edu/~mpj/thih/.

Synopsis

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).

Constructors

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.

Instances

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).

Constructors

Scheme Int Type 

Instances

data Assump Source

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

Constructors

Id :>: Scheme 

Instances

Types Assump 

Type inference

data TypeError Source

What can go wrong when inferring the types.

Constructors

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).

TypeError

Generic error, needed for the Error instances.

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

prettyType :: Type -> DocSource

prettyScheme :: Scheme -> DocSource