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 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 type", but it is actually more of an arity specifier. Syntactically, it is natural to consider polymorphic types to betype constructors, thus non-polymorphic types to be nullary type constructors. But all nullary constructors, thus all monomorphic types, have the same, simplest kind; namely. 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.
Examples
, pronounced "type", is the kind of all data types seen as nullary type constructors, and also called proper types in this context. This normally includes function types in functional programming languages.
is the kind of a type constructor, e.g. of a pair type constructor, and also that of a function type constructor
is the kind of a higher-order type operator from unary type constructors to proper types.
Kinds in Haskell
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 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 . Therefore, Int and have kind, 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 applicationthanks tocurrying. This is how Haskell achieves parametric types. For instance, the type is a type constructor - it takes a single argument to specify the type of the elements of the list. Hence, , and even are valid applications of the type constructor. Therefore, is a type of kind. Because Int has kind, applying to it results in , of kind. The 2-tuple constructor has kind, the 3-tuple constructor has kind 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
the kind of z could be anything, including, but also etc. Haskell by default will always infer kinds to be, unless the type explicitly indicates otherwise. Therefore the type checker will reject the following use of Tree: type FunnyTree = Tree -- invalid
because the kind of , does not match the expected kind for z, which is always. Higher-order type operators are allowed however. For instance: data App unt z = Z
has kind, 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 = Leaf | Fork type FunnyTree = Tree -- OK
