DataKinds拡張を有効にすると、独自のkindを定義することができるようになります。

data Nat = Z | S Nat

通常これは「値コンストラクタZとSからなる型Nat」が定義されますが、DataKinds拡張が有効になっている場合、この型Natと値コンストラクタZ, Sが、それぞれkindと型コンストラクタに「昇格」します。すなわち、型Zと型S (n :: Nat)からなる新たなkind Natが定義されます。

例えば、長さつきリストを定義したい場合、上で定義したkind Natを利用して、以下のように書くことができます。

data List (n :: Nat) a where
  Nil :: List Z a
  (:>) :: a -> List n a -> List (S n) a

deriving instance Show a => Show (List n a)
infixr 5 :>

DataKindsが無い場合、Listの定義は以下のようになるでしょう。

data Z'
data S' n

data List' n a where
  Nil' :: List' Z' a
  (::>) :: a -> List' n a -> List' (S' n) a

deriving instance Show a => Show (List' n a)
infixr 5 ::>

これでもある程度は機能しますが、nの型が限定されていないため、以下のような関数もコンパイルを通ってしまいます。

hoge :: List' (Maybe Int) a -> List' (Maybe Int) a
hoge x = x

ところが、nのkindをNatに限定することによって、このような無意味な関数はコンパイル時に弾くことができるようになります。
実際にこのhoge関数と同様なものをList'ではなくListについて定義してみましょう。

fuga :: List (Maybe Int) a -> List (Maybe Int) a
fuga x = x

これをコンパイルしようとすると、以下のようにエラーとなります。

    The first argument of ‘List’ should have kind ‘Nat’,
      but ‘Maybe Int’ has kind ‘*’
    In the type signature for ‘fuga’:
      fuga :: List (Maybe Int) a -> List (Maybe Int) a
Failed, modules loaded: none.

このような長さ付きリストを作ることにより、以下のような型安全なheadを書くこともできるようになります。

safeHead :: List (S n) a -> a
safeHead (x :> _) = x

これを実行してみると、以下のようになります。

>>> safeHead $ 3 :> 4 :> 5 :> Nil
3
>>> safeHead Nil

<interactive>:77:10:
    Couldn't match type ‘'Z’ with ‘'S n0’
    Expected type: List ('S n0) a
      Actual type: List 'Z a
    In the first argument of ‘safeHead’, namely ‘Nil’
    In the expression: safeHead Nil

Nilに対してsafeHeadを呼ぼうとした場合、エラーになっていることが分かります。

ところで、このエラーメッセージに登場する型名をよく見てみましょう。kindがNatである型の頭に、「'」が付いていることが分かりますか?
これはDataKindsによる構文の拡張で、DataKindsによりkindと型に「昇格」した型と値コンストラクタを、昇格なしで元から存在していたkindや型と区別するためにつけられるものです。

例えば、以下のコードを見てみましょう。

data P = MkP String
data A = P

DataKindsが有効になっている状態で型Pを指定した場合、このPは「値コンストラクタMkPからなる型P」を指しているのか、「kindがAであるような唯一の型P」を指しているのかが分からなくなります。そのため、こういった場合には後者の頭に「'」をつけることによって、両者を区別することができます。

>>> :set -XDataKinds
>>> :m +Data.Data
>>> Proxy :: Proxy P    -- 前者のP
Proxy
>>> Proxy :: Proxy 'P   -- 後者のP
Proxy

もちろん、名前の被る可能性がない場合は後者のPも「P」の名前でアクセスすることができます。



しかし、ここで問題点が1つ。
以下のような型が存在したとします。

data X' = X | X'

このとき、型に昇格したほうの「X'」は元々型である「X'」と名前が被っているため、アクセスするためには頭に「'」をつける必要があります。
しかし、「'X'」と書くとパーサには文字リテラルと解釈されてしまうため、コンパイルが通りません。
そのため、こういった場合は型に昇格したほうのX'にアクセスすることはできなくなってしまいます。

あとTemplateHaskellの構文とも重複している気がするけど、これも大丈夫なのかな……??