依存関数
dependent function
値域が、引数に応じて変化する関数
高階多相型との関連
例
A:U という型を用いて、関数型 B: A -> U と表すと、この関数型 B は a ∈ A に対して、 B: A -> B(a) となることを表す a によって B の値域が変わるわかるようでわからｎ
A:U という型を用いて、関数型 B: A -> U と表すと、この関数型 B は a ∈ A に対して、 B: A -> B(a) となることを表す a によって B の値域が変わる