In the area of mathematical logic

Mathematical logic

Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...

 and computer science

Computer science

Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...

 known as type theory

Type theory

In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...

, a kind is the type of a type constructor

Type constructor

In the area of mathematical logic and computer science known as type theory, a type constructor is a feature of a typed formal language that builds new types from old. Typical type constructors encountered are product types, function types, power types and list types. Basic types are considered...

 or, less commonly, the type of a higher-order type operator. A kind system is essentially a simply typed lambda calculus

Simply typed lambda calculus

The simply typed lambda calculus , a formof type theory, is a typed interpretation of the lambda calculus with only one type constructor: \to that builds function types. It is the canonical and simplest example of a typed lambda calculus...

 "one level up", endowed with a primitive type, denoted * and called "type", which is the kind of any (monomorphic

Parametric polymorphism

In programming languages and type theory, parametric polymorphism is a way to make a language more expressive, while still maintaining full static type-safety. Using parametric polymorphism, a function or a data type can be written generically so that it can handle values identically without...

) data type

Data type

In computer programming, a data type is a classification identifying one of various types of data, such as floating-point, integer, or Boolean, that determines the possible values for that type; the operations that can be done on values of that type; the meaning of the data; and the way values of...

.
A kind is sometimes confusingly described as the "type of a (data) type

Data type

In computer programming, a data type is a classification identifying one of various types of data, such as floating-point, integer, or Boolean, that determines the possible values for that type; the operations that can be done on values of that type; the meaning of the data; and the way values of...

", but this is a trivia

Trivia

The trivia are the three lower Artes Liberales, i.e. grammar, rhetoric and logic. These were the topics of basic education, foundational to the quadrivia of higher education, and hence the material of basic education, of interest only to undergraduates...

lity, unless one considers polymorphic types

Parametric polymorphism

In programming languages and type theory, parametric polymorphism is a way to make a language more expressive, while still maintaining full static type-safety. Using parametric polymorphism, a function or a data type can be written generically so that it can handle values identically without...

 to be data types. Syntactically, it is natural to consider polymorphic types to be type constructors, thus monomorphic 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 language

Programming language

A programming language is an artificial language designed to communicate instructions to a machine, particularly a computer. Programming languages can be used to create programs that control the behavior of a machine and/or to express algorithms precisely....

s, in most programming practice, kinds are used to distinguish between data types and the types of constructors which are used to implement parametric polymorphism

Parametric polymorphism

In programming languages and type theory, parametric polymorphism is a way to make a language more expressive, while still maintaining full static type-safety. Using parametric polymorphism, a function or a data type can be written generically so that it can handle values identically without...

. Kinds appear, either explicitly or implicitly, in languages with complex type systems, such as Haskell

Haskell (programming language)

Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the...

 and Scala.

Examples

• , pronounced "type", is the kind of all data type
  Data type
  In computer programming, a data type is a classification identifying one of various types of data, such as floating-point, integer, or Boolean, that determines the possible values for that type; the operations that can be done on values of that type; the meaning of the data; and the way values of...
  
  s 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
  Unary
  * Unary numeral system, the simplest numeral system to represent natural numbers* Unary operation, a kind of mathematical operator that has only one operand* Unary coding, an entropy encoding that represents a number n with n − 1 ones followed by a zero...
  
   type constructor
  Type constructor
  In the area of mathematical logic and computer science known as type theory, a type constructor is a feature of a typed formal language that builds new types from old. Typical type constructors encountered are product types, function types, power types and list types. Basic types are considered...
  
  , e.g. of a list type constructor.
• is the kind of a binary type constructor (via currying
  Currying
  In mathematics and computer science, currying is the technique of transforming a function that takes multiple arguments in such a way that it can be called as a chain of functions each with a single argument...
  
  ), e.g. of a pair type constructor, and also that of a function type
  Function type
  In computer science, a function type is the type of a variable or parameter to which a function has or can be assigned or the result type of a higher-order function returning a function....
  
   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. These are very seldom encountered, even in programming language theory, but see Pierce (2002), chapter 32 for an application.

Kinds in Haskell

(Note: Haskell documentation uses the same arrow for both function types and kinds; we use different arrows here for clarity. Type classes do not enter in this discussion.)

Haskell

Haskell (programming language)

Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the...

's kind system has just two rules:

• , pronounced "type" is the kind of all data type
  Data type
  In computer programming, a data type is a classification identifying one of various types of data, such as floating-point, integer, or Boolean, that determines the possible values for that type; the operations that can be done on values of that type; the meaning of the data; and the way values of...
  
  s.
• is the kind of a unary
  Unary
  * Unary numeral system, the simplest numeral system to represent natural numbers* Unary operation, a kind of mathematical operator that has only one operand* Unary coding, an entropy encoding that represents a number n with n − 1 ones followed by a zero...
  
   type constructor
  Type constructor
  In the area of mathematical logic and computer science known as type theory, a type constructor is a feature of a typed formal language that builds new types from old. Typical type constructors encountered are product types, function types, power types and list types. Basic types are considered...
  
  , which takes a type of kind and produces a type of kind .

An inhabited type (as proper types are called in Haskell) is a type which has values. For instance, ignoring type class

Type class

In computer science, a type class is a type system construct that supports ad-hoc polymorphism. This is achieved by adding constraints to type variables in parametrically polymorphic types...

es 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, for instance 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

Partial application

In computer science, partial application refers to the process of fixing a number of arguments to a function, producing another function of smaller arity...

 thanks to currying. This is how Haskell achieves parametric types. For instance, 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 it to [] results in [Int], of kind . The 2-tuple

Tuple

In mathematics and computer science, a tuple is an ordered list of elements. In set theory, an n-tuple is a sequence of n elements, where n is a positive integer. There is also one 0-tuple, an empty sequence. An n-tuple is defined inductively using the construction of an ordered pair...

 constructor has kind , the 3-tuple constructor has kind and so on.

Kind inference

Haskell does not allow polymorphic kinds. This is in contrast to parametric polymorphism

Parametric polymorphism

In programming languages and type theory, parametric polymorphism is a way to make a language more expressive, while still maintaining full static type-safety. Using parametric polymorphism, a function or a data type can be written generically so that it can handle values identically without...

on types, which is supported in Haskell. For instance, in the following example:

data Tree z = Leaf | Fork (Tree z) (Tree z)

the kind of z could be anything, including *, but also etc. Haskell always assume such kinds to be *, therefore the type checker will reject the following use of Tree:

type FunnyTree = 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 instance:

data App unt z = Z (unt z)

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.