我无法解释这个词 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 等语言中的代码示例,用于在缺乏这种细化的微积分中无法实现的每个细化?
最佳答案
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 多维数据集中的系统之间的差异。这里有些例子:
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 中是不可能的。
class Foo[T[_]] {
val x: T[Int]
val y: T[Double]
}
这在 Java 中是不可能的。
public static <A> A identity(A a) {
return a;
}
这在 Java 1.4 中是不可能的
我认为这样的例子可以帮助理解 lambda 多维数据集,而 lambda 多维数据集可以帮助理解这些例子。但这并不意味着这些示例涵盖了有关 lambda 多维数据集的所有知识,或者 lambda 多维数据集涵盖了这些语言之间的所有差异。
关于scala - 执行 lambda 演算每条边的独特可能性的代码,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/8282479/