標準のHaskellには豊かな型言語が備わっている。型は式を分類し、多くのよくあるプログラミング上の間違いを避けるのに役立つ。一方で、Haskellの種言語(訳注: kind language; 型の型の言語)は比較的単純であり、持ち上げられた型(種*)と型構築子(たとえば種* -> * -> *)と持ち上げられていない型(7.2.1. 非ボックス化型 )を区別するのみである。特に型族(7.7. 型の族)やGADT(7.4.8. 一般化代数データ型(GADT))などの高度な型システム上の機能を使う場合、この単純な種システムは不十分であり、単純な間違いを防ぐことができない。例として、型水準の自然数と、長さによって添字付けられたベクトルを考えよ。

data Ze
data Su n

data Vec :: * -> * -> * where
  Nil  :: Vec a Ze
  Cons :: a -> Vec a n -> Vec a (Su n)

Vecの種は* -> * -> *である。これば、例えばVec Int Charが正しい種を持つ型であることを意味する。しかし、これは長さによって添字付けられたベクトルを定義するという意図から外れたものである。

-XDataKindsを使うと、上の例は次のように書き直せる。

data Nat = Ze | Su Nat

data Vec :: * -> Nat -> * where
  Nil  :: Vec a Ze
  Cons :: a -> Vec a n -> Vec a (Su n)

Vecの種をこのように改善すると、Vec Int Charのようなものは今や種が間違っており、GHCはエラーを報告するだろう。

-XDataKindsを使うと、GHCは適したデータ型を全て種へと昇格させ、その(値)構築子を型構築子へと昇格させる。以下の型は、

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

以下の種と型構築子を生み出す。

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は種を分類する(唯一の)ソートである。例えばListがBOX -> BOXというソートを得ないことに注意。種はそれ以上区別されないからである。全ての種はBOXというソートを持つ。

昇格には以下の制約が適用される。

昇格があると、構築子と型が同じ名前空間を共有するので、型名が曖昧になることがある。

data P          -- 1

data Prom = P   -- 2

type T = P      -- 1か、それとも昇格した2か？

このような場合に昇格した構築子に言及したい場合、名前に引用符を前置する必要がある。

type T1 = P     -- 1

type T2 = 'P    -- 昇格した2

昇格したデータ型は名前の付いた種を生み出すことに注意。これらが曖昧になることはないので、種名に引用符を付けることは認めていない。

Template Haskell(7.16.1. 構文)の場合と同様に、二文字目が一重引用符であるようなデータ構築子や型構築子をクォートする方法はない。

Haskellのリストおよびタプル型は言語レベルで種へと昇格されており、引用符を前置する必要があるものの型水準でも同じ便利な記法が使える。

data HList :: [*] -> * where
  HNil  :: HList '[]
  HCons :: a -> HList t -> HList (a ': t)

data Tuple :: (*,*) -> * where
  Tuple :: a -> b -> Tuple '(a,b)

これは-XTypeOperatorsを必要とすることに注意。

存在的なデータ構築子は、別に禁止される理由がない限り昇格されることに注意せよ。例として、以下を考えよ。

data Ex :: * where
  MkEx :: forall a. a -> Ex

型Exとデータ構築子MkExの両方が昇格され、多相種'MkEx :: forall k. k -> Exが与えられる。やや驚くべきことに、型族を使うことで、型水準の存在的構築子からその中身を取り出すことができる。

type family UnEx (ex :: Ex) :: k
type instance UnEx (MkEx x) = x

一見すると、UnExは種がちゃんと指定されていないように見える。戻り値の種kは引数で言及されていないため、インスタンスは、あらゆるkに対してkの要素を返さねばならないように見える。しかしそうではない。UnExは、種によって添字付けられた型族であり、戻り値の種kはUnExの暗黙の引数なのである。この定義をもっと詳しくすると次のようになる。

type family UnEx (k :: BOX) (ex :: Ex) :: k
type instance UnEx k (MkEx k x) = x

よって、このインスタンスは、UnExに与えられた暗黙の引数が、MkExに与えられた暗黙の引数に等しいときにのみ使われる。kが実際にはUnExの引数であるため、この種は存在量化から抜け出しているとはみなされず、上記のコードは正当である。

Trac #7347も見よ。

型演算子は、種の水準に昇格されることがない。なぜか。*が種であり、識別子であるかのようにパースされるからである。ここで、プログラマがEither * Boolと書こうとした場合、これはEitherを*とBoolに適用しているのだろうか。それとも*をEitherとBoolに適用しているのだろうか。この窮地を回避するため、我々は型演算子を種の水準に昇格することを単に禁止する。