Personal tools

GHC/Kinds

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
(→Which data types are promotable?)
(Remove the branch story)
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? ==

Revision as of 16:28, 28 November 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
* -> .. * -> *
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 this paper.

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]
Retrieved from "http://www.haskell.org/haskellwiki/GHC/Kinds"