Difference between revisions of "GHC/Kinds"
(→How do I use it?: remove hoopl patch) |
Iceland jack (talk | contribs) (Gender) |
||
| (8 intermediate revisions by 2 users not shown) | |||
| 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 |
+ | 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> |
||
| Line 21: | Line 21: | ||
== How do I use it? == |
== How do I use it? == |
||
| − | + | 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 |
||
| − | $ git checkout ghc-kinds |
||
| − | $ pushd utils/haddock |
||
| − | $ git checkout ghc-kinds |
||
| − | $ popd |
||
| − | $ pushd testsuite |
||
| − | $ git checkout ghc-kinds |
||
| − | $ popd |
||
| − | |||
| − | You then need to edit your <code>mk/build.mk</code> copying the <code>mk/build.mk.sample</code> file and uncommenting the line stating: |
||
| − | #BuildFlavour = quick |
||
| − | |||
| − | You can now build the compiler: |
||
| − | $ perl boot |
||
| − | $ ./configure |
||
| − | $ make |
||
| − | Or run the testsuite: |
||
| − | $ ./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:// |
+ | 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]. |
| − | + | 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] |
||
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.
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)
How do I use it?
Simply build GHC HEAD.
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]