代码运用lambda演算的每个边缘的独特可能性

Question

我无法解释lambda立方体这个术语比维基百科更好:

[...]λ-cube是一个框架,用于探索Coquand构造计算中的细化轴,从简单类型的lambda演算开始,作为放置在原点的立方体的顶点,以及构造的微积分(更高阶)依赖型多态lambda演算作为其完全相反的顶点.立方体的每个轴代表一种新的抽象形式:

• 术语取决于类型或多态性.系统F,又名二阶lambda演算,仅通过强加此属性获得.
• 类型取决于类型或类型运算符.简单地键入lambda-calculus与类型运算符λω,只通过强加此属性获得.与系统F结合,产生系统Fω.
• 类型取决于术语或依赖类型.仅施加此属性会产生λΠ,这是一种与LF密切相关的类型系统.

所有八个计算都包括最基本的抽象形式,术语取决于术语,普通函数与简单类型的lambda演算一样.立方体中最富有的微积分,包括所有三个抽象,是结构的微积分.所有八个结石都强烈正常化.

是否有可能在Java,Scala,Haskell,Agda,Coq等语言中找到代码示例,以便在缺少此优化的结石中无法实现每个细化？

Answer 1

是否有可能在 Java、Scala、Haskell、Agda、Coq 等语言中找到针对每个细化的代码示例，而这在缺乏这种细化的演算中是不可能实现的？

这些语言并不直接对应于 lambda 立方体中的任何系统，但是我们仍然可以通过这些语言之间的差异来举例说明 lambda 立方体中的系统之间的差异。这里有些例子：

• Agda 有依赖类型，但 Haskell 没有。所以在 Agda 中，我们可以用列表的长度来参数化列表：

  data Nat : Set where
    zero : Nat
    succ : Nat -> Nat
  
  data Vec (A : Set) : Nat -> Set where
    empty : Vec zero
    cons : (n : Nat) -> A -> Vec n -> Vec (succ n)
  

  这在 Haskell 中是不可能的。

• Scala 对类型运算符的支持比 Java 更好。所以在 Scala 中，我们可以在类型运算符上参数化类型：

  class Foo[T[_]] {
    val x: T[Int]
    val y: T[Double]
  }
  

  这在 Java 中是不可能的。

• Java 1.5 比 Java 1.4 对多态性有更好的支持。因此从 Java 1.5 开始，我们可以对类型的方法进行参数化：

  public static <A> A identity(A a) {
    return a;
  }
  

  这在 Java 1.4 中是不可能的

我认为这样的例子可以帮助理解lambda立方体，而lambda立方体可以帮助理解这些例子。但这并不意味着这些示例捕获了有关 lambda 立方体的所有信息，也不意味着 lambda 立方体捕获了这些语言之间的所有差异。