ウィキペディアよりもラムダキューブという用語をうまく説明できません。
[...] λ-cube は、単純に型付けされたラムダ計算を原点に配置された立方体の頂点として開始し、構成の微積分 (より高次の依存的に型付けされたポリモーフィック ラムダ計算) を正反対の頂点として使用します。立方体の各軸は、新しい形式の抽象化を表します。
- タイプに応じた用語、またはポリモーフィズム。システム F、別名 2 次ラムダ計算は、このプロパティのみを課すことによって得られます。
- 型に応じた型、または型演算子。型演算子 λω を使用した単純型付きラムダ計算は、このプロパティのみを課すことによって得られます。システム F と組み合わせると、システム Fω が得られます。
- 用語に依存する型、または依存型。このプロパティのみを課すと、LF に密接に関連する型システムである λΠ が生成されます。
8 つのすべての計算には、抽象化の最も基本的な形式、用語に依存する用語、単純型付けされたラムダ計算のような通常の関数が含まれます。3 つの抽象化をすべて備えた立方体で最も豊富な微積分は、構造の微積分です。8 つの計算はすべて、強力に正規化されています。
Java、Scala、Haskell、Agda、Coq などの言語で、この洗練されていない計算では達成できない各改良のコード例を見つけることは可能ですか?