# Difference between revisions of "Kind"

From HaskellWiki

m (monotypes, nullary types) |
m (Add a more complicated example (StateT)) |
||

(One intermediate revision by the same user 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." |
[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'' |
+ | 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

- GHC/Kinds
- Kinds on the GHC Commentary
- TypeType on the GHC Commentary
- Kinds ?, ??, # and (#)
- Pierce, Benjamin.
*Types and Programming Languages*.