データ型の昇格
原文
DataKinds
7.4.1以降
データ型の種レベルへの昇格を許す．
この節では，データ型の昇格，つまり種多相を補う種システムの拡張について説明する．これはDataKindsによって実現され，TLDI 2012で発表された論文Giving Haskell a Promotionでより詳細に説明されている．
動機
標準のHaskellは豊富な型言語を持っている．型は項を分類し，多くの一般的なプログラミングミスを回避するのに役立つ．しかし，種言語は比較的単純で，通常の型(Type種)と型コンストラクタ(例えば，Type -> Type -> Type種)だけを区別する．特に型族やGADTのような高度な型システムの機能を使う場合，この単純な種システムでは不十分であり，(訳注：型言語では防げたような)単純なエラーを防ぐことができない．型レベル自然数と長さ添字付きベクトルの例を考えてみよう．
code: dp1.hs
data Ze
data Su n
data Vec :: Type -> Type -> Type where
Nil :: Vec a Ze
Cons :: a -> Vec a n -> Vec a (Su n)
Vecの種はType -> Type -> Typeである．これは，例えば，Vec Int Charのようにwell-kindedな型であれば，これが長さ添字付きベクトルを定義するときに期待しているものでなかったとしても，定義できてしまうということを意味する．
DataKindsを使えば，上記の例は，以下のように書き換えることができる．
code: dp2.hs
data Nat = Ze | Su Nat
data Vec :: Type -> Nat -> Type where
Nil :: Vec a 'Ze
Cons :: a -> Vec a n -> Vec a ('Su n)
改良されたVecの種により，Vec Int Charのようなものはill-kindedになり，GHCはエラーを吐くようになる．
概要
DataKindsを使うと，GHCは自動的にすべてのデータ型を種に，その(値)コンストラクタを型コンストラクタに昇格する．以下の型
code: dp3.hs
data Nat = Zero | Succ Nat
data List a = Nil | Cons a (List a)
data Pair a b = Pair a b
data Sum a b = L a | R b
は以下のような種と型コンストラクタに昇格される(なお，昇格されたコンストラクタの先頭には目印として'が付いている)．
code: dp4.hs
Nat :: Type
'Zero :: Nat
'Succ :: Nat -> Nat
List :: Type -> Type
'Nil :: forall k. List k
'Cons :: forall k. k -> List k -> List k
Pair :: Type -> Type -> Type
'Pair :: forall k1 k2. k1 -> k2 -> Pair k1 k2
Sum :: Type -> Type -> Type
'L :: k1 -> Sum k1 k2
'R :: k2 -> Sum k1 k2
豊富な種を持つものも含め，事実上すべてデータコンストラクタを昇格できる．この規則には2, 3の例外がある．
現時点ではデータ族のインスタンスのコンストラクタは昇格できない．完全な依存型を要求するようなデータ族を昇格するには，GHCの型理論では力不足だ．
等価制約以外を含むコンテキストを持つデータコンストラクタは昇格できない．例えば，
code: dp5.hs
data Foo :: Type -> Type where
MkFoo1 :: a ~ Int => Foo a -- promotable
MkFoo2 :: a ~~ Int => Foo a -- promotable
MkFoo3 :: Show a => Foo a -- not promotable
MkFoo1とMkFoo2は，コンテキストが等価指向の制約のみを含むため，昇格できる．しかし，MkFoo3のコンテキストには等価制約ではないShow aが含まれているため，昇格できない．
型とコンストラクタの区別
上記の例では，すべての昇格されたコンストラクタは，先頭にシングルクォーテーション'が付いている．このマークはGHCに型(コンストラクタ)の名前空間ではなくデータ(コンストラクタ)の名前空間の中で名前を探すように伝える．次の例を考えてみよう．
code: dp6.hs
data P = MkP -- 1
data Prom = P -- 2
したがって，(MkPというコンストラクタを持つ)型Pと，データコンストラクタを昇格したものである(Prom種を持つ)'Pは区別される．
便宜上，名前が明確な場合はGHCでは'を省略できる．しかし，'を使用するとコードが読みやすくなり，エラーが発生しにくくなる．したがって，GHCは-Wunticked-promoted-constructors -Wunticked-promoted-constructorsをサポートしている．これは，先頭に'を付けずに昇格されたデータコンストラクタを使用した場合に警告を表示する．
Template Haskell構文の場合と同様に，2番目の文字が'であるデータコンストラクタの前に'を付けると，GHCは混乱する．この場合は，昇格の'とデータコンストラクタの間にスペースを入れるだけでこの問題を回避できる．
code: dp7.hs
data T = A'
type S = 'A' -- ERROR: looks like a character
type R = ' A' -- OK: promoted A'
昇格されたリストとタプル
DataKindsを使うと，Haskellのリストとタプルは自然に種に昇格され，先頭に'をつける必要があるものの，型レベルで同じ便利な構文を使うことができる．
code: dp8.hs
data HList :: Type -> Type where
HNil :: HList '[]
HCons :: a -> HList t -> HList (a ': t)
data Tuple :: (Type, Type) -> Type where
Tuple :: a -> b -> Tuple '(a,b)
foo0 :: HList '[]
foo0 = HNil
foo1 :: HList 'Int
foo1 = HCons (3::Int) HNil
foo2 :: HList Int, Bool
foo2 = ...
上記のfoo2のシグニチャのように，2つ以上の要素の型レベルのリストでは，意味が明確であるため，'符を省略することができる．ただし，(foo0やfoo1のように)1つまたは0つの要素のリストの場合は，[]と[Int]の型がHaskellでは既存の意味を持つため，'が必要である．
注意
HConsの宣言では，型レベルの中置演算子(':)のためにTypeOperators拡張も必要である．
存在的なデータコンストラクタの昇格
存在的なデータコンストラクタは，適切な禁止する理由がない限り昇格されることに注意せよ．例えば，次の例を考えてみよう．
code: dp9.hs
data Ex :: Type where
MkEx :: forall a. a -> Ex
Ex型とデータコンストラクタMkExの両方が，多相種'MkEx :: forall k. k -> Exに 昇格される．やや驚くべきことに，型レベルの存在量化されたメンバを抽出するための型族を書くことができる．
code: dp10.hs
type family UnEx (ex :: Ex) :: k
type instance UnEx (MkEx x) = x
一見したところ，UnExはpoorly-kindedに見える．返り値(訳注：型族なので返り値は当然型である)の種kは引数にないので，インスタンスがすべてのkに対してkのメンバを返す必要があるようにと思われる．しかし，そうはならない．型族UnExは，種添字付き型族であり，返り値の種kは，UnExの暗黙のパラメータである．詳細な定義は次のとおりである(暗黙のパラメータは中括弧で示している)．
code: dp12.hs
type family UnEx {k :: Type} (ex :: Ex) :: k
type instance UnEx {k} (MkEx @k x) = x
したがって，インスタンスは，UnExの暗黙のパラメータがMkExの暗黙的パラメータと一致する場合にのみ動作する．実際には，kはUnExのパラメータなので，種は存在量化から抜け出しているわけではなく，上記のコードは有効である．
Trac＃7347も参照せよ．