Difference between revisions of "Kind"

From HaskellWiki
Jump to: navigation, search
m
m (Add a more complicated example (StateT))
 
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."
 
[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."
   
Ordinary types, also called ''monotypes'' or ''nullary'' type constructors, have kind <TT>*</TT>. Higher order type constructors such as <hask>Tree a</hask> have kinds of the form <TT>P -> Q</TT>, where <TT>P</TT> and <TT>Q</TT> are kinds. For instance:
+
Ordinary types, also called ''monotypes'' or ''nullary'' type constructors, have kind <TT>*</TT>. Higher order type constructors have kinds of the form <TT>P -> Q</TT>, where <TT>P</TT> and <TT>Q</TT> are kinds. For instance:
   
 
Int :: *
 
Int :: *
Line 9: Line 9:
 
[] :: * -> *
 
[] :: * -> *
 
(->) :: * -> * -> *
 
(->) :: * -> * -> *
  +
  +
A type with a more complicated kind is the [https://hackage.haskell.org/package/mtl-2.2.1/docs/Control-Monad-State-Lazy.html#t:StateT StateT monad transformer]
  +
  +
<haskell>
  +
newtype StateT s m a :: * -> (* -> *) -> * -> *
  +
</haskell>
   
 
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 [[unlifted 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 [[unlifted type]]s.

Latest revision as of 19:05, 28 September 2017

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, also called monotypes or nullary type constructors, have kind *. Higher order type constructors have kinds of the form P -> Q, where P and Q are kinds. For instance:

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

A type with a more complicated kind is the StateT monad transformer

 newtype StateT s m a :: * -> (* -> *) -> * -> *

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

See also