# GHC/Kinds

### From HaskellWiki

< GHC(Difference between revisions)

m (→Which data types are promotable?: update link to paper) |
Iceland jack (Talk | contribs) (Gender) |
||

Line 5: | Line 5: | ||

Haskell defines [[Kind|kinds]] as <code>κ ::= * | κ -> κ</code>. Nowadays, programmers use type-level computation more often using [[GADT|GADTs]] and [[GHC/Type families|type families]]. The need of a well-kinded type-level computation has become bigger. This extension provides a simple mechanism called ''promotion'' to populate the kind level. |
Haskell defines [[Kind|kinds]] as <code>κ ::= * | κ -> κ</code>. Nowadays, programmers use type-level computation more often using [[GADT|GADTs]] and [[GHC/Type families|type families]]. The need of a well-kinded type-level computation has become bigger. This extension provides a simple mechanism called ''promotion'' to populate the kind level. |
||

− | Each time the user defines a ''promotable'' data type at the term level, he will be able to use it at the type level too. For instance, the user can write the following example: |
+ | Each time the user defines a ''promotable'' data type at the term level they are able to use it at the type level too. For instance, the user can write the following example: |

<haskell> |
<haskell> |

## Latest revision as of 16:02, 28 February 2014

Kinds (this is not the definitive name) will be a language extension adding a kind level and some kind polymorphic support to Haskell.

## [edit] 1 What does this extension do?

Haskell defines kinds as `κ ::= * | κ -> κ`

. Nowadays, programmers use type-level computation more often using GADTs and type families. The need of a well-kinded type-level computation has become bigger. This extension provides a simple mechanism called *promotion* to populate the kind level.

Each time the user defines a *promotable* data type at the term level they are able to use it at the type level too. For instance, the user can write the following example:

data Nat = Zero | Succ Nat data Vector :: * -> Nat -> * where VNil :: Vector a Zero VCons :: a -> Vector a n -> Vector a (Succ n) data List a = Nil | Cons a (List a) data HList :: List * -> * where HNil :: HList Nil HCons :: a -> HList as -> HList (Cons a as)

## [edit] 2 How do I use it?

Simply build GHC HEAD.

## [edit] 3 Which data types are promotable?

A data type is promotable if its type constructor and data constructors are. A type constructor is promotable if it is of the form* -> .. * -> *

A simple way to decide if your data type is promotable is to see if you can write without the where-clause like this:

data T (a::*) (b::*) (c::*) = A a | B Int b | C (Either a c) [b]