Difference between revisions of "Kind"
Jump to navigation
Jump to search
(Include Wikipedia introduction, which is clearer (to me) and link to TaPL) |
m (Add a more complicated example (StateT)) |
||
| (5 intermediate revisions by 3 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 |
+ | [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 have kind <TT>*</TT>. |
+ | 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 10: | Line 10: | ||
(->) :: * -> * -> * |
(->) :: * -> * -> * |
||
| + | 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> |
||
| + | |||
| ⚫ | |||
= See also = |
= See also = |
||
* [[GHC/Kinds]] |
* [[GHC/Kinds]] |
||
| + | * [https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/Kinds Kinds] on the GHC Commentary |
||
| + | * [https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/TypeType TypeType] on the GHC Commentary |
||
* [http://hackage.haskell.org/trac/ghc/wiki/IntermediateTypes#KindsareTypes Kinds ?, ??, # and (#)] |
* [http://hackage.haskell.org/trac/ghc/wiki/IntermediateTypes#KindsareTypes Kinds ?, ??, # and (#)] |
||
* [[Books#Foundations|Pierce, Benjamin. ''Types and Programming Languages'']]. |
* [[Books#Foundations|Pierce, Benjamin. ''Types and Programming Languages'']]. |
||
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
- GHC/Kinds
- Kinds on the GHC Commentary
- TypeType on the GHC Commentary
- Kinds ?, ??, # and (#)
- Pierce, Benjamin. Types and Programming Languages.