Kind (type theory)

In the area of

"one level up", endowed with a primitive type, denoted ${\displaystyle *}$ and called "type", which is the kind of any

A kind is sometimes confusingly described as the "type of a

${\displaystyle *}$

Since higher-order type operators are uncommon in

• ${\displaystyle *}$, pronounced "type", is the kind of all
  functional programming languages
  .
• ${\displaystyle *\rightarrow *}$ is the kind of a
  list type
  constructor.
• ${\displaystyle *\rightarrow *\rightarrow *}$ is the kind of a
  pair type constructor, and also that of a function type
  constructor (not to be confused with the result of its application, which itself is a function type, thus of kind ${\displaystyle *}$)
• ${\displaystyle (*\rightarrow *)\rightarrow *}$ is the kind of a higher-order type operator from unary type constructors to proper types.[3]

Kinds in Haskell

(Note: Haskell documentation uses the same arrow for both function types and kinds.)

The kind system of

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

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, 4 is a value of type Int, while [1, 2, 3] is a value of type [Int] (list of Ints). Therefore, Int and [Int] have kind ${\displaystyle *}$, but so does any function type, for instance Int -> Bool or even Int -> Int -> Bool.

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.^[5][6] 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 ${\displaystyle *\rightarrow *}$. Because Int has kind ${\displaystyle *}$, applying [] to it results in [Int], of kind ${\displaystyle *}$. The 2-tuple constructor (,) has kind ${\displaystyle *\rightarrow *\rightarrow *}$, the 3-tuple constructor (,,) has kind ${\displaystyle *\rightarrow *\rightarrow *\rightarrow *}$ 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 z could be anything, including ${\displaystyle *}$, but also ${\displaystyle *\rightarrow *}$ etc. Haskell by default will always infer kinds to be ${\displaystyle *}$, unless the type explicitly indicates otherwise (see below). Therefore the type checker will reject the following use of Tree:

type FunnyTree = Tree []     -- invalid

because the kind of [], ${\displaystyle *\rightarrow *}$ does not match the expected kind for z, which is always ${\displaystyle *}$.

Higher-order type operators are allowed however. For instance:

data App unt z = Z (unt z)

has kind ${\displaystyle (*\rightarrow *)\rightarrow *\rightarrow *}$, i.e. unt 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 PolyKinds, which, together with KindSignatures, 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.^[7]

See also

• System F-omega
• Pure type system

References