In the area ofmathematical logic andcomputer science known astype theory, akind is the type of atype constructor or, less commonly, the type of a higher-order type operator (type constructor). A kind system is essentially asimply typed lambda calculus "one level up", endowed with a primitive type, usually denoted${\displaystyle \ast }$ and called "type", which is the kind of anydata type that does not need anytype parameters.

Syntactically, it is natural to considerpolymorphicdata types to be type constructors, thus non-polymorphic types to benullary type constructors. But all nullary constructors, thus all monomorphic types, have the same, simplest kind; namely${\displaystyle \ast }$. This is^[1] essentially a stratified type theory approach, in the style of Leivant's stratified system F,^[2] a predicative variant ofGirard's impredicativesystem F.

Since higher-order type operators are uncommon inprogramming languages, in most programming practice, kinds are used to distinguish between data types and the types of constructors which are used to implementparametric polymorphism. Kinds appear, either explicitly or implicitly, in languages whose type systems account for parametric polymorphism in a programmatically accessible way, such asC++,^[3]Haskell, andScala.^[4] ML-polymorphism coincides with rank-1 polymorphism in Leivant's stratification,^[5] thus kinds are not explicitly present inML, although theoretical presentations ofML's type inference algorithm sometimes do use kinds. This is useful for instance when record types (androw polymorphism) are introduced, because the recordtype constructor is basically apartial function; it does not allow for instance labels to be repeated. This restriction can be expressed as the row kind being parametrized by aset of labels.^[6]

• ${\displaystyle \ast }$, pronounced "type", is the kind of alldata types seen asnullary type constructors, and also called proper types in this context. This normally includes function types infunctional programming languages.
• ${\displaystyle \ast \to \ast }$ is the kind of aunarytype constructor, e.g., of alist type constructor.
• ${\displaystyle \ast \to \ast \to \ast }$ is the kind of abinary type constructor (viacurrying), e.g., of apair type constructor, and also that of afunction type constructor (not to be confused with the result of its application, which itself is a function type, thus of kind${\displaystyle \ast }$)
• ${\displaystyle (\ast \to \ast )\to \ast }$ is the kind of a higher-order type operator from unary type constructors to proper types.^[7]
• InCyclone,boxed types have kind B, while unboxed types have kind A (for "any") and there is a subkinding relationship between B and A, B≤A.^[8]
• Cyclone also uses kinds to separate ordinary types fromlock names; locks have kind L. Furthermore, there are shareable (S) and unshareable (U) kinds. This kinding separation ensures that all data shared betweenthreads uses locking. (This results in a "necessarily conservative"data race prevention discipline, which does prevent some race-free programs from type checking.) More precisely, combined with the previous example, that results in the sub-kidding relationships: BS≤BU, AS≤AU, BS≤AS, BU≤AU, and BS≤AU in Cyclone. B and A are, in fact, short-hand for BU and AU.^[9]

Haskell98 had mostly untyped kinds, thus kinds in Haskell98 are more of anarity specifier.^[10] For instance, taking the usualoption generics as example, it could distinguish between the kind of the constructorMaybe of kind* -> * andMaybe 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 ofGADTs 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.^[11](There is a certain similarity between this concrete approach with how typeschemes with nometavariables 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.^[11][12] Its proponents deemed it a resonable compromise between Haskell98 and adding full-fledgeddependent types.^[10]

Haskell documentation uses the same arrow for both functiontypes andkinds.

The kind system ofHaskell 98^[13] includes exactly two kinds:

• ${\displaystyle \ast }$, pronounced "type" is the kind of alldata types.
• ${\displaystyle k_1\to k_2}$ is the kind of aunarytype 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 example, ignoringtype classes which complicate the picture,4 is a value of typeInt, while[1, 2, 3] is a value of type[Int] (list of Ints). Therefore,Int and[Int] have kind${\displaystyle \ast }$, but so does any function type, for exampleInt -> Bool or evenInt -> Int -> Bool.

A type constructor takes one or more type arguments, and produces a data type when enough arguments are supplied, i.e. it supportspartial application thanks to currying.^[14][15] 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${\displaystyle \ast \to \ast }$. BecauseInt has kind${\displaystyle \ast }$, applying[] to it results in[Int], of kind${\displaystyle \ast }$. The 2-tuple constructor(,) has kind${\displaystyle \ast \to \ast \to \ast }$, the 3-tuple constructor(,,) has kind${\displaystyle \ast \to \ast \to \ast \to \ast }$ and so on.

Standard Haskell does not allowpolymorphic kinds, in contrast toparametric polymorphism on types, which Haskell supports. For example:

dataTreez=Leaf|Fork(Treez)(Treez)

the kind ofz could be anything, including${\displaystyle \ast }$, but also${\displaystyle \ast \to \ast }$ etc. Haskell by default will always infer kinds to be${\displaystyle \ast }$, unless the type explicitly indicates otherwise (see below). Therefore the type checker will reject this use ofTree:

typeFunnyTree=Tree[]-- invalid

because the kind of[],${\displaystyle \ast \to \ast }$ does not match the expected kind forz, which is always${\displaystyle \ast }$.

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

dataAppuntz=Z(untz)

has kind${\displaystyle (\ast \to \ast )\to \ast \to \ast }$, 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 extensionPolyKinds, which, together withKindSignatures, 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.^[16] Despite adding the typing rule* : *, which would usually causeGirard's paradox, typing in the post-2012 versions of Haskell remainsdecidable, because the GHC typing algorithms don't rely on that rule; instead "all type equalities are witnessed byfinite equality proofs, not potentially infinite reductions", according to its authors.^[17]

At the introduction ofunboxed types in GHC, these were abstracted to the# kind, different from the* kind of boxed types. And there was no subkinding relation between the two, meaning for instance that a partially applied polymorphic function, which was always inferred to be over boxed types, could not be applied to unboxed types. In GHC 8.2 this approach was changed to use kind polymorphism instead. There is a newTYPE constructor that is used to classify types, and the old* kind, now aliased toType is defined asTYPE LiftedRep, while a boxed type likeInt# is defined asTYPE IntRep. The argument to TYPE "is a perfectly ordinary algebraic data type, promoted to the kind level by GHC’s DataKinds extension. [...] Only TYPE is primitive in this design." Because all boxed types likeInt andBool have the same kind, they can sharecalling convention details in the compiler implementation, while the unboxed types are treated individually. The most general type of the polymorphic function constructor is henceforthTYPE r1 → TYPE r2 → Type in GHC 8. This approach is dubbed "levity polymorphism". Levity-polymorphic types cannot be inferred in GHC, only type checked. This is because the most general type for such functions is un-compilable (due to unknown calling convention details for the arguments), so the loss of principal types (for them) is inevitable.^[8]

• System F-omega
• Pure type system

• Type theory
• Data types

• Articles with short description
• Short description matches Wikidata
• Articles with example Haskell code