依存型
dependent type
$ \lambda\Pi
Dependent type - Wikipedia
dependent type in nLab
篩型
Dependent Types と Refinement Types の違い - SevenColoured
set-as-types (Curry-style)→
篩型
model-as-types (Church-style)→
依存型
Racket
Racket.icon
Racket 6.11で篩型(refinement type)と依存関数型(dependent function type)が安定機能に
直觀主義型理論