|Portability||portable (GHC, Hugs)|
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/.
- type TyVar = Int
- data Type
- data Scheme = Scheme Int Type
- data Assump = Id :>: Scheme
- data TypeError
- typeExpr :: [Assump] -> Expr -> Either TypeError Scheme
- typeProgram :: Program -> Either TypeError ([(Id, Scheme)], Scheme)
- prettyType :: Type -> Doc
- prettyScheme :: Scheme -> Doc
A type variable.
|TyArr Type Type|
The arrow type (A -> B)
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.
A type scheme. The
Int represents the number of quantified variables
(must be >= 0).
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'.
Unbound variable (value, not type variable).
Generic error, needed for the
Types a list of declarations (a
Program) returning the principal type for
each declaration and the type of the final expression.