前提
DataKindsを使ったソースコードを眺めていたら頭がわかりそうでわからないので質問します.
わからないところを説明するにあたって変なことを言っているかもしれないので,間違っていたら指摘をお願いします.
ソースコード
Nat型は0以上の整数値を表現できます.
Vector型コンストラクタは長さの型と実際にもつ情報の型を受け取ります.
Haskell
1{-# LANGUAGE DataKinds #-} 2{-# LANGUAGE GADTs #-} 3{-# LANGUAGE KindSignatures #-} 4 5data Nat 6 = Zero 7 | Succ Nat 8 9data Vector (n :: Nat) a where 10 VNil :: Vector 'Zero a 11 VCons :: a -> Vector n a -> Vector ('Succ n) a 12
考えていること
正直全くついていけないのですが,
Vectorの定義における(n :: Nat)のNatは[nがどの種なのか]を表しているのでしょうか?
- 種はいままでの知っている知識では * や * -> * のことだと思っています.
- ここでのNatも * や * -> * と同じ存在(すなわち種)という認識でいいのでしょうか?.
回答1件
あなたの回答
tips
プレビュー
バッドをするには、ログインかつ
こちらの条件を満たす必要があります。
退会済みユーザー
2019/02/22 02:31
2019/02/22 05:21 編集
退会済みユーザー
2019/02/22 16:48
2019/02/23 03:01