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 type^{1} 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 that`newtype`

is the same thing as`data`

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 kind`Type -> 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 an`instance MonadTrans MaybeT`

defined in the`transformers`

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 at`Data.Void`

for this.Write a function

`preposterous :: Type -> a`

. You can make use of the`EmptyCase`

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`

to`Verification`

, where`Verification`

is`data 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.
```