依存型
dependent type
値に依存している型
Vect n a の n とか、 Bool の True とか引数に依存してλ抽象の型が決まる
型をファーストクラスなものとして扱える
もしかして↑これは依存型の話ではなく、Idris特有の話 #??
型を値と同等の扱いができる
関数の引数に型を取れる
型宣言に関数を書ける
雰囲気はIdrisで依存型に触れるを参照
対応
| 依存される\依存する | 項 | 型 |
| 項 | 普通の関数 | 依存型 |
| 型 | 多相型 | 高階多相型 |
ユースケース
型レベル自然数を用いて、行列同士の乗算 ref
hsdata Matrix (row :: Nat) (col :: Nat) = ... -- 行列を’表す型
prod :: Matrix a b -> Matrix b c -> Matrix a c -- 行列同士の乗算参考
tapl
良さそう
『The Little Typer』という本がかなり評判が良いっぽい
圏論