If you’ve been using Haskell you’ll know that it has an expressive static type system. This gives us a way to reason about how our programs will behave before we even run them, and, at least in my case, prevents a lot of dumb errors.
Just as Haskell has a type system to classify values, it has a kind system to classify types. It provides a way to reason about what types make sense to construct. Let’s see what it’s all about.
Type
s, Type
s Everywhere
The most common kind of type1 you’ll see are Type
s (shocking, isn’t it?). These include Int
, Bool
, Char
, as well as Double -> String
, [Integer]
, and Either Rational [Bool]
. Another name for the kind Type
is *
. We can check a type’s kind in GHCi with :kind
or :k
for short.
ghci> :k [Integer]
[Integer] :: *
If we turn on the language extension NoStarIsType
GHCi will instead use the more modern name Type
(which is located in the Data.Kind
module).
ghci> :set -XNoStarIsType
ghci> :k [Integer]
[Integer] :: Type
If you see that a type has kind Type
that means it can appear on its own on the right-hand side of a ::
2, as in
ints :: [Integer]
= [1,2,3] ints
Of course, it’s hard to understand what being a Type
means if you don’t know what types don’t have kind Type
. An example of something with kind different from Type
is Maybe
. Maybe
can’t show up on its own as a type signature, it just doesn’t make sense. The same thing goes for Either
. However, if we apply Maybe
to a type, for example, Int
, and then we get a normal type, Maybe Int
, which can appear on its own on the right of a ::
.
it'sAnIntIPromise :: Maybe Int
= Just 42 it'sAnIntIPromise
Also notice that we specifically have to give Maybe
something of kind Type
. It wouldn’t make sense to have a Maybe Either
. So if we give Maybe
a Type
, it becomes a Type
. So you might even say that the kind of Maybe
is Type -> Type
. And indeed GHCi agrees with us:
ghci> :k Maybe
Maybe :: Type -> Type
Now, what about Either
? Just as with Maybe
it doesn’t make sense to pass it something that’s not a Type
. But even if we pass it a Type
, we don’t get a Type
just yet, I can’t have an Either Bool
in my pocket. But if we pass Either Bool
a Type
we indeed get a normal bona fide Type
, such as Either Bool Int
. Meaning, Either Bool
must have kind Type -> Type
, just like Maybe
. But what that means is that if we pass Either
a Type
we get back a Type -> Type
, meaning Either
must have kind Type -> (Type -> Type)
.
Did you notice? This is currying! Since ->
associates to the right by default we can drop the parentheses and say that Either
has kind Type -> Type -> Type
. Just like with currying functions, there are two equivalent ways of looking at Either
. We can look at it as a type that takes two Type
s and becomes a Type
, or as a type that takes a Type
and returns a Type -> Type
. Check it in GHCi!
If we try to have something nonsensical like Maybe Either
then GHC will give us a kind error:
λ> type T = Maybe Either
<interactive>:1:16: error:
• Expecting two more arguments to ‘Either’
Expected a type, but ‘Either’ has kind ‘Type -> Type -> Type’
• In the first argument of ‘Maybe’, namely ‘Either’
In the type ‘Maybe Either’
In the type declaration for ‘T’
This is the bread and butter of what kinds are for, sanity checking.
Another thing we can notice is that (->)
is just like Either
, it takes two Type
s and returns a Type
, specifically a function type. Another important type to consider is []
, the list type. It takes a type, such as Int
, and returns a Type
. In fact, [Int]
is the same as [] Int
, it’s just syntax sugar, you can try it yourself.
Let’s look at a more complex example:
data OfInts f = MkOfInts (f Int)
This is a pretty weird type. It takes some f
and stores an f
of Int
s. Let’s figure out the kind of OfInts
. f
must take a type as input since we see f Int
appear. But then f Int
must be a Type
since OfInts
stores a value of type f Int
. So f
must have kind Type -> Type
. Now, OfInts f
must be a Type
, since it’s a fully-fledged datatype that you can have values of. So putting this together, OfInts
must take a Type -> Type
and returns a Type
, meaning it has (Type -> Type) -> Type
.
Exercises
Without using GHCi, what is the kind of
(,,)
, the type constructor for 3-tuples?Consider the following datatype declaration:
newtype MaybeT m a = MaybeT { runMaybeT :: m (Maybe a) }
Without using GHCi, what is the kind of
MaybeT
? Note thatnewtype
is the same thing asdata
as far as the kinds go.Consider the following datatype declaration:
data Contrived f g a = MkContrived (f Maybe (Either a (g Bool)))
Without using GHCi, what is the kind of
Contrived
?
Getting Classy with Constraint
We’ve seen the kinds of various datatypes, and it seems they always have a kind which is some mix of Type
and ->
perhaps with some parentheses. What about something a bit different, like Num
? Well, as input, it only makes sense to pass Num
a Type
, such as Int
or Double
, or even Bool
, since Num
defines methods like negate :: Num a => a -> a
. Since the function arrow takes Type
s as inputs (remember the kind of (->)
?) it means that a
must be a Type
. What does Num
return though? What is the kind of Num Int
? Well, this is a new kind called Constraint
. A type expression of kind Constraint
is any type expression that can appear on the left of a =>
in a type signature. For example, the following is legal:
what :: Num Bool => Bool
= True + False what
This is a bit of an odd example, but it’s an important one to understand. Bool
is a type of kind Type
, so it’s legal to pass it to Num
, and the resulting Constraint
is completely valid. Beyond that, unrelated to the kind system, in the definition for what
we’ve required that there be a Num Bool
instance in scope at the call site. Therefore we can safely use +
with our Bool
s. Of course, we can’t actually use what
without defining this instance. GHC will complain:
ghci> what
<interactive>:5:1: error:
• No instance for (Num Bool) arising from a use of ‘what’
• In the expression: what
In an equation for ‘it’: it = what
So Num
has kind Type -> Constraint
since it takes a Type
and returns a Constraint
. So do many other familiar type classes such as Ord
, Show
, and Monoid
. An example of a typeclass with a more complex kind would be Functor
. Functor
doesn’t take a Type
. For example, it doesn’t make sense to write a Functor Bool
instance. To see exactly why let’s look at the type of fmap
:
ghci> :t fmap
fmap :: Functor f => (a -> b) -> f a -> f b
Since a
appears next to a ->
it must have kind Type
, and similarly f a
appears next to a ->
so it must also have kind Type
. Therefore f
must have kind Type -> Type
, which makes sense as f
could be Maybe
or Either Bool
for example. So Functor
takes a Type -> Type
and yields a Constraint
, meaning it has kind (Type -> Type) -> Constraint
. Applicative
must also have the same kind, even without looking at its methods. If we look at the class header for Applicative
we see
class Functor f => Applicative f where
Since f
appears as an argument to Functor
it must have kind Type -> Type
and therefore Applicative
must have kind (Type -> Type) -> Constraint
. For the same reason, Monad
must also have that kind.
Exercises
Consider the following (trimmed down) definition of the
Bifunctor
class:class Bifunctor p where bimap :: (a -> b) -> (c -> d) -> p a c -> p b d
Without using GHCi, what is the kind of
Bifunctor
? Don’t worry about understanding what the class is for, just focus on the kinds.Haskell has an extension called
MultiParamTypeClasses
. It allows for typeclass with multiple type parameters. For example, take the following class:class Convert a b where convert :: a -> b
Convert
has kindType -> Type -> Constraint
.Consider the following (simplified) definition of the
MonadReader
class:class Monad m => MonadReader r m where ask :: m r
Without using GHCi, what is the kind of
MonadReader
?Consider the following (simplified) definition of the
MonadTrans
class:class MonadTrans t where lift :: Monad m => m a -> t m a
Without using GHCi, what is the kind of
MonadTrans
?Hint: Recall
MaybeT
from earlier. There is aninstance MonadTrans MaybeT
defined in thetransformers
library.Define your own type such that it could potentially have a
MonadTrans
instance, considering only the kinds involved.
Yo Dawg, I Heard You Like Types
Consider this curious function:
import Data.Kind (Type)
myId :: Type -> Type
= x myId x
GHC accepts this code, which seems very odd. What’s Type
doing in a type signature? I thought Type
was a kind? In truth, in modern GHC there is no such thing as a kind. By that, I mean that there’s no separate “kind level” with its own special values. Rather, all kinds are just types. The ->
in kinds is the normal function arrow. This is a relatively recent change introduced by the TypeInType
language extension in GHC 8.0 which later became the default way GHC handles kinds (deprecating the TypeInType
extension).
If we ask GHCi the kind of Type
we get back
ghci> import Data.Kind
ghci> :k Type
Type
So Type
is a normal type that could potentially have values. In actuality, it’s uninhabited like the Void
datatype is. As a reminder, Void
is an empty datatype, with no values (that don’t loop or crash when evaluated), defined as
data Void
Just like you can have undefined :: Void
and myId :: Void -> Void
so too you can have undefined :: Type
and myId :: Type -> Type
.
It’s best to think of “kinds” as a relationship between types. Type
“is the kind of” Int
. Type -> Type
“is the kind of” Maybe
. The only thing that differentiates “a kind” from “a type” is that a kind is just a type that happens to be the kind of another type. As an analogy, “a parent” is a person that happens to “be the parent of” another person.
This is cool and all, but perhaps this will make more sense once we learn about DataKinds
.
Exercises
Write a function with the type
Void -> Type
. I recommend taking a look atData.Void
for this.Write a function
preposterous :: Type -> a
. You can make use of theEmptyCase
extension for this.
Get Promoted with DataKinds
Up until now, the only kinds we’ve seen are Type
/*
, Constraint
, and k1 -> k2
where k1
and k2
are themselves kinds. Keep in mind that “kind” here means a type that is the kind of another type. The DataKinds
extension opens up the world of kinds and turns every algebraic datatype into a kind. As an example, normally Bool
is a type but not a kind. There is no type expression with Bool
as its kind. But with DataKinds
we get two new type expressions, 'False
and 'True
, which both have kind Bool
. Notice the tick marks, these are not the same as the term-level values False
and True
, they exist on the type level. It also doesn’t make sense to have a value whose type is 'True
, since it only makes sense to have values if your kind is Type
and 'True
has kind Bool
, not Type
.
So what is this useful for? In general, DataKinds
is mostly useful in conjunction with other extensions to the type system, since those extensions are all about manipulating types, and DataKinds
gives us a plethora of new types to work with. You’ll notice that I’ve used them in every single one of my previous posts because they’re just that useful.
Just as an example, you can have a datatype that’s parameterized over a Bool
type parameter.
newtype NonZero (verified :: Bool) = NonZero Int
-- ^^^^^^^^^^^^^^^^^
-- This is a kind signature, which lets us tell GHC
-- what kind `verified` has. Without it, GHC will infer the kind
-- to be `Type`.
Then you can have code like
mkNonZero :: Int -> NonZero False
= NonZero
mkNonZero
verifyNonZero :: NonZero False -> Maybe (NonZero True)
NonZero 0) = Nothing
verifyNonZero (NonZero n) = Just (NonZero n)
verifyNonZero (
divSafe :: Int -> NonZero True Int -> Int
NonZero n) = div m n divSafe m (
This is a bit of a dumb example since having an unverified NonZero
isn’t very useful,
but you can imagine that it might be useful for something like an email address type, for example,
where an unverified email address is syntactically valid, while a verified email address is one
that has been verified to exist, perhaps by sending a verification email.
Exercises
Write the data/newtype declaration for an
Email
type as mentioned above.Change the kind of the type parameter from
Bool
toVerification
, whereVerification
isdata Verification = Unverified | Verified
Write a hypothetical API for such an email type as type signatures. You can fill in the definitions with
undefined
or typed holes if you wish.
Some Kind of Conclusion
There is much that this article hasn’t covered, such as PolyKinds
, TYPE r
, and more. The kind system pervades the GHC Haskell language more and more as more type-level programming features are added. This adds many interactions which could each be enough to fill their own article.
One last thing I will note is that since GHC 8.10 you can give your type declarations what are called standalone kind signatures, enabled by the (gasp) StandaloneKindSignatures
language extension. They look much like type signatures do, but with the type
keyword in front of them. Some examples:
type Foo :: Type -> Type
newtype Foo a = Foo [a]
type C :: Type -> Constraint
class C a where
type NonZero :: Bool -> Type
newtype NonZero bool = NonZero Int
-- ^^^^
-- This is a phantom type parameter of kind Bool
-- using DataKinds.