Type inference for Haskell, part 13
This is part 13 of the series on type inference for Haskell.
There’s a kind of error our type system doesn’t check for yet. Right now, nothing prevents you from writing down a type that makes no sense. Consider this example:
That type signature makes no sense for two reasons: first, you cannot apply another type to
Maybe needs to have another type applied to it. Most likely the user intended to write
Maybe Int. But how do you catch that sort of error?
Trying to apply
Int to another type seems really similar to trying to apply a number like
123 to a value. The type system catches the later error. Do we perhaps create a sort of meta-type system to catch the former error?
It turns out that Haskell does have such a system. The “meta types” are called kinds. You can see the compiler talking about kinds if you try to compile the example above:
• Expecting one fewer argument to ‘Int’ Expected kind ‘(* -> *) -> *’, but ‘Int’ has kind ‘*’ • In the type signature: foo :: Int Maybe
(THIH Section 3, Kinds)
Kinds are a simpler system than types. All they really need to capture is how many types a given type wants to be applied to.
Int wants to be applied to no other types,
Maybe wants to be applied to one, and
Either wants to be applied to two. Kinds also recursively capture the kinds of those other types that this type will be applied to.
The way kinds are written looks a lot like function types. The kind of
* -> *. The kind of
* -> * -> *. The kind of
Int is just
*. The kind
* indicates that the type doesn’t need to be applied to anything more. When you apply a type of kind
* -> * to a type of kind
*, you get another type of kind
*. That’s what happens when you apply
Note that it is possible to express a kind like
(* -> *) -> *. This is different from the kind of
Either, which instead groups like
* -> (* -> *). A kind like this means that the type needs to be applied to another type of kind
* -> *. Here’s an example of a type with this kind:
You can run
:k SomeKind in GHCi to print out the kind of a type.
*Main> :k SomeKind SomeKind :: (* -> *) -> *
It has that kind because the type
a is applied to
Int. The type
Maybe would be valid to use as
*Main> :k (SomeKind Maybe) (SomeKind Maybe) :: *
Most of the possible places where a kind error could take place are in type declarations. Our code assumes that these have already been checked for validity. The actual type inference algorithm only needs to check that it doesn’t accidentally change kinds when it refines types. In other words, the substitutions need to be kind-preserving (see THIH Section 5, Substitutions).
The data structure used to store kinds is fairly simple.
A kind is then attached to type variables and type constructors:
Schemes also keep a list of kinds. When there is a
TGen n in the scheme’s type, that
n is an index into the list of kinds. That’s how it knows what kind the type variables should be when the scheme is instantiated.
(THIH Section 4, Types)
Most of the type definitions are of kind
* (because they cannot be applied to other types). They now look like:
The types that do need to be applied to some types get a kind like
* -> * or
* -> * -> *:
We also need a function to get the kind back out of these structures:
Note the logic for getting the kind of a
TAp. It trusts that the
TAp has been constructed correctly. If that’s the case, the kind of the left-hand side will be some
Kfun. The kind of the result of applying the two types is the right-hand side of that kind.
Say the type on the left was
Either (which has the kind
* -> * -> *) and the type on the right was
Bool (which has the kind
*). The kind of
Either Bool would then be
* -> * because that’s the right hand side of
* -> (* -> *) (parens added for clarity). Note that the left hand side of the kind matches the kind of
When creating a new type variable, we now need to supply the kind it should have:
The calls to
tiImpls always use
Star. That’s because bindings and variables shouldn’t be of an incomplete type. Any kind other than
* indicates that the type needs to be applied to more types.
The functions for creating a scheme are also updated. Note that quantification now stores the original kinds of the type variables that are being generalized:
toScheme :: Type -> Scheme toScheme t = Forall  t quantify :: [Tyvar] -> Type -> Scheme quantify vs t = Forall ks (apply s t) where vs' = [ v | v <- tv t, v `elem` vs ] ks = map kind vs' s = zip vs' (map TGen [0..]) freshInst :: Scheme -> TI Type freshInst (Forall ks t) = do ts <- mapM newTVar ks return (inst ts t)
Finally, the kinds are checked during unification. Specifically, they are checked when replacing a type variable with another type. A type variable should only be replaced with another type of the same kind.
(THIH Section 6, Unification and Matching)
You can find the updated code in kinds.hs.
It’s not easy to construct an expression that fails the “kinds do not match” check. Here’s one I was able to find. This fails in the definition of
It’s interesting to look at why this causes the error. The
getVal function has type
SomeKind t -> t Int. Applying
y means that the type of
y has to be
SomeKind t (for some
t). The kind of
t there is
* -> *. That means that the type of
y is the type constructor
SomeKind applied to another type of kind
* -> *.
unwrap function is also applied to
y. In the type of
unwrap, the kind of
b is simply
unwrap is applied to
y, it requires that the type of
y unify with
a b. Pay attention to
b. Here the right-hand side of
y’s type needs to be of kind
*, but the
getVal y expression forced it to be a type of kind
* -> *. And thus, there is an error.
This wraps up the fourth extension to the simple type system we originally defined. There is still a little bit left to do before moving on to type classes.