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 $ for package in . utils/haddock testsuite do pushd $package; git checkout ghc-kinds; popd; done
You then need to edit your
mk/build.mk copying the
mk/build.mk.sample file and uncommenting the line stating:
#BuildFlavour = quick
You can now build the compiler:
$ perl boot $ ./configure $ make
Or run the testsuite:
In both cases the resulting compiler will be located at
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]