[Haskell] DataKinds 型と種について

Question

前提

DataKindsを使ったソースコードを眺めていたら頭がわかりそうでわからないので質問します．
わからないところを説明するにあたって変なことを言っているかもしれないので，間違っていたら指摘をお願いします．

ソースコード

Nat型は0以上の整数値を表現できます．
Vector型コンストラクタは長さの型と実際にもつ情報の型を受け取ります．

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE KindSignatures       #-}

data Nat
  = Zero
  | Succ Nat

data Vector (n :: Nat) a where
  VNil :: Vector 'Zero a
  VCons :: a -> Vector n a -> Vector ('Succ n) a

考えていること

正直全くついていけないのですが，

Vectorの定義における(n :: Nat)のNatは[nがどの種なのか]を表しているのでしょうか?

• 種はいままでの知っている知識では * や * -> * のことだと思っています．
• ここでのNatも * や * -> * と同じ存在(すなわち種)という認識でいいのでしょうか?．

Answer 1

すべてご認識の通りです。 DataKinds という拡張はまさにそのように、Natという本来であればただの型でしかないものを種として扱えるようにして、ZeroやSuccなどの、本来であればNat型の値でしかないものを「Nat種の型」として扱えるようにするためのものです。

そして、n :: Nat という表記はKindSignaturesという拡張が可能にするもので、
通常型引数の種が*になるところを、n :: Nat等のように書くことで、他の種にすることができるようにしてくれます。

Vectorの定義における(n :: Nat)のNatは[nがどの種なのか]を表しているのでしょうか?

• 種はいままでの知っている知識では * や * -> * のことだと思っています．
• ここでのNatも * や * -> * と同じ存在(すなわち種)という認識でいいのでしょうか?．

Comments

[退会済みユーザー]

回答ありがとうございます．値が型になるのはすごいですね．今思った疑問なのですが，Zeroが型ということは，Zero型の値というのは存在するのでしょうか?

[igrep]

残念ながらありません。
ZeroやSuccをラップした型(「singleton types」と呼ばれます)を作ることで、間接的に扱うことは出来ますが。
例えばNatの場合GADTsを使って、下記のように定義することで、SZeroは必ずSNat Zeroという型の値になります。（コメントの制約上、インデントがなくなってしまいます点はご容赦を）

data SNat (a :: Nat) where
SZero :: SNat 'Zero
SSucc :: SNat n -> SNat ('Succ n)

[退会済みユーザー]

ありがとうございます．こういうのをスラスラ書けるようになりたいですね．精進します．

[igrep]

一点捕捉すると、「singleton types」の定義は基本的にラップする対象の型と完全に同じような定義になるので、 http://hackage.haskell.org/package/singletons というパッケージを使って自動生成する（あるいは、よく使う型はすでに生成済みなのでそれを使う）ことが多いです。
なので、仕組みを理解するとき以外に自分で書く必要はないでしょう。