This section describes *data type promotion*, an extension
to the kind system that complements kind polymorphism. It is enabled by `-XDataKinds`

,
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.7, “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 `Vec`

is `* -> * -> *`

. This means
that eg. `Vec Int Char`

is a well-kinded type, even though this
is not what we intend when defining length-indexed vectors.

With `-XDataKinds`

, the example above can then be
rewritten to:

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
error.

With `-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

where `BOX`

is the (unique) sort that classifies kinds.
Note that `List`

, for instance, does not get sort
`BOX -> BOX`

, because we do not further classify kinds; all
kinds have sort `BOX`

.

The following restrictions apply to promotion:

We only promote datatypes 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 datatypes whose constructors are kind polymorphic, involve constraints, or use existential quantification.

We do not promote data family instances (Section 7.7.1, “Data families”).

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.14.1, “Syntax”), there is no way to quote a data constructor or type constructor whose second character is a single quote.

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)

Note that this requires `-XTypeOperators`

.

Numeric and string literals are prmoted to the type level, giving convenient
access to a large number of predefined type-level constants. Numeric literals
are of kind `Nat`

, while string literals are of kind
`Symbol`

. These kinds are defined in the module
`GHC.TypeLits`

.

Here is an exampe of using type-level numeric literals to provide a safe interface to a low-level function:

import GHC.TypeLits import Data.Word import Foreign newtype ArrPtr (n :: Nat) a = ArrPtr (Ptr a) clearPage :: ArrPtr 4096 Word8 -> IO () clearPage (ArrPtr p) = ...

Here is an example of using type-level string literals to simulate simple record operations:

data Label (l :: Symbol) = Get class Has a l b | a l -> b where from :: a -> Label l -> b data Point = Point Int Int deriving Show instance Has Point "x" Int where from (Point x _) _ = x instance Has Point "y" Int where from (Point _ y) _ = y example = from (Point 1 2) (Get :: Label "x")