DataKinds
GHC v7.4.1で入った
data Nat = Zero | Succ Natのような型を定義したとき
普通は値コンストラクタZero, Succのkindは定義されていない DataKindsを用いると
型→kindと昇格されるので、型がkindとして表示される
値→型と昇格されるので、値のkindを調べることができる
code:hs
{-# LANGUAGE DataKinds #-} data Nat = Zero | Succ Nat
table:こう変わる
before after
:k Nat * *
:k Succ error Nat -> Nat ここが変わる
:k Zero error Nat ここが変わる
:t Nat error error
:t Succ Nat -> Nat Nat -> Nat
:t Zero Nat Nat
DataKindsを使うと以下の3つが新たに暗黙に定義されている
kindとしてのNat
型コンストラクタとしてのSucc
型コンストラクタとしてのZero
こうなると、元の世界のNat, Succ, Zeroと名前が被ってしまう
しかし文脈(書く場所)で区別できるので、推論されるため特に気にする必要はない
しかし人間にとってわかりやすくする為に、新しく定義された方は、頭に'を付けて明示もできる
e.g. 'Succ, 'Zero
kindとしてのNatは、'Natと書いても同じ意味だが、人間が書くことはないのであまりその表記はされないと思うmrsekut.icon
上の表のghciの出力結果はわざわざ'を付けないためやや分かりづらい
上の表をこれを区別して書くと
table:こう変わる
after
:k Nat *
:k 'Succ 'Nat -> 'Nat
:k 'Zero 'Nat
:t Nat error
:t Succ Nat -> Nat
:t Zero Nat
昇格されたとて、'Succや'Zeroは具体型ではないことに注意
具体型はkindが*になるので
'がないと区別できないパターン
data Hoge a = Hoge aのような型を定義した場合に、
値コンストラクタの方(右辺)のHogeから生成される型コンストラクタのkindは、'がないと区別できない
code:ghci
:k Hoge
Hoge :: * -> *
:k 'Hoge
'Hoge :: a -> Hoge a
生成されたものはこういう対応になっている
table:対応
元の世界 DataKindsの世界
kind -
型コンストラクタ kind 型コンストラクタを種へ昇格している
値コンストラクタ 型コンストラクタ 値コンストラクタを型コンストラクタへ昇格している
- 値コンストラクタ
data A a = B aというような型を定義した場合
table:data A a = B a
元の世界 DataKindsの世界
* -> * -
A a ''A a
B a 'B a
- 無
元の世界のA aのaは任意の型を表すが、DataKindsの世界のA aのaは任意のkindを表す
身近な具体例として
table:Bool = True | False
元の世界 DataKindsの世界
* -
Bool 'Bool
True 'True
- 無
だから:k 'Hogeと、:t Hogeは見た目が同じ感じの出力に鳴る
見た目が同じだけで概念は異なる
「元の世界に存在しないもの」が、「DataKinds世界の値」になっているので、
DataKinds世界の'B a型や'True型になるような値は存在しない
例えば要素数を型引数に含むVector n b型の定義 ref nには自然数型、bには要素の型を取る、ということを明示する
code:いめーじ.hs
{-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} data Nat = Zero | Succ Nat
data Vector (n :: Nat) (b :: *) = ..
:k *や:k *->*の結果が、*なのと同じように、
:k 'Natの結果も*になっても良い気もするけどならないんだねmrsekut.icon
つまり、kindの上の概念としての'Natは新たに定義はされていない
応用例
参考
シンプルでわかりやすい
丁寧だが、型と値に同じ文字列を使っていて微妙にわかりづらさ増してる気がする
じっくり読むならよい