依存型

dependent type

引数に依存してλ抽象の型が決まる

型をファーストクラスなものとして扱える

型を値と同等の扱いができる

関数の引数に型を取れる

型宣言に関数を書ける

table:対応

依存される\依存する 項 型

項 普通の関数 依存型

型 多相型 高階多相型

ユースケース

code:hs

data Matrix (row :: Nat) (col :: Nat) = ... -- 行列を’表す型

prod :: Matrix a b -> Matrix b c -> Matrix a c -- 行列同士の乗算

参考

tapl

圏論