A Kind Introduction
by Nicolas Wu
Posted on 4 November 2010
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:
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
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
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:
Kind signatures provide information about types. For example, consider the datatype
Id, which represents an identity datatype:
The kind of this type constructor can be inspected in
ghci using the
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
* -> *:
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:
Id, a number of different constructors satisfy this signature, but here’s one that is in line with the
const function mentioned above:
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:
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:
The complexity of a type constructor is measured in terms of its order. The order is defined as follows:
The order of ordinary types like
Int is therefore 0, while the rank of
Id is 1, since
More complex orders, such as that of
(:.:) can also be calculated:
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
- Kinds can be inspected in
- Kinds can be annotated in data declarations.
- Kinds can be categorised in terms of their order.