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 (monomorphic) data type. A kind is sometimes confusingly described as the "type of a (data) type", but this is a triviality, unless one considers polymorphic types 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 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 with complex type systems, such as Haskell and Scala.
Read more about Kind (type Theory): Examples, Kinds in Haskell, See Also, References
Famous quotes containing the word kind:
“We want our children to become warm, decent human beings who reach out generously to those in need. We hope they find values and ideals to give their lives purpose so they contribute to the world and make it a better place because they have lived in it. Intelligence, success, and high achievement are worthy goals, but they mean nothing if our children are not basically kind and loving people.”
—Neil Kurshan (20th century)