This section describes data type promotion, an extension
to the kind system that complements kind polymorphism. It is enabled by
and described in more detail in the paper
Giving Haskell a
Promotion, which appeared at TLDI 2012.
Standard Haskell has a rich type language. Types classify terms and serve to
avoid many common programming mistakes. The kind language, however, is
relatively simple, distinguishing only lifted types (kind
type constructors (eg. kind
* -> * -> *), and unlifted
types (Section 7.2.1, “Unboxed types”). In particular when using advanced
type system features, such as type families (Section 7.7, “Type families”)
or GADTs (Section 7.4.8, “Generalised Algebraic Data Types (GADTs)”), this simple kind system is insufficient,
and fails to prevent simple errors. Consider the example of type-level natural
numbers, and length-indexed vectors:
data Ze data Su n data Vec :: * -> * -> * where Nil :: Vec a Ze Cons :: a -> Vec a n -> Vec a (Su n)
The kind of
* -> * -> *. This means
Vec Int Char is a well-kinded type, even though this
is not what we intend when defining length-indexed vectors.
-XDataKinds, the example above can then be
data Nat = Ze | Su Nat data Vec :: * -> Nat -> * where Nil :: Vec a Ze Cons :: a -> Vec a n -> Vec a (Su n)
With the improved kind of
Vec, things like
Vec Int Char are now ill-kinded, and GHC will report an
-XDataKinds, GHC automatically promotes every suitable
datatype to be a kind, and its (value) constructors to be type constructors.
The following types
data Nat = Ze | Su Nat data List a = Nil | Cons a (List a) data Pair a b = Pair a b data Sum a b = L a | R b
give rise to the following kinds and type constructors:
Nat :: BOX Ze :: Nat Su :: Nat -> Nat List k :: BOX Nil :: List k Cons :: k -> List k -> List k Pair k1 k2 :: BOX Pair :: k1 -> k2 -> Pair k1 k2 Sum k1 k2 :: BOX L :: k1 -> Sum k1 k2 R :: k2 -> Sum k1 k2
BOX is the (unique) sort that classifies kinds.
List, for instance, does not get sort
BOX -> BOX, because we do not further classify kinds; all
kinds have sort
The following restrictions apply to promotion:
data types and
but not type synonyms, or type/data families (Section 7.7, “Type families”).
We only promote types whose kinds are of the form
* -> ... -> * -> *. In particular, we do not promote
higher-kinded datatypes such as
data Fix f = In (f (Fix f)),
or datatypes whose kinds involve promoted types such as
Vec :: * -> Nat -> *.
We do not promote data constructors that are kind polymorphic, involve constraints, mention type or data families, or involve types that are not promotable.
Since constructors and types share the same namespace, with promotion you can get ambiguous type names:
data P -- 1 data Prom = P -- 2 type T = P -- 1 or promoted 2?
In these cases, if you want to refer to the promoted constructor, you should prefix its name with a quote:
type T1 = P -- 1 type T2 = 'P -- promoted 2
Note that promoted datatypes give rise to named kinds. Since these can never be ambiguous, we do not allow quotes in kind names.
Just as in the case of Template Haskell (Section 7.17.1, “Syntax”), there is no way to quote a data constructor or type constructor whose second character is a single quote.
-XDataKinds, Haskell's list and tuple types are natively promoted to kinds, and enjoy the
same convenient syntax at the type level, albeit prefixed with a quote:
data HList :: [*] -> * where HNil :: HList ' HCons :: a -> HList t -> HList (a ': t) data Tuple :: (*,*) -> * where Tuple :: a -> b -> Tuple '(a,b) foo0 :: HList ' foo0 = HNil foo1 :: HList '[Int] foo1 = HCons (3::Int) HNil foo2 :: HList [Int, Bool] foo2 = ...
(Note: the declaration for
HCons also requires
because of infix type operator
For type-level lists of two or more elements,
such as the signature of
foo2 above, the quote may be omitted because the meaning is
unambiguous. But for lists of one or zero elements (as in
foo1), the quote is required, because the types
[Int] have existing meanings in Haskell.
Note that we do promote existential data constructors that are otherwise suitable. For example, consider the following:
data Ex :: * where MkEx :: forall a. a -> Ex
Both the type
Ex and the data constructor
get promoted, with the polymorphic kind
'MkEx :: forall k. k -> Ex.
Somewhat surprisingly, you can write a type family to extract the member
of a type-level existential:
type family UnEx (ex :: Ex) :: k type instance UnEx (MkEx x) = x
At first blush,
UnEx seems poorly-kinded. The return kind
k is not mentioned in the arguments, and thus it would seem
that an instance would have to return a member of
k. However, this is not the
case. The type family
UnEx is a kind-indexed type family.
The return kind
k is an implicit parameter to
The elaborated definitions are as follows:
type family UnEx (k :: BOX) (ex :: Ex) :: k type instance UnEx k (MkEx k x) = x
Thus, the instance triggers only when the implicit parameter to
matches the implicit parameter to
is actually a parameter to
UnEx, the kind is not escaping the
existential, and the above code is valid.
See also Trac #7347.
Type operators are not promoted to the kind level. Why not? Because
* is a kind, parsed the way identifiers are. Thus, if a programmer
tried to write
Either * Bool, would it be
Bool? Or would it be
* applied to
To avoid this quagmire, we simply forbid promoting type operators to the kind level.