libcspm-0.2.1: A library providing a parser, type checker and evaluator for CSPM.

CSPM.TypeChecker.Unification

Synopsis

Documentation

generaliseGroup :: [Name] -> [TypeCheckMonad [(Name, Type)]] -> TypeCheckMonad [[(Name, TypeScheme)]]Source

Generalise the types of the declarations. The parameter names gives the names that were bound by all the declarations that we are interested in. This is done because we convert a type T into forall vs T where vs = fvts (T) - fvts(Env) where Env does not contain the function whose type we are generalizing (this is because when we type a declaration we are really typing a lambda function).

instantiate :: TypeScheme -> TypeCheckMonad TypeSource

Instantiates the typescheme with some fresh type variables.

unify :: Type -> Type -> TypeCheckMonad TypeSource

The main type unification algorithm. This adds values to the unification stack in order to ensure error messages are helpful.

unifyAll :: [Type] -> TypeCheckMonad TypeSource

Unifys all types to a single type. The first type is used as the expected Type in error messages.

evaluateDots :: Type -> TypeCheckMonad TypeSource

Takes a type and attempts to simplify all TDots inside by combining TDotable t1 t2 and arguments.

typeToDotList :: Type -> TypeCheckMonad [Type]Source

Takes a type and converts TDot t1 t2 to [t1, t2].