Dependent Types と Refinement Types の違い - SevenColoured自分の tweets.zip をみてたら発掘された文章. Dependent Types (依存型) と Refinement Types (篩型) は目指すところは似ているが, 導入スタイルに根本的な違いがある. TL;DR Refinement types は (Curry-style typing のように) extrinsic で, Dependent types は (Church-style typing のように) intrinsic である. 前提 一般に, プログラム言語への型の導入スタイルには Curry-style と Church-style の2種類がある. Curry-style: 型付けは 既に存在する項を 分類するもの Church-style: 項が存在するとは 型付けされているということ 前者は動的型付き言語での型アノテーションなどが当てはまり, 型アノ
