# GHC/Kinds

### From HaskellWiki

< GHC(Difference between revisions)

(→Which data types are promotable?) |
m (→Which data types are promotable?: update link to paper) |
||

(2 intermediate revisions by one user not shown) | |||

Line 21: | Line 21: | ||

== How do I use it? == |
== How do I use it? == |
||

− | You first need to [http://hackage.haskell.org/trac/ghc/wiki/Building get the sources] and checkout the branch: |
+ | Simply [http://hackage.haskell.org/trac/ghc/wiki/Building build GHC HEAD]. |

− | |||

− | $ git clone http://darcs.haskell.org/ghc.git ghc-kinds |
||

− | $ cd ghc-kinds |
||

− | $ ./sync-all --testsuite get |
||

− | $ ./sync-all checkout ghc-kinds |
||

− | |||

− | Make sure you are up-to-date: |
||

− | |||

− | $ ./sync-all pull |
||

− | |||

− | You can now build the compiler: |
||

− | $ perl boot |
||

− | $ ./configure |
||

− | $ make |
||

− | Or run the testsuite: |
||

− | $ sh validate |
||

− | |||

− | In both cases the resulting compiler will be located at <code>inplace/bin/ghc-stage2</code>. |
||

== Which data types are promotable? == |
== 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 <hask>* -> .. * -> *</hask> which is a first-order Haskell98 type constructor. All Haskell98 data constructors of a first-order Haskell98 data type are promotable. More details can be found in [http://research.microsoft.com/en-us/people/dimitris/fc-kind-poly.pdf this paper]. |
+ | A data type is promotable if its type constructor and data constructors are. A type constructor is promotable if it is of the form <hask>* -> .. * -> *</hask> which is a first-order Haskell98 type constructor. All Haskell98 data constructors of a first-order Haskell98 data type are promotable. More details can be found in [http://dreixel.net/research/pdf/ghp.pdf this paper]. |

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

<haskell> |
<haskell> |
||

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

## Revision as of 13:18, 13 December 2011

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

## 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, he will be 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)

## 2 How do I use it?

Simply build GHC HEAD.

## 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]