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 only one primitive type, denoted *, and called "type", which is the kind of any data type.
| Property | Value |
|---|
| dbpprop:abstract
|
- 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 only one primitive type, denoted *, and called "type", which is the kind of any 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.
|
| dbpprop:reference
| |
| rdfs:comment
|
- 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 only one primitive type, denoted *, and called "type", which is the kind of any data type.
|
| rdfs:label
| |
| skos:subject
| |
| foaf:page
| |
![[RDF Data]](/statics/sw-cube.png)
