scala - 执行 lambda 演算每条边的独特可能性的代码

Question

我无法解释这个词 lambda cube比维基百科好得多:

[...] the λ-cube is a framework for exploring the axes of refinement in Coquand's calculus of constructions, starting from the simply typed lambda calculus as the vertex of a cube placed at the origin, and the calculus of constructions (higher order dependently-typed polymorphic lambda calculus) as its diametrically opposite vertex. Each axis of the cube represents a new form of abstraction:

• Terms depending on types, or polymorphism. System F, aka second order lambda calculus, is obtained by imposing only this property.
• Types depending on types, or type operators. Simply typed lambda-calculus with type operators, λω, is obtained by imposing only this property. Combined with System F it yields System Fω.
• Types depending on terms, or dependent types. Imposing only this property yields λΠ, a type system closely related to LF.

All eight calculi include the most basic form of abstraction, terms depending on terms, ordinary functions as in the simply-typed lambda calculus. The richest calculus in the cube, with all three abstractions, is the calculus of constructions. All eight calculi are strongly normalizing.

是否有可能找到 Java、Scala、Haskell、Agda、Coq 等语言中的代码示例，用于在缺乏这种细化的微积分中无法实现的每个细化？

Answer 1

Is it possible to find code examples in languages like Java, Scala, Haskell, Agda, Coq for each refinement which would be impossible to achieve in calculi lacking this refinement?

这些语言并不直接对应于 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 多维数据集涵盖了这些语言之间的所有差异。