ラムダ・キューブ
ラムダキューブ(lambda cube)
$ \rightarrow : x軸: 依存型(dependent type) $ \nearrow : z軸: 型構成子(type operator)
型演算、型オペレーター、型コンストラクタ、型構築子は同じものを指してるっぽい
λ→
λP
(→ λ→) → λP
単純型付きラムダ計算 + 依存型
$ \lambda \underline{\omega}
($ \nearrow λ→) → λP
単純型付きラムダ計算 + 型コンストラクタ
λ2
($ \uparrow λ→) → λ2
単純型付きラムダ計算 + 多相型
λω
λ2 → λω or $ \lambda \underline{\omega} → λω
単純型付きラムダ計算 + 多相型 + 型コンストラクタ
λP2
λ2 → λP2 or λP → λP2
単純型付きラムダ計算 + 依存型 + 多相型
$ λP\underline{\omega}
λP → λPω or $ \lambda \underline{\omega} → λPω
単純型付きラムダ計算 + 依存型 + 型コンストラクタ
λC
λω → λC
λP2 → λC
$ λP\underline{\omega} → λC
単純型付きラムダ計算 + 依存型 + 多相型 + 型コンストラクタ
確認用
Q. ラムダキューブ
関連
参考
メモ
調査用
Wikipedia.icon
Wikipedia.icon