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