by Nicolas Wu

Posted on 4 November 2010

Tags: Haskell

While most programmers will already have a good notion of what a value *type* is, the notion of a *kind* is not as widespread. This article introduces value kinds. Roughly speaking, a type is to a value as a kind is to a type, or in other words, kinds can be thought of as the type of a type.

To understand what a kind is, it helps to think of functions as ways of expressing *value constructors*, and make the following observation:

Types provide signatures for value constructors.

In a similar way, we can look to *type constructors*, and make the following observation:

Kinds provide signatures for type constructors.

Later on, I’ll be making use of the following extensions:

`> {-# LANGUAGE TypeOperators, KindSignatures #-}`

Modern programming languages make use of the notion of a value *type* in order to categorise values into different groups. In Haskell, the type signature of a function is particularly revealing, since it gives an indication of what the function does.

For example, consider the type of the function `id`

:

```
> id :: a -> a
> id x = x
```

The type of this function forces the definition of `id`

to be the identity function, since there is no way of producing a value of type `a`

other than using the one that is supplied as an argument to the function itself.

Another simple example is the type signature of `const`

:

```
> const :: a -> b -> a
> const x y = x
```

Although two inputs values are given as input, only one of these values has the required output type so the definition of this functions is forced too.

As a more complicated example, consider the definition of function composition:

```
> (.) :: (b -> c) -> (a -> b) -> (a -> c)
> (g . f) x = g (f x)
```

Kind signatures provide information about types. For example, consider the datatype `Id`

, which represents an identity datatype:

`> data Id a = Id a`

The kind of this type constructor can be inspected in `ghci`

using the `:k`

query:

```
*Main> :k Id
Id :: * -> *
```

When giving kind signatures the `*`

symbol is used to denote a placeholder for a type, and the arrows between the kinds tell us that this type constructor takes a type of kind `*`

and returns a type of kind `*`

.

Unlike type signatures, the choice of implementation for `Id`

is not forced: the definition of `Maybe`

also has kind `* -> *`

:

`data Maybe a = Nothing | Just a`

This difference between types and kinds arises because kinds are not polymorphic. The next primitive type constructor to consider is the constant constructor, which has the following signature:

`Const :: * -> * -> *`

As with `Id`

, a number of different constructors satisfy this signature, but here’s one that is in line with the `const`

function mentioned above:

`> data Const a b = Const a`

Our final example mirrors the function composition we saw previously (which we can think of as value construction composition). In a similar vein, we’ll consider a definition for type constructor composition:

`> data (g :.: f) a = (:.:) g (f a)`

Here we’ve made use of the `TypeOperators`

extension of Haskell, which allows us to define symbolic operators at the type level. A type operator must be prefixed with a colon, which explains the strange syntax that is used here (the trailing colon is there to make the operator symmetric). The type signature of this construct is as follows:

`(:.:) :: (* -> *) -> (* -> *) -> (* -> *)`

In other words, this type constructor takes two type constructors of kind `* -> *`

to produce another.

As a closing remark, the `KindSignatures`

language extension of `ghc`

allows us to annotate the kinds of type variables, which can sometimes make things a little easier. For example, here’s a definition of a product type:

`> data ((f :: * -> *) :*: (g :: * -> *)) a = f a :*: g a`

The complexity of a type constructor is measured in terms of its *order*. The order is defined as follows:

```
order * = 0
order (a -> b) = max (1 + order a) (order b)
```

The order of ordinary types like `Bool`

and `Int`

is therefore \(0\), while the rank of `Id`

is \(1\), since

```
order (* -> *)
==
max (1 + order *) (order *)
==
max (1 + 0) 0
==
1
```

More complex orders, such as that of `(:.:)`

can also be calculated:

```
order ((* -> *) -> (* -> *) -> (* -> *))
==
max (1 + order (* -> *)) (order ((* -> *) -> (* -> *)))
==
max (1 + 1) (max (1 + order (* -> *)) (order (* -> *)))
==
max 2 (max (1 + 1) 1)
==
max 2 (max 2 1)
==
2
```

This article has provided a short introduction to kind signatures. Here’s a summary of some of the points made:

- Kinds are to types as types are to values.
- Kinds are built using
`*`

and`->`

. - Kinds can be inspected in
`ghci`

using`:k`

. - Kinds can be annotated in data declarations.
- Kinds can be categorised in terms of their order.