A kind system is essentially a simply typed lambda calculus "one level up", endowed with a primitive type, denoted
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 programmatically accessible way, such as C++,[1] Haskell and Scala.
[2] (Note: Haskell documentation uses the same arrow for both function types and kinds.)
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).
[5][6] This is how Haskell achieves parametric types.
Standard Haskell does not allow polymorphic kinds.
This is in contrast to parametric polymorphism on types, which is supported in Haskell.
Therefore the type checker will reject the following use of Tree: because the kind of [],
Higher-order type operators are allowed however.
, 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: Since GHC 8.0.1, types and kinds are merged.