GHC/Kinds
From HaskellWiki
< GHC(Difference between revisions)
(Remove the branch story) |
m (→Which data types are promotable?: update link to paper) |
||
| Line 25: | Line 25: | ||
== 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: | A simple way to decide if your data type is promotable is to see if you can write without the where-clause like this: | ||
Current revision
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* -> .. * -> *
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]
