Kind (type theory)

In the area of mathematical logic and computer science known as type theory, a kind is the type of a type constructor or, less commonly, the type of a higher-order type operator. A kind system is essentially a simply typed lambda calculus "one level up", endowed with a primitive type, denoted formula_1 and called "type", which is the kind of any data type which does not need any type parameters.
A kind is sometimes confusingly described as the "type of a (data) type", but it is actually more of an arity specifier. Syntactically, it is natural to consider polymorphic types to be type constructors, thus non-polymorphic types to be nullary type constructors. But all nullary constructors, thus all monomorphic types, have the same, simplest kind; namely formula_1.
Since higher-order type operators are uncommon in programming languages, in most programming practice, kinds are used to distinguish between data types and the types of constructors which are used to implement parametric polymorphism. Kinds appear, either explicitly or implicitly, in languages whose type systems account for parametric polymorphism in a programatically accessible way, such as C++, Haskell and Scala.
Kinds in Haskell.
The kind system of Haskell 98 includes exactly two kinds:
An inhabited type (as proper types are called in Haskell) is a type which has values. For instance, ignoring type classes which complicate the picture, codice_1 is a value of type codice_2, while codice_3 is a value of type codice_4 (list of Ints). Therefore, codice_2 and codice_4 have kind formula_1, but so does any function type, for instance codice_7 or even codice_8.
A type constructor takes one or more type arguments, and produces a data type when enough arguments are supplied, i.e. it supports partial application thanks to currying. This is how Haskell achieves parametric types. For instance, the type codice_9 (list) is a type constructor - it takes a single argument to specify the type of the elements of the list. Hence, codice_4 (list of Ints), codice_11 (list of Floats) and even codice_12 (list of lists of Ints) are valid applications of the codice_9 type constructor. Therefore, codice_9 is a type of kind formula_4. Because codice_2 has kind formula_1, applying codice_9 to it results in codice_4, of kind formula_1. The 2-tuple constructor codice_18 has kind formula_5, the 3-tuple constructor codice_19 has kind formula_17 and so on.
Kind inference.
Standard Haskell does not allow polymorphic kinds. This is in contrast to parametric polymorphism on types, which is supported in Haskell. For instance, in the following example:
data Tree z = Leaf | Fork (Tree z) (Tree z)
the kind of codice_20 could be anything, including formula_1, but also formula_4 etc. Haskell by default will always infer kinds to be formula_1, unless the type explicitly indicates otherwise (see below). Therefore the type checker will reject the following use of codice_21:
type FunnyTree = Tree [] -- invalid
because the kind of codice_9, formula_4 does not match the expected kind for codice_20, which is always formula_1.
Higher-order type operators are allowed however. For instance:
data App unt z = Z (unt z)
has kind formula_23, i.e. codice_24 is expected to be a unary data constructor, which gets applied to its argument, which must be a type, and returns another type.
GHC has the extension codice_25, which, together with codice_26, allows polymorphic kinds. For example:
data Tree (z :: k) = Leaf | Fork (Tree z) (Tree z)
type FunnyTree = Tree [] -- OK
Since GHC 8.0.1, types and kinds are merged.