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, usually denoted ∗ {\displaystyle *} and called "type", which is the kind of any data type that does not need any type parameters. 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 essentially a stratified type theory approach, in the style of Leivant's stratified system F, 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++, Haskell, and Scala. ML-polymorphism coincides with rank-1 polymorphism in Leivant's stratification, 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.
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. In Cyclone, 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. Cyclone also uses kinds to separate ordinary types from lock names; locks have kind L. Furthermore, there are shareable (S) and unshareable (U) kinds. This kinding separation ensures that all data shared between threads 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.
Kinds in Haskell Haskell98 had mostly untyped kinds, thus kinds in Haskell98 are more of an arity specifier. 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 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. (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.) As this in turn introduced more ground kinds (called "datakinds") than the mere *, kind polymorphism was added to Haskell around that time as well. Its proponents deemed it a resonable compromise between Haskell98 and adding full-fledged dependent types. Haskell documentation uses the same arrow for both function types and kinds. The kind system of Haskell 98 includes exactly two kinds:
∗ {\displaystyle *} , pronounced "type" is the kind of all data types.
… excerpt ends here. Continue reading the full article.
