Kind (type theory)

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 ${\displaystyle *}$ 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 ${\displaystyle *}$. 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. This is useful for instance when record types (and row polymorphism) are introduced, because the record type constructor is basically a partial function; it does not allow for instance labels to be repeated. This restriction can be expressed as the row kind being parametrized by a set of labels. ^[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]

Examples

• ${\displaystyle *}$, 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.
• ${\displaystyle *\rightarrow *}$ is the kind of a unary type constructor, e.g., of a list type constructor.
• ${\displaystyle *\rightarrow *\rightarrow *}$ is the kind of a binary type constructor (via currying), e.g., of a pair type constructor, and also that of a function type constructor (not to be confused with the result of its application, which itself is a function type, thus of kind ${\displaystyle *}$)
• ${\displaystyle (*\rightarrow *)\rightarrow *}$ is the kind of a higher-order type operator from unary type constructors to proper types. ^[10]

Kinds in Haskell

Haskell documentation uses the same arrow for both function types and kinds.

The kind system of Haskell 98 ^[11] includes exactly two kinds:

• ${\displaystyle *}$, pronounced "type" is the kind of all data types.
• ${\displaystyle k_{1}\rightarrow k_{2}}$ is the kind of a unary type 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, 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 ${\displaystyle *}$, 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 ${\displaystyle *\rightarrow *}$. Because Int has kind ${\displaystyle *}$, applying [] to it results in [Int], of kind ${\displaystyle *}$. The 2-tuple constructor (,) has kind ${\displaystyle *\rightarrow *\rightarrow *}$, the 3-tuple constructor (,,) has kind ${\displaystyle *\rightarrow *\rightarrow *\rightarrow *}$ and so on.

Kind inference

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 ${\displaystyle *}$, but also ${\displaystyle *\rightarrow *}$ etc. Haskell by default will always infer kinds to be ${\displaystyle *}$, 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 [], ${\displaystyle *\rightarrow *}$ does not match the expected kind for z, which is always ${\displaystyle *}$.

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

dataAppuntz=Z(untz)

has kind ${\displaystyle (*\rightarrow *)\rightarrow *\rightarrow *}$, 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]

See also

• System F-omega
• Pure type system

References

• Pierce, Benjamin (2002). Types and Programming Languages . MIT Press. ISBN   0-262-16209-1., chapter 29, "Type Operators and Kinding"

1. Mangin, Cyprien; Sozeau, Matthieu (2015). "Equations for Hereditary Substitution in Leivant's Predicative System F: A Case Study". Electronic Proceedings in Theoretical Computer Science. 185: 71–86. arXiv: 1508.00455 . doi:10.4204/EPTCS.185.5.
2. Leivant, Daniel (1991). "Finitely stratified polymorphism". Information and Computation. 93: 93–113. doi:10.1016/0890-5401(91)90053-5.
3. Fong, Philip W. L. (2 April 2008). "CS 115: Parametric Polymorphism: Template Functions". University of Regina. Archived from the original on 2019-09-07. Retrieved 2020-08-06.
4. "Generics of a Higher Kind" (PDF). Archived from the original (PDF) on 2012-06-10. Retrieved 2012-06-10.
5. Pistone, Paolo; Tranchini, Luca (2021). "What's Decidable about (Atomic) Polymorphism". arXiv: 2105.00748 [cs.LO].
6. François Pottier and Didier Rémy, "The Essence of ML Type Inference", chapter 10 in Advanced Topics in Types and Programming Languages, edited by Benjamin C. Pierce, MIT Press, 2005. pages 389–489. In particular see pp. 400-402 where kinds and type schemes are introduced in that presentation, and p. 466 where record types are discussed.
7. Yorgey et al., Giving Haskell a promotion, TLDI'12
8. https://arxiv.org/pdf/1610.07978 , pp. 10-11
9. This was initially as the PolyKinds extension, but was substantially revised for GHC 8 https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/poly_kinds.html#overview-of-kind-polymorphism
10. Pierce (2002), chapter 32
11. Kinds - The Haskell 98 Report
12. "Chapter 4 Declarations and Binding". Haskell 2010 Language Report. Retrieved 23 July 2012.
13. Miran, Lipovača. "Learn You a Haskell for Great Good!". Making Our Own Types and Typeclasses. Retrieved 23 July 2012.
14. "9.1. Language options — Glasgow Haskell Compiler Users Guide".
15. Weirich et al., System FC with explicit kind equality, ICFP '13