40 KiB
There is nothing more practical than a good theory.
— James C. Maxwell
Hindley-Milner Inference
The Hindley-Milner type system ( also referred to as Damas-Hindley-Milner or HM ) is a family of type systems that admit the serendipitous property of having a tractable algorithm for determining types from untyped syntax. This is achieved by a process known as unification, whereby the types for a well-structured program give rise to a set of constraints that when solved always have a unique principal type.
The simplest Hindley Milner type system is defined by a very short set of rules.
The first four rules describe the judgements by which we can map each syntactic
construct (Lam
, App
, Var
, Let
) to their expected types. We'll
elaborate on these rules shortly.
\begin{array}{cl}
\displaystyle\frac{x:\sigma \in \Gamma}{\Gamma \vdash x:\sigma} & \trule{T-Var} \\ \\
\displaystyle\frac{\Gamma \vdash e_1:\tau_1 \rightarrow \tau_2 \quad\quad \Gamma \vdash e_2 : \tau_1 }{\Gamma \vdash e_1\ e_2 : \tau_2} & \trule{T-App} \\ \\
\displaystyle\frac{\Gamma,\;x:\tau_1 \vdash e:\tau_2}{\Gamma \vdash \lambda\ x\ .\ e : \tau_1 \rightarrow \tau_2}& \trule{T-Lam} \\ \\
\displaystyle\frac{\Gamma \vdash e_1:\sigma \quad\quad \Gamma,\,x:\sigma \vdash e_2:\tau}{\Gamma \vdash \mathtt{let}\ x = e_1\ \mathtt{in}\ e_2 : \tau} & \trule{T-Let} \\ \\
\displaystyle\frac{\Gamma \vdash e: \sigma \quad \overline{\alpha} \notin \mathtt{ftv}(\Gamma)}{\Gamma \vdash e:\forall\ \overline{\alpha}\ .\ \sigma} & \trule{T-Gen}\\ \\
\displaystyle\frac{\Gamma \vdash e: \sigma_1 \quad\quad \sigma_1 \sqsubseteq \sigma_2}{\Gamma \vdash e : \sigma_2 } & \trule{T-Inst} \\ \\
\end{array}
Milner's observation was that since the typing rules map uniquely onto syntax, we can in effect run the typing rules "backwards" and whenever we don't have a known type for a subexpression, we "guess" by putting a fresh variable in its place, collecting constraints about its usage induced by subsequent typing judgements. This is the essence of type inference in the ML family of languages, that by the generation and solving of a class of unification problems we can reconstruct the types uniquely from the syntax. The algorithm itself is largely just the structured use of a unification solver.
However full type inference leaves us in a bit a bind, since while the problem of inference is tractable within this simple language and trivial extensions thereof, but nearly any major addition to the language destroys the ability to infer types unaided by annotation or severely complicates the inference algorithm. Nevertheless the Hindley-Milner family represents a very useful, productive "sweet spot" in the design space.
Syntax
The syntax of our first type inferred language will effectively be an extension of our untyped lambda calculus, with fixpoint operator, booleans, integers, let, and a few basic arithmetic operations.
type Name = String
data Expr
= Var Name
| App Expr Expr
| Lam Name Expr
| Let Name Expr Expr
| Lit Lit
| If Expr Expr Expr
| Fix Expr
| Op Binop Expr Expr
deriving (Show, Eq, Ord)
data Lit
= LInt Integer
| LBool Bool
deriving (Show, Eq, Ord)
data Binop = Add | Sub | Mul | Eql
deriving (Eq, Ord, Show)
data Program = Program [Decl] Expr deriving Eq
type Decl = (String, Expr)
The parser is trivial, the only addition will be the toplevel let declarations
(Decl
) which are joined into the global Program
. All toplevel
declarations must be terminated with a semicolon, although they can span
multiple lines and whitespace is ignored. So for instance:
-- SKI combinators
let I x = x;
let K x y = x;
let S f g x = f x (g x);
As before let rec
expressions will expand out in terms of the fixpoint
operator and are just syntactic sugar.
Polymorphism
We will add an additional constructs to our language that will admit a new form of polymorphism for our language. Polymorphism is the property of a term to simultaneously admit several distinct types for the same function implementation.
For instance the polymorphic signature for the identity function maps an input of
type \alpha
\begin{aligned}
\mathtt{id}\ & ::\ \forall \alpha. \alpha \to \alpha \\
\mathtt{id}\ & =\ \lambda x : \alpha.\ x
\end{aligned}
Now instead of having to duplicate the functionality for every possible type (i.e. implementing idInt, idBool, ...) we our type system admits any instantiation that is subsumed by the polymorphic type signature.
\begin{aligned}
& \t{id}_\t{Int} = \t{Int} \to \t{Int} \\
& \t{id}_\t{Bool} = \t{Bool} \to \t{Bool} \\
\end{aligned}
A rather remarkably fact of universal quantification is that many properties
about inhabitants of a type are guaranteed by construction, these are the
so-called free theorems. For instance any (nonpathological)
inhabitant of the type (a, b) -> a
must be equivalent to fst
.
A slightly less trivial example is that of the fmap
function of type
Functor f => (a -> b) -> f a -> f b
. The second functor law demands that:
forall f g. fmap f . fmap g = fmap (f . g)
However it is impossible to write down a (nonpathological) function for fmap
that has the required type and doesn't have this property. We get the theorem for free!
Types
The type language we'll use starts with the simple type system we used for our typed lambda calculus.
newtype TVar = TV String
deriving (Show, Eq, Ord)
data Type
= TVar TVar
| TCon String
| TArr Type Type
deriving (Show, Eq, Ord)
typeInt, typeBool :: Type
typeInt = TCon "Int"
typeBool = TCon "Bool"
Type schemes model polymorphic types, they indicate that the type variables bound in quantifier are polymorphic across the enclosed type and can be instantiated with any type consistent with the signature. Intuitively the indicate that the implementation of the function
data Scheme = Forall [TVar] Type
Type schemes will be written as \sigma
in our typing rules.
\begin{aligned}
\sigma ::=\ & \tau \\
& \forall \overline \alpha . \tau \\
\end{aligned}
For example the id
and the const
functions would have the following
types:
\begin{aligned}
\text{id} & : \forall a. a \rightarrow a \\
\text{const} & : \forall a b. a \rightarrow b \rightarrow a
\end{aligned}
We've now divided our types into two syntactic categories, the monotypes and the polytypes. In our simple initial languages type schemes will always be the representation of top level signature, even if there are no polymorphic type variables. In implementation terms this means when a monotype is yielded from our Infer monad after inference, we will immediately generalize it at the toplevel closing over all free type variables in a type scheme.
Context
The typing context or environment is the central container around which all
information during the inference process is stored and queried. In Haskell our
implementation will simply be a newtype wrapper around a Map of Var
to
Scheme
types.
newtype TypeEnv = TypeEnv (Map.Map Var Scheme)
The two primary operations are extension and restriction which introduce or remove named quantities from the context.
\Gamma \backslash x = \{ y : \sigma | y : \sigma \in \Gamma, x \ne y \}
\Gamma, x:\tau = (\Gamma \backslash x) \cup \{ x :\tau \}
Operations over the context are simply the usual Set operations on the underlying map.
extend :: TypeEnv -> (Var, Scheme) -> TypeEnv
extend (TypeEnv env) (x, s) = TypeEnv $ Map.insert x s env
Inference Monad
All our logic for type inference will live inside of the Infer
monad. It
is a monad transformer stack of ExceptT
+ State
, allowing various error
reporting and statefully holding the fresh name supply.
type Infer a = ExceptT TypeError (State Unique) a
Running the logic in the monad results in either a type error or a resulting type scheme.
runInfer :: Infer (Subst, Type) -> Either TypeError Scheme
runInfer m = case evalState (runExceptT m) initUnique of
Left err -> Left err
Right res -> Right $ closeOver res
Substitution
Two operations that will perform quite a bit are querying the free variables of an expression and applying substitutions over expressions.
\begin{aligned}
\FV{x} &= x \\
\FV{\lambda x. e} &= \FV{e} - \{ x \} \\
\FV{e_1 e_2} &= \FV{e_1} \cup \FV{e_2} \\
\end{aligned}
The same pattern applies to type variables at the type level.
\begin{aligned}
\FTV{\alpha} &= \{ \alpha \} \\
\FTV{\tau_1 \rightarrow \tau_2} &= \FTV{\tau_1} \cup \FTV{\tau_2} \\
\FTV{\t{Int}} &= \varnothing \\
\FTV{\t{Bool}} &= \varnothing \\
\FTV{\forall x. t} &= \FTV{t} - \{ x \} \\
\end{aligned}
Substitutions over expressions apply the substitution to local variables, replacing the named subexpression if matched. In the case of name capture a fresh variable is introduced.
\begin{aligned}
{[x / e'] x} &= e' \\
[x / e'] y &= y \quad (y \ne x) \\
[x / e'] (e_1 e_2) &= ([x / e'] \ e_1) ([x / e'] e_2) \\
[x / e'] (\lambda y. e_1) &= \lambda y. [x / e']e \quad y \ne x, y \notin \FV{e'} \\
\end{aligned}
And likewise, substitutions can be applied element wise over the typing environment.
[t / s] \Gamma = \{ y : [t /s] \sigma \ |\ y : \sigma \in \Gamma \}
Our implementation of a substitution in Haskell is simply a Map from type variables to types.
type Subst = Map.Map TVar Type
Composition of substitutions ( s_1 \circ s_2
, s1 `compose` s2
) can be encoded simply
as operations over the underlying map. Importantly note that in our
implementation we have chosen the substitution to be left-biased, it is up to
the implementation of the inference algorithm to ensure that clashes do not
occur between substitutions.
nullSubst :: Subst
nullSubst = Map.empty
compose :: Subst -> Subst -> Subst
s1 `compose` s2 = Map.map (apply s1) s2 `Map.union` s1
The implementation in Haskell is via a series of implementations of a
Substitutable
typeclass which exposes an apply
function which applies the
substitution given over the structure of the type replacing type variables as
specified.
class Substitutable a where
apply :: Subst -> a -> a
ftv :: a -> Set.Set TVar
instance Substitutable Type where
apply _ (TCon a) = TCon a
apply s t@(TVar a) = Map.findWithDefault t a s
apply s (t1 `TArr` t2) = apply s t1 `TArr` apply s t2
ftv TCon{} = Set.empty
ftv (TVar a) = Set.singleton a
ftv (t1 `TArr` t2) = ftv t1 `Set.union` ftv t2
instance Substitutable Scheme where
apply s (Forall as t) = Forall as $ apply s' t
where s' = foldr Map.delete s as
ftv (Forall as t) = ftv t `Set.difference` Set.fromList as
instance Substitutable a => Substitutable [a] where
apply = fmap . apply
ftv = foldr (Set.union . ftv) Set.empty
instance Substitutable TypeEnv where
apply s (TypeEnv env) = TypeEnv $ Map.map (apply s) env
ftv (TypeEnv env) = ftv $ Map.elems env
Throughout both the typing rules and substitutions we will require a fresh supply of names. In this naive version we will simply use an infinite list of strings and slice into n'th element of list per an index that we hold in a State monad. This is a simplest implementation possible, and later we will adapt this name generation technique to be more robust.
letters :: [String]
letters = [1..] >>= flip replicateM ['a'..'z']
fresh :: Infer Type
fresh = do
s <- get
put s{count = count s + 1}
return $ TVar $ TV (letters !! count s)
The creation of fresh variables will be essential for implementing the inference rules. Whenever we encounter the first use of a variable within some expression we will create a fresh type variable.
Unification
Central to the idea of inference is the notion of unification. A unifier
for two expressions e_1
and e_2
is a substitution s
such that:
s := [n_0 / m_0, n_1 / m_1, ..., n_k / m_k] \\
{[s]} e_1 = [s] e_2
Two terms are said to be unifiable if there exists a unifying substitution set between them. A substitution set is said to be confluent if the application of substitutions is independent of the order applied, i.e. if we always arrive at the same normal form regardless of the order of substitution chosen.
We'll adopt the notation
\tau \sim \tau' : s
for the fact that two types \tau, \tau'
are unifiable by a substitution s
,
such that:
[s] \tau = [s] \tau'
Two identical terms are trivially unifiable by the empty unifier.
c \sim c : [\ ]
The unification rules for our little HM language are as follows:
\begin{array}{cl}
c \sim c : [] & \quad \trule{Uni-Const} \\ \\
\alpha \sim \alpha : [] & \quad \trule{Uni-Var} \\ \\
\infrule{\alpha \notin \FTV{\tau}}{\alpha \sim \tau : [\alpha / \tau]}
& \quad \trule{Uni-VarLeft} \\ \\
\infrule{\alpha \notin \FTV{\tau}}{\tau \sim \alpha : [\alpha / \tau]}
& \quad \trule{Uni-VarRight} \\ \\
\infrule{
\tau_1 \sim \tau_1' : \theta_1 \andalso [\theta_1] \tau_2 \sim [\theta_1] \tau_2' : \theta_2
}{
\tau_1 \tau_2 \sim \tau_1' \tau_2' : \theta_2 \circ \theta_1
}
& \quad \trule{Uni-Con} \\ \\
\infrule{
\tau_1 \sim \tau_1' : \theta_1 \andalso [\theta_1] \tau_2 \sim [\theta_1] \tau_2' : \theta_2
}{
\tau_1 \rightarrow \tau_2 \sim \tau_1' \rightarrow \tau_2' : \theta_2 \circ \theta_1
}
& \quad \trule{Uni-Arrow} \\ \\
\end{array}
If we want to unify a type variable \alpha
with a type \tau
, we usually
can just substitute the variable with the type: [\alpha/\tau]
.
However, our rules state a precondition known as the occurs check
for that unification: the type variable \alpha
must not occur free in \tau
.
If it did, the substitution would not be a unifier.
Take for example the problem of unifying \alpha
and \alpha\rightarrow\beta
.
The substitution s=[\alpha/\alpha\rightarrow\beta]
doesn't unify:
we get
[s]\alpha=\alpha\rightarrow\beta
and
[s]\alpha\rightarrow\beta=(\alpha\rightarrow\beta)\rightarrow\beta.
Indeed, whatever substitution s
we try, [s]\alpha\rightarrow\beta
will
always be longer than [s]\alpha
, so no unifier exists.
The only chance would be to substitute with an infinite type:
$[\alpha/(\dots((\alpha\rightarrow\beta)\rightarrow\beta)\rightarrow\dots
\rightarrow\beta)\rightarrow\beta]$
would be a unifier, but our language has no such types.
If the unification fails because of the occurs check, we say that unification would give an infinite type.
Note that unifying \alpha\rightarrow\beta
and \alpha
is exactly what
we would have to do if we tried to type check the omega combinator
\lambda x.x x
, so it is ruled out by the occurs check, as are other
pathological terms we discussed when covering the untyped lambda calculus.
occursCheck :: Substitutable a => TVar -> a -> Bool
occursCheck a t = a `Set.member` ftv t
The unify function lives in the Infer monad and yields a subsitution:
unify :: Type -> Type -> Infer Subst
unify (l `TArr` r) (l' `TArr` r') = do
s1 <- unify l l'
s2 <- unify (apply s1 r) (apply s1 r')
return (s2 `compose` s1)
unify (TVar a) t = bind a t
unify t (TVar a) = bind a t
unify (TCon a) (TCon b) | a == b = return nullSubst
unify t1 t2 = throwError $ UnificationFail t1 t2
bind :: TVar -> Type -> Infer Subst
bind a t | t == TVar a = return nullSubst
| occursCheck a t = throwError $ InfiniteType a t
| otherwise = return $ Map.singleton a t
Generalization and Instantiation
At the heart of Hindley-Milner is two fundamental operations:
- Generalization: Converting a
\tau
type into a\sigma
type by closing over all free type variables in a type scheme. - Instantiation: Converting a
\sigma
type into a\tau
type by creating fresh names for each type variable that does not appear in the current typing environment.
\begin{array}{cl}
\displaystyle\frac{\Gamma \vdash e: \sigma \quad \overline{\alpha} \notin \mathtt{ftv}(\Gamma)}{\Gamma \vdash e:\forall\ \overline{\alpha}\ .\ \sigma} & \trule{T-Gen}\\ \\
\displaystyle\frac{\Gamma \vdash e: \sigma_1 \quad\quad \sigma_1 \sqsubseteq \sigma_2}{\Gamma \vdash e : \sigma_2 } & \trule{T-Inst} \\ \\
\end{array}
The \sqsubseteq
operator in the \trule{T-Inst}
rule indicates that a type is
an instantiation of a type scheme.
\forall \overline \alpha. \tau_2 \sqsubseteq \tau_1
A type \tau_1
is a instantiation of a type scheme $\sigma = \forall
\overline \alpha. \tau_2$ if there exists a substitution [s] \beta = \beta
for
all \beta \in \mathtt{ftv}(\sigma)
so that \tau_1 = [s] \tau_2
. Some
examples:
\begin{aligned}
\forall a. a \rightarrow a & \sqsubseteq \t{Int} \rightarrow \t{Int} \\
\forall a. a \rightarrow a & \sqsubseteq b \rightarrow b \\
\forall a b. a \rightarrow b \rightarrow a & \sqsubseteq \t{Int} \rightarrow \t{Bool} \rightarrow \t{Int}
\end{aligned}
These map very intuitively into code that simply manipulates the Haskell Set
objects of variables and the fresh name supply:
instantiate :: Scheme -> Infer Type
instantiate (Forall as t) = do
as' <- mapM (const fresh) as
let s = Map.fromList $ zip as as'
return $ apply s t
generalize :: TypeEnv -> Type -> Scheme
generalize env t = Forall as t
where as = Set.toList $ ftv t `Set.difference` ftv env
By convention let-bindings are generalized as much as possible. So for
instance in the following definition f
is generalized across the body of the
binding so that at each invocation of f
it is instantiated with fresh type
variables.
Poly> let f = (\x -> x) in let g = (f True) in f 3
3 : Int
In this expression, the type of f
is generated at the let definition and
will be instantiated with two different signatures. At call site of f
it
will unify with Int
and the other unify with Bool
.
By contrast, binding f
in a lambda will result in a type error.
Poly> (\f -> let g = (f True) in (f 3)) (\x -> x)
Cannot unify types:
Bool
with
Int
This is the essence of let generalization.
Typing Rules
And finally with all the typing machinery in place, we can write down the typing rules for our simple little polymorphic lambda calculus.
infer :: TypeEnv -> Expr -> Infer (Subst, Type)
The infer
maps the local typing environment and the active expression to a
2-tuple of the partial unifier solution and the intermediate type. The AST is
traversed bottom-up and constraints are solved at each level of recursion by
applying partial substitutions from unification across each partially inferred
subexpression and the local environment. If an error is encountered the
throwError
is called in the Infer
monad and an error is reported.
infer :: TypeEnv -> Expr -> Infer (Subst, Type)
infer env ex = case ex of
Var x -> lookupEnv env x
Lam x e -> do
tv <- fresh
let env' = env `extend` (x, Forall [] tv)
(s1, t1) <- infer env' e
return (s1, apply s1 tv `TArr` t1)
App e1 e2 -> do
tv <- fresh
(s1, t1) <- infer env e1
(s2, t2) <- infer (apply s1 env) e2
s3 <- unify (apply s2 t1) (TArr t2 tv)
return (s3 `compose` s2 `compose` s1, apply s3 tv)
Let x e1 e2 -> do
(s1, t1) <- infer env e1
let env' = apply s1 env
t' = generalize env' t1
(s2, t2) <- infer (env' `extend` (x, t')) e2
return (s1 `compose` s2, t2)
If cond tr fl -> do
(s1, t1) <- infer env cond
(s2, t2) <- infer env tr
(s3, t3) <- infer env fl
s4 <- unify t1 typeBool
s5 <- unify t2 t3
return (s5 `compose` s4 `compose` s3 `compose` s2 `compose` s1, apply s5 t2)
Fix e1 -> do
(s1, t) <- infer env e1
tv <- fresh
s2 <- unify (TArr tv tv) t
return (s2, apply s1 tv)
Op op e1 e2 -> do
(s1, t1) <- infer env e1
(s2, t2) <- infer env e2
tv <- fresh
s3 <- unify (TArr t1 (TArr t2 tv)) (ops Map.! op)
return (s1 `compose` s2 `compose` s3, apply s3 tv)
Lit (LInt _) -> return (nullSubst, typeInt)
Lit (LBool _) -> return (nullSubst, typeBool)
Let's walk through each of the rule derivations and look how it translates into code:
T-Var
The T-Var
rule, simply pull the type of the variable out of the typing
context.
Var x -> lookupEnv env x
The function lookupVar
looks up the local variable reference in typing
environment and if found it instantiates a fresh copy.
lookupEnv :: TypeEnv -> Var -> Infer (Subst, Type)
lookupEnv (TypeEnv env) x = do
case Map.lookup x env of
Nothing -> throwError $ UnboundVariable (show x)
Just s -> do t <- instantiate s
return (nullSubst, t)
\begin{array}{cl}
\displaystyle\frac{x:\sigma \in \Gamma}{\Gamma \vdash x:\sigma} & \trule{T-Var} \\ \\
\end{array}
T-Lam
For lambdas the variable bound by the lambda is locally scoped to the typing environment and then the body of the expression is inferred with this scope. The output type is a fresh type variable and is unified with the resulting inferred type.
Lam x e -> do
tv <- fresh
let env' = env `extend` (x, Forall [] tv)
(s1, t1) <- infer env' e
return (s1, apply s1 tv `TArr` t1)
\begin{array}{cl}
\displaystyle\frac{\Gamma,\;x:\tau_1 \vdash e:\tau_2}{\Gamma \vdash \lambda\ x\ .\ e : \tau_1 \rightarrow \tau_2}& \trule{T-Lam} \\ \\
\end{array}
T-App
For applications, the first argument must be a lambda expression or return a
lambda expression, so we know it must be of form t1 -> t2
but the output
type is not determined except by the confluence of the two values. We infer both
types, apply the constraints from the first argument over the result second
inferred type and then unify the two types with the excepted form of the entire
application expression.
App e1 e2 -> do
tv <- fresh
(s1, t1) <- infer env e1
(s2, t2) <- infer (apply s1 env) e2
s3 <- unify (apply s2 t1) (TArr t2 tv)
return (s3 `compose` s2 `compose` s1, apply s3 tv)
\begin{array}{cl}
\displaystyle\frac{\Gamma \vdash e_1:\tau_1 \rightarrow \tau_2 \quad\quad \Gamma \vdash e_2 : \tau_1 }{\Gamma \vdash e_1\ e_2 : \tau_2} & \trule{T-App} \\ \\
\end{array}
T-Let
As mentioned previously, let will be generalized so we will create a local typing environment for the body of the let expression and add the generalized inferred type let bound value to the typing environment of the body.
Let x e1 e2 -> do
(s1, t1) <- infer env e1
let env' = apply s1 env
t' = generalize env' t1
(s2, t2) <- infer (env' `extend` (x, t')) e2
return (s1 `compose` s2, t2)
\begin{array}{cl}
\displaystyle\frac{\Gamma \vdash e_1:\sigma \quad\quad \Gamma,\,x:\sigma \vdash e_2:\tau}{\Gamma \vdash \mathtt{let}\ x = e_1\ \mathtt{in}\ e_2 : \tau} & \trule{T-Let} \\ \\
\end{array}
T-BinOp
There are several builtin operations, we haven't mentioned up to now because the typing rules are trivial. We simply unify with the preset type signature of the operation.
Op op e1 e2 -> do
(s1, t1) <- infer env e1
(s2, t2) <- infer env e2
tv <- fresh
s3 <- unify (TArr t1 (TArr t2 tv)) (ops Map.! op)
return (s1 `compose` s2 `compose` s3, apply s3 tv)
ops :: Map.Map Binop Type
ops = Map.fromList [
(Add, (typeInt `TArr` (typeInt `TArr` typeInt)))
, (Mul, (typeInt `TArr` (typeInt `TArr` typeInt)))
, (Sub, (typeInt `TArr` (typeInt `TArr` typeInt)))
, (Eql, (typeInt `TArr` (typeInt `TArr` typeBool)))
]
\begin{array}{cl}
(+) &: \t{Int} \rightarrow \t{Int} \rightarrow \t{Int} \\
(\times) &: \t{Int} \rightarrow \t{Int} \rightarrow \t{Int} \\
(-) &: \t{Int} \rightarrow \t{Int} \rightarrow \t{Int} \\
(=) &: \t{Int} \rightarrow \t{Int} \rightarrow \t{Bool} \\
\end{array}
Literals
The type of literal integer and boolean types is trivially their respective types.
\begin{array}{cl}
\displaystyle \frac{}{\Gamma \vdash n : \mathtt{Int}} & \trule{T-Int} \\ \\
\displaystyle \frac{}{\Gamma \vdash \t{True} : \mathtt{Bool}} & \trule{T-True} \\ \\
\displaystyle \frac{}{\Gamma \vdash \t{False} : \mathtt{Bool}} & \trule{T-False}
\end{array}
Constraint Generation
The previous implementation of Hindley Milner is simple, but has this odd property of intermingling two separate processes: constraint solving and traversal. Let's discuss another implementation of the inference algorithm that does not do this.
In the constraint generation approach, constraints are generated by bottom-up traversal, added to a ordered container, canonicalized, solved, and then possibly back-substituted over a typed AST. This will be the approach we will use from here out, and while there is an equivalence between the "on-line solver", using the separate constraint solver becomes easier to manage as our type system gets more complex and we start building out the language.
Our inference monad now becomes a RWST
( Reader-Writer-State Transformer ) +
Except
for typing errors. The inference state remains the same, just the
fresh name supply.
-- | Inference monad
type Infer a = (RWST
Env -- Typing environment
[Constraint] -- Generated constraints
InferState -- Inference state
(Except -- Inference errors
TypeError)
a) -- Result
-- | Inference state
data InferState = InferState { count :: Int }
Instead of unifying type variables at each level of traversal, we will instead
just collect the unifiers inside the Writer and emit them with the uni
function.
-- | Unify two types
uni :: Type -> Type -> Infer ()
uni t1 t2 = tell [(t1, t2)]
Since the typing environment is stored in the Reader monad, we can use the
local
to create a locally scoped additions to the typing environment. This
is convenient for typing binders.
-- | Extend type environment
inEnv :: (Name, Scheme) -> Infer a -> Infer a
inEnv (x, sc) m = do
let scope e = (remove e x) `extend` (x, sc)
local scope m
Typing
The typing rules are identical, except they now can be written down in a much less noisy way that isn't threading so much state. All of the details are taken care of under the hood and encoded in specific combinators manipulating the state of our Infer monad in a way that lets us focus on the domain logic.
infer :: Expr -> Infer Type
infer expr = case expr of
Lit (LInt _) -> return $ typeInt
Lit (LBool _) -> return $ typeBool
Var x -> lookupEnv x
Lam x e -> do
tv <- fresh
t <- inEnv (x, Forall [] tv) (infer e)
return (tv `TArr` t)
App e1 e2 -> do
t1 <- infer e1
t2 <- infer e2
tv <- fresh
uni t1 (t2 `TArr` tv)
return tv
Let x e1 e2 -> do
env <- ask
t1 <- infer e1
let sc = generalize env t1
t2 <- inEnv (x, sc) (infer e2)
return t2
Fix e1 -> do
t1 <- infer e1
tv <- fresh
uni (tv `TArr` tv) t1
return tv
Op op e1 e2 -> do
t1 <- infer e1
t2 <- infer e2
tv <- fresh
let u1 = t1 `TArr` (t2 `TArr` tv)
u2 = ops Map.! op
uni u1 u2
return tv
If cond tr fl -> do
t1 <- infer cond
t2 <- infer tr
t3 <- infer fl
uni t1 typeBool
uni t2 t3
return t2
Constraint Solver
The Writer layer for the Infer monad contains the generated set of constraints emitted from inference pass. Once inference has completed we are left with a resulting type signature full of meaningless unique fresh variables and a set of constraints that we must solve to refine the type down to its principal type.
The constraints are pulled out solved by a separate Solve
monad which holds
the Unifier ( most general unifier ) solution that when applied to generated
signature will yield the solution.
type Constraint = (Type, Type)
type Unifier = (Subst, [Constraint])
-- | Constraint solver monad
type Solve a = StateT Unifier (ExceptT TypeError Identity) a
The unification logic is also identical to before, except it is now written independent of inference and stores its partial state inside of the Solve monad's state layer.
unifies :: Type -> Type -> Solve Unifier
unifies t1 t2 | t1 == t2 = return emptyUnifer
unifies (TVar v) t = v `bind` t
unifies t (TVar v) = v `bind` t
unifies (TArr t1 t2) (TArr t3 t4) = unifyMany [t1, t2] [t3, t4]
unifies t1 t2 = throwError $ UnificationFail t1 t2
unifyMany :: [Type] -> [Type] -> Solve Unifier
unifyMany [] [] = return emptyUnifer
unifyMany (t1 : ts1) (t2 : ts2) =
do (su1,cs1) <- unifies t1 t2
(su2,cs2) <- unifyMany (apply su1 ts1) (apply su1 ts2)
return (su2 `compose` su1, cs1 ++ cs2)
unifyMany t1 t2 = throwError $ UnificationMismatch t1 t2
The solver function simply iterates over the set of constraints, composing them and applying the resulting constraint solution over the intermediate solution eventually converting on the most general unifier which yields the final subsitution which when applied over the inferred type signature, yields the principal type solution for the expression.
-- Unification solver
solver :: Solve Subst
solver = do
(su, cs) <- get
case cs of
[] -> return su
((t1, t2): cs0) -> do
(su1, cs1) <- unifies t1 t2
put (su1 `compose` su, cs1 ++ (apply su1 cs0))
solver
This a much more elegant solution than having to intermingle inference and solving in the same pass, and adapts itself well to the generation of a typed Core form which we will discuss in later chapters.
Worked Examples
Let's walk through two examples of how inference works for simple functions.
Example 1
Consider:
\x y z -> x + y + z
The generated type from the infer
function consists simply of a fresh
variable for each of the arguments and the return type.
a -> b -> c -> e
The constraints induced from T-BinOp are emitted as we traverse both of the addition operations.
a -> b -> d ~ Int -> Int -> Int
d -> c -> e ~ Int -> Int -> Int
Here d
is the type of the intermediate term x + y
.
By applying Uni-Arrow we can then deduce the following set of substitutions.
a ~ Int
b ~ Int
c ~ Int
d ~ Int
e ~ Int
Substituting this solution back over the type yields the inferred type:
Int -> Int -> Int -> Int
Example 2
compose f g x = f (g x)
The generated type from the infer
function consists again simply of unique
fresh variables.
a -> b -> c -> e
Induced by two cases of the T-App rule we get the following constraints:
b ~ c -> d
a ~ d -> e
Here d
is the type of (g x)
.
The constraints are already in a canonical form, by applying Uni-VarLeft
twice we get the following set of substitutions:
b ~ c -> d
a ~ d -> e
So we get this type:
compose :: forall c d e. (d -> e) -> (c -> d) -> c -> e
If desired, we can rename the variables in alphabetical order to get:
compose :: forall a b c. (a -> b) -> (c -> a) -> c -> b
Interpreter
Our evaluator will operate directly on the syntax and evaluate the results in
into a Value
type.
data Value
= VInt Integer
| VBool Bool
| VClosure String Expr TermEnv
The interpreter is set up an Identity monad. Later it will become a more complicated monad, but for now its quite simple. The value environment will explicitly threaded around, and whenever a closure is created we simply store a copy of the local environment in the closure.
type TermEnv = Map.Map String Value
type Interpreter t = Identity t
Our logic for evaluation is an extension of the lambda calculus evaluator implemented in previous chapter. However you might notice quite a few incomplete patterns used throughout evaluation. Fear not though, the evaluation of our program cannot "go wrong". Each of these patterns represents a state that our type system guarantees will never happen. For example, if our program did have not every variable referenced in scope then it would never reach evaluation to begin with and would be rejected in our type checker. We are morally correct in using incomplete patterns here!
eval :: TermEnv -> Expr -> Interpreter Value
eval env expr = case expr of
Lit (LInt k) -> return $ VInt k
Lit (LBool k) -> return $ VBool k
Var x -> do
let Just v = Map.lookup x env
return v
Op op a b -> do
VInt a' <- eval env a
VInt b' <- eval env b
return $ (binop op) a' b'
Lam x body ->
return (VClosure x body env)
App fun arg -> do
VClosure x body clo <- eval env fun
argv <- eval env arg
let nenv = Map.insert x argv clo
eval nenv body
Let x e body -> do
e' <- eval env e
let nenv = Map.insert x e' env
eval nenv body
If cond tr fl -> do
VBool br <- eval env cond
if br == True
then eval env tr
else eval env fl
Fix e -> do
eval env (App e (Fix e))
binop :: Binop -> Integer -> Integer -> Value
binop Add a b = VInt $ a + b
binop Mul a b = VInt $ a * b
binop Sub a b = VInt $ a - b
binop Eql a b = VBool $ a == b
Interactive Shell
Our language has now grown out the small little shells we were using before, and now we need something much more robust to hold the logic for our interactive interpreter.
We will structure our REPL as a monad wrapped around IState (the interpreter state) datatype. We will start to use the repline library from here out which gives us platform independent readline, history, and tab completion support.
data IState = IState
{ tyctx :: TypeEnv -- Type environment
, tmctx :: TermEnv -- Value environment
}
initState :: IState
initState = IState emptyTyenv emptyTmenv
type Repl a = HaskelineT (StateT IState IO) a
hoistErr :: Show e => Either e a -> Repl a
hoistErr (Right val) = return val
hoistErr (Left err) = do
liftIO $ print err
abort
Our language can be compiled into a standalone binary by GHC:
$ ghc --make Main.hs -o poly
$ ./poly
Poly>
At the top of our program we will look at the command options and allow three variations of commands.
$ poly # launch shell
$ poly input.ml # launch shell with 'input.ml' loaded
$ poly test input.ml # dump test for 'input.ml' to stdout
main :: IO ()
main = do
args <- getArgs
case args of
[] -> shell (return ())
[fname] -> shell (load [fname])
["test", fname] -> shell (load [fname] >> browse [] >> quit ())
_ -> putStrLn "invalid arguments"
The shell command takes a pre
action which is run before the shell starts
up. The logic simply evaluates our Repl monad into an IO and runs that from the
main function.
shell :: Repl a -> IO ()
shell pre
= flip evalStateT initState
$ evalRepl "Poly> " cmd options completer pre
The cmd
driver is the main entry point for our program, it is executed every
time the user enters a line of input. The first argument is the line of user
input.
cmd :: String -> Repl ()
cmd source = exec True (L.pack source)
The heart of our language is then the exec
function which imports all the
compiler passes, runs them sequentially threading the inputs and outputs and
eventually yielding a resulting typing environment and the evaluated result of
the program. These are monoidally joined into the state of the interpreter and
then the loop yields to the next set of inputs.
exec :: Bool -> L.Text -> Repl ()
exec update source = do
-- Get the current interpreter state
st <- get
-- Parser ( returns AST )
mod <- hoistErr $ parseModule "<stdin>" source
-- Type Inference ( returns Typing Environment )
tyctx' <- hoistErr $ inferTop (tyctx st) mod
-- Create the new environment
let st' = st { tmctx = foldl' evalDef (tmctx st) mod
, tyctx = tyctx' <> (tyctx st)
}
-- Update the interpreter state
when update (put st')
Repline also supports adding special casing certain sets of inputs so that they map to builtin commands in the compiler. We will implement three of these.
Command Action
:browse
Browse the type signatures for a program
:load <file>
Load a program from file
:type
Show the type of an expression
:quit
Exit interpreter
Their implementations are mostly straightforward.
options :: [(String, [String] -> Repl ())]
options = [
("load" , load)
, ("browse" , browse)
, ("quit" , quit)
, ("type" , Main.typeof)
]
-- :browse command
browse :: [String] -> Repl ()
browse _ = do
st <- get
liftIO $ mapM_ putStrLn $ ppenv (tyctx st)
-- :load command
load :: [String] -> Repl ()
load args = do
contents <- liftIO $ L.readFile (unwords args)
exec True contents
-- :type command
typeof :: [String] -> Repl ()
typeof args = do
st <- get
let arg = unwords args
case Infer.typeof (tyctx st) arg of
Just val -> liftIO $ putStrLn $ ppsignature (arg, val)
Nothing -> exec False (L.pack arg)
-- :quit command
quit :: a -> Repl ()
quit _ = liftIO $ exitSuccess
Finally tab completion for our shell will use the interpreter's typing
environment keys to complete on the set of locally defined variables. Repline
supports prefix based tab completion where the prefix of the current command
will be used to determine what to tab complete. In the case where we start with
the command :load
we will instead tab complete on filenames in the current
working directly instead.
completer :: CompleterStyle (StateT IState IO)
completer = Prefix (wordCompleter comp) defaultMatcher
-- Prefix tab completer
defaultMatcher :: MonadIO m => [(String, CompletionFunc m)]
defaultMatcher = [
(":load" , fileCompleter)
]
-- Default tab completer
comp :: (Monad m, MonadState IState m) => WordCompleter m
comp n = do
let cmds = [":load", ":browse", ":quit", ":type"]
TypeEnv ctx <- gets tyctx
let defs = Map.keys ctx
return $ filter (isPrefixOf n) (cmds ++ defs)
Observations
There we have it, our first little type inferred language! Load the poly
interpreter by running ghci Main.hs
and the call the main
function.
$ ghci Main.hs
λ: main
Poly> :load test.ml
Poly> :browse
Try out some simple examples by declaring some functions at the toplevel of the
program. We can query the types of expressions interactively using the :type
command which effectively just runs the expression halfway through the pipeline
and halts after typechecking.
Poly> let id x = x
Poly> let const x y = x
Poly> let twice x = x + x
Poly> :type id
id : forall a. a -> a
Poly> :type const
const : forall a b. a -> b -> a
Poly> :type twice
twice : Int -> Int
Notice several important facts. Our type checker will now flat our reject programs with scoping errors before interpretation.
Poly> \x -> y
Not in scope: "y"
Also programs that are also not well-typed are now rejected outright as well.
Poly> 1 + True
Cannot unify types:
Bool
with
Int
The omega combinator will not pass the occurs check.
Poly> \x -> x x
Cannot construct the the infinite type: a = a -> b
The file test.ml
provides a variety of tests of the little interpreter. For
instance both fact
and fib
functions uses the fixpoint to compute
Fibonacci numbers or factorials.
let fact = fix (\fact -> \n ->
if (n == 0)
then 1
else (n * (fact (n-1))));
let rec fib n =
if (n == 0)
then 0
else if (n==1)
then 1
else ((fib (n-1)) + (fib (n-2)));
Poly> :type fact
fact : Int -> Int
Poly> fact 5
120
Poly> fib 16
610
Full Source
\pagebreak