二階の依存型理論
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2021/09/29 03:08 UTC 版)
二階の依存型を持つ λ Π 2 {\displaystyle \lambda \Pi 2} 型システムは、 λ Π {\displaystyle \lambda \Pi } に型コンストラクタ上での量化を許容することで得られる。この型システムでは、依存積演算子は単純型付きラムダ計算の → {\displaystyle \to } 演算子とSystem Fの ∀ {\displaystyle \forall } 束縛子の両方の役割を果たす。
※この「二階の依存型理論」の解説は、「依存型」の解説の一部です。
「二階の依存型理論」を含む「依存型」の記事については、「依存型」の概要を参照ください。
- 二階の依存型理論のページへのリンク