Difference between revisions of "Kind"

From HaskellWiki
Jump to navigation Jump to search
m
(Include Wikipedia introduction, which is clearer (to me) and link to TaPL)
(3 intermediate revisions by 2 users not shown)
Line 1: Line 1:
  +
[http://en.wikipedia.org/wiki/Kind_%28type_theory%29 Wikipedia] says, "In 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."
'''Kinds''' classify [[type]]s. Kinds are to types and type-constructors what types are to values.
 
   
 
Ordinary types have kind <TT>*</TT>. Type constructors have kind <TT>P -> Q</TT>, where <TT>P</TT> and <TT>Q</TT> are kinds. For instance:
 
Ordinary types have kind <TT>*</TT>. Type constructors have kind <TT>P -> Q</TT>, where <TT>P</TT> and <TT>Q</TT> are kinds. For instance:
Line 11: Line 11:
   
 
In Haskell 98, <TT>*</TT> is the only '''inhabited kind''', that is, all values have types of kind <TT>*</TT>. GHC introduces another inhabited kind, <TT>#</TT>, for [[unboxed type]]s.
 
In Haskell 98, <TT>*</TT> is the only '''inhabited kind''', that is, all values have types of kind <TT>*</TT>. GHC introduces another inhabited kind, <TT>#</TT>, for [[unboxed type]]s.
  +
  +
= See also =
  +
  +
* [[GHC/Kinds]]
  +
* [http://hackage.haskell.org/trac/ghc/wiki/IntermediateTypes#KindsareTypes Kinds ?, ??, # and (#)]
  +
* [[Books#Foundations|Pierce, Benjamin. ''Types and Programming Languages'']].
  +
  +
[[Category:Language]]

Revision as of 19:44, 26 August 2012

Wikipedia says, "In 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."

Ordinary types have kind *. Type constructors have kind P -> Q, where P and Q are kinds. For instance:

Int :: *
Maybe :: * -> *
Maybe Bool :: *
a -> a :: *
[] :: * -> *
(->) :: * -> * -> *

In Haskell 98, * is the only inhabited kind, that is, all values have types of kind *. GHC introduces another inhabited kind, #, for unboxed types.

See also