Kind (type Theory) - Kinds in Haskell

Kinds in Haskell

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

Haskell's kind system has just two rules:

• , pronounced "type" is the kind of all data types.
• is the kind of a unary type constructor, which takes a type of kind and produces a type of kind .

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 is a value of type (list of Ints). Therefore, Int and have kind, but so does any function, 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. 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, (list of Ints), (list of Floats) and even ] (list of lists of Ints) are valid applications of the type constructor. Therefore, is a type of kind . Because Int has kind, applying it to results in , of kind . The 2-tuple constructor (,) has kind, the 3-tuple constructor (,,) has kind and so on.