30

我无法比 Wikipedia 更好地解释lambda cube一词：

[...] λ-cube 是一个框架，用于探索 Coquand 构造演算中的细化轴，从简单类型的 lambda 演算开始，作为放置在原点的立方体的顶点，以及构造演算（高阶依赖类型的多态 lambda 演算）作为其截然相反的顶点。立方体的每个轴都代表一种新的抽象形式：

  • 术语取决于类型或多态性。System F，又称二阶 lambda 演算，是通过仅施加此属性而获得的。
  • 类型取决于类型或类型运算符。仅通过强加此属性即可获得具有类型运算符 λω 的简单类型 lambda 演算。与系统 F 结合产生系统 Fω。
  • 类型取决于术语或依赖类型。仅施加此属性会产生 λΠ，这是一个与 LF 密切相关的类型系统。

所有八个演算都包括最基本的抽象形式、依赖于术语的术语、简单类型的 lambda 演算中的普通函数。立方体中最丰富的演算，包含所有三个抽象，是构造演算。所有八个结石都在强烈规范化。

是否可以为每个改进找到 Java、Scala、Haskell、Agda、Coq 等语言的代码示例，而这些改进在缺乏这种改进的微积分中是不可能实现的？

4

1 回答 1

4

是否可以为每个改进找到 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 多维数据集涵盖了这些语言之间的所有差异。

于 2014-04-13T16:04:48.303 回答