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 (type constructor). 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 (data) type", but it is actually more of an arity specifier. Syntactically, it is natural to consider polymorphic data 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 . This is [1] essentially a stratified type theory approach, in the style of Leivant's stratified system F, [2] a predicative variant of Girard's impredicative system F.
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++, [3] Haskell, and Scala. [4] ML-polymorphism coincides with rank-1 polymorphism in Leivant's stratification, [5] thus kinds are not explicitly present in ML, although theoretical presentations of ML's type inference algorithm sometimes do use kinds. [6]
Haskell98 had mostly untyped kinds. [7] For instance, taking the usual option generics as example, it could distinguish between the kind of the constructor Maybe
of kind * -> *
and Maybe Int
(for instance) of kind *
, but the arrow was essentially the only kind constructor. Around 2010, this was approach was deemed unsatisfactory, especially with the introduction of GADTs in the language, because the untyped stratification prevented the "promotion" (or equal treatment) of kind equations on par with type equations in a GADT context. Consequently Haskell (around GHC 7.4) added "promoted datatypes", in which a type is automatically mirrored to a kind. [8] (There is a certain similarity between this concrete approach with how type schemes with no metavariables are identified with the underlying types, in certain theoretical presentation of ML's type inference algorithm, although in that context it is a mere mathematical artifice. [6] ) As this in turn introduced more ground kinds (called "datakinds") than the mere *
, kind polymorphism was added to Haskell around that time as well. [8] [9] Its proponents deemed it a resonable compromise between Haskell98 and adding full-fledged dependent types. [7]
Haskell documentation uses the same arrow for both function types and kinds.
The kind system of Haskell 98 [11] includes exactly two kinds:
An inhabited type (as proper types are called in Haskell) is a type which has values. For example, 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 , but so does any function type, for example 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. [12] [13] This is how Haskell achieves parametric types. For example, 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 . Because Int
has kind , applying []
to it results in [Int]
, of kind . The 2-tuple constructor (,)
has kind , the 3-tuple constructor (,,)
has kind and so on.
Standard Haskell does not allow polymorphic kinds, in contrast to parametric polymorphism on types, which Haskell supports. For example:
dataTreez=Leaf|Fork(Treez)(Treez)
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 (see below). Therefore the type checker will reject this use of Tree
:
typeFunnyTree=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 example:
dataAppuntz=Z(untz)
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.
Glasgow Haskell Compiler (GHC) has the extension PolyKinds
, which, together with KindSignatures
, allows polymorphic kinds. For example:
dataTree(z::k)=Leaf|Fork(Treez)(Treez)typeFunnyTree=Tree[]-- OK
Since GHC 8.0.1, types and kinds are merged. [14] Despite adding the typing rule * : *
, which would usually cause Girard's paradox, typing in the post-2012 versions of Haskell remains decidable, because the GHC typing algorithms don't rely on that rule; instead "all type equalities are witnessed by finite equality proofs, not potentially infinite reductions", according to its authors. [15]