A Kind Introduction

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 #-}

Types

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)

Kinds

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

Order

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

Summary

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.

Comments