依存関数
dependent function
値域が、引数に応じて変化する関数
この様な関数の型のことを
依存関数型
や
依存直積型
と呼ぶ
高階多相型
との関連
例
A:U
という型を用いて、関数型
B: A -> U
と表すと、この関数型
B
は
a ∈ A
に対して、
B: A -> B(a)
となることを表す
a
によって
B
の値域が変わる
わかるようでわからｎ
mrsekut.icon
Idrisで依存型に触れる#5ede00ca1982700000be434e
のイメージか
https://ja.wikipedia.org/wiki/依存型
https://ncatlab.org/nlab/show/dependent+type