GHC/Kinds

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

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)

How do I use it?

You first need to get the sources and checkout the branch:

 $ git clone http://darcs.haskell.org/ghc.git ghc-kinds
 $ cd ghc-kinds
 $ ./sync-all --testsuite get
 $ ./sync-all checkout ghc-kinds

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 inplace/bin/ghc-stage2.

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 * -> .. * -> * 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 the theory 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:

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