One of a Kind: An Introduction to Kinds in Haskell

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¹ you’ll see are Types (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 ::², as in

ints :: [Integer]
ints = [1,2,3]

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
it'sAnIntIPromise = Just 42

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 Types 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 Types 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 Ints. 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 Types 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
what = True + False

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 Bools. 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
myId x = 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
mkNonZero = NonZero

verifyNonZero :: NonZero False -> Maybe (NonZero True)
verifyNonZero (NonZero 0) = Nothing
verifyNonZero (NonZero n) = Just (NonZero n)

divSafe :: Int -> NonZero True Int -> Int
divSafe m (NonZero n) = div m n

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.

One of a Kind: An Introduction to Kinds in Haskell

Types, Types Everywhere

Exercises

Getting Classy with Constraint

Exercises

Yo Dawg, I Heard You Like Types

Exercises

Get Promoted with DataKinds

Exercises

Some Kind of Conclusion

`Type`s, `Type`s Everywhere

Getting Classy with `Constraint`

Get Promoted with `DataKinds`