2013-04-10 Cartesian product 定義 Dependent type Cartesian product, 直積 集合族 について、の元の族: が を満たすとき と(個人的に)書く。このような族の集合を、 と書き、集合族 のcartesian productと呼ぶ。つまり、 Dependent product 型理論においては、 の代わりに や が使われる。 特に、型を添字集合とする型族の直積をdependent productと呼ぶ。 id関数の型 Haskellのid関数の型の意味について、 を型の集合とすると、 選択公理 記法 参考文献 集合・位相入門 Types and Programming Languages Type Theory and Functional Programming (International Computer Science Series) Intuitionistic type theory - Wikipedia, the free encyclopedia