Difference between revisions of "GHC/Kinds"
(→Which data types are promotable?) 
Iceland jack (talk  contribs) (Gender) 

(3 intermediate revisions by one other user not shown)  
Line 5:  Line 5:  
Haskell defines [[Kindkinds]] as <code>κ ::= *  κ > κ</code>. Nowadays, programmers use typelevel computation more often using [[GADTGADTs]] and [[GHC/Type familiestype families]]. The need of a wellkinded typelevel computation has become bigger. This extension provides a simple mechanism called ''promotion'' to populate the kind level. 
Haskell defines [[Kindkinds]] as <code>κ ::= *  κ > κ</code>. Nowadays, programmers use typelevel computation more often using [[GADTGADTs]] and [[GHC/Type familiestype families]]. The need of a wellkinded typelevel 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 ghckinds 

−  $ cd ghckinds 

−  $ ./syncall testsuite get 

−  $ ./syncall checkout ghckinds 

−  
−  Make sure you are uptodate: 

−  
−  $ ./syncall 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/ghcstage2</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 firstorder Haskell98 type constructor. All Haskell98 data constructors of a firstorder 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 firstorder Haskell98 type constructor. All Haskell98 data constructors of a firstorder 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 whereclause 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 typelevel computation more often using GADTs and type families. The need of a wellkinded typelevel 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 firstorder Haskell98 type constructor. All Haskell98 data constructors of a firstorder 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 whereclause like this:
data T (a::*) (b::*) (c::*) = A a  B Int b  C (Either a c) [b]