標準のHaskellには豊かな型言語が備わっている。型は式を分類し、多くのよくあるプログラミング上の間違いを避けるのに役立つ。一方で、Haskellの種言語(訳注: kind language; 型の型の言語)は比較的単純であり、持ち上げられた型(種*)と型構築子(たとえば種* -> * -> *)と持ち上げられていない型(7.2.1. 非ボックス化型 )を区別するのみである。特に型族(7.7. 型の族)やGADT(7.4.7. 一般化代数データ型(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.14.1. 構文)の場合と同様に、二文字目が一重引用符であるようなデータ構築子や型構築子をクォートする方法はない。

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

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

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

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

数値リテラルと文字列リテラルは型水準に昇格され、定義済みの大量の型水準の定数へのアクセスを容易にする。数値リテラルの種はNatであり、文字列リテラルの種はSymbolである。これらの種はGHC.TypeLitsモジュールで定義されている。

低水準の関数に安全なインタフェースを与えるために型水準の数値リテラルを使う例を示す。

import GHC.TypeLits
import Data.Word
import Foreign

newtype ArrPtr (n :: Nat) a = ArrPtr (Ptr a)

clearPage :: ArrPtr 4096 Word8 -> IO ()
clearPage (ArrPtr p) = ...

単純なレコード操作をシミュレートするために型水準の文字列リテラルを使う例を示す。

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")

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

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も見よ。