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. 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 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 . 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. 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. is the kind of a unary type constructor, e.g. of a list type constructor. 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 ) is the kind of a higher-order type operator from unary type constructors to proper types. (Note: Haskell documentation uses the same arrow for both function types and kinds.) The kind system of Haskell 98 includes exactly two kinds: pronounced "type" is the kind of all data types. is the kind of a unary type constructor, which takes a type of kind and produces a type of kind .