依存ペア型
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/09/29 03:08 UTC 版)
依存積型の双対は、依存ペア型、依存和型、あるいはΣ型と呼ばれる型である。これは余積や直和、非交和などのアナロジーである。依存和型は存在量化のモデルとして理解することもできる。依存和型は Σ ( x : A ) B ( x ) {\displaystyle \Sigma _{(x:A)}B(x)} と表記される。 依存和型は、2番目の型が1番目の値に応じて変化するペアの型を表している。したがって、もし ( a , b ) : Σ ( x : A ) B ( x ) {\displaystyle (a,b):\Sigma _{(x:A)}B(x)} ならば、 a : A {\displaystyle a:A} であり、 b : B ( a ) {\displaystyle b:B(a)} である。Bが定数関数 B ( x ) = C {\displaystyle B(x)=C} のときは、依存和型は直積型、すなわち通常の直積 A × C {\displaystyle A\times C} と一致する(型判定において一致する)。
※この「依存ペア型」の解説は、「依存型」の解説の一部です。
「依存ペア型」を含む「依存型」の記事については、「依存型」の概要を参照ください。
ウィキペディア小見出し辞書の「依存ペア型」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。
お問い合わせ。
- 依存ペア型のページへのリンク
