Language.HM.AlgorithmW

Typing contexts

type Context = Map Var Sigma

Typing contexts.

empty :: Context

empty is the empty typing context.

External interface

runW :: Context -> Term -> Either TypeError TyTerm

runW gamma term runs Algorithm W on term with an initial context gamma and returns an updated term with explicit type annotations.

inferW :: Context -> Term -> Either TypeError Tau

inferW gamma term runs Algorithm W on term with an initial context gamma and returns the polymorphic type of the whole term.

Misc

genInOrder :: Context -> Tau -> Sigma

genInOrder ctx t generalises a monomorphic type t to a polymorphic type in a context ctx. This variant of gen ensures that the order of quantifiers matches that in which type variables occur in t.