Kind (type theory)

In computer science and type theory, a kind is a "type of a type". Kinds appear, either explicitly or implicitly, in certain languages with complex type systems, such as Haskell and Scala . In the same way that types are used to describe the available operations on a value, kinds are used to describe the available operations on a type.

Kind systems are often far simpler than type systems. They are used primarily to distinguish between "data types" and "type constructors".

Kinds in Haskell

Haskell's kind system has just two rules:

• $*$ is the kind of all "data types".
• $k_{1}\to k_{2}$ is the kind of a "type constructor", which takes a type of kind $k_{1}$ and produces a type of kind $k_{2}$.

A "data type" (or "inhabited type") is a type which has values. For instance, 4 is a value of type Int, while [1, 2, 3] is a value of type [Int] (list of Ints). Therefore, Int and [Int] are both types of kind $*$.

A "type constructor" takes one or more type arguments, and produces a data type when enough arguments are supplied. This is how Haskell achieves parametric types. For instance, the type [] (list) is a type constructor - it takes a single argument to specify the type of the elements of the list. Hence, [Int] (list of Ints), [Float] (list of Floats) and even [[Int]] (list of lists of Ints) are valid applications of the [] type constructor. Therefore, [] is a type of kind $*\to *$. Because Int has kind $*$, applying it to [] results in [Int], of kind $*$.

In general, if a type $t_{1}$ has kind $k_{1}\to k_{2}$, and type $t_{2}$ has kind $k_{1}$, then the result of the type application $t_{1}\ t_{2}$ has kind $k_{2}$.

The way kinds govern types is analogous to the way types govern values. If a function value $f$ has type $t_{1}\to t_{2}$ (that is, it is a function which accepts a $t_{1}$ and produces a $t_{2}$), and value $x$ has type $t_{1}$, then the result of the function application $f\ x$ has type $t_{2}$.