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

发布于 2024-12-18 13:21:59 字数 677 浏览 1 评论 0原文

我无法比维基百科更好地解释术语 lambda 立方体：

[...] λ 立方体是一个用于探索细化轴的框架 Coquand 的构造演算，从简单类型开始 lambda 演算作为放置在原点的立方体的顶点，并且构造演算（高阶依赖类型多态 lambda 演算）作为其完全相反的顶点。各轴立方体代表了一种新的抽象形式：
术语取决于类型或多态性。系统 F，又名二阶 lambda 演算，是通过仅施加此属性获得的。
类型取决于类型或类型运算符。使用类型运算符 λω 的简单类型 lambda 演算仅通过强加即可获得此属性。与系统 F 结合，产生系统 Fω。
取决于术语或依赖类型的类型。仅施加此属性会产生 λΠ，这是一种与 LF 密切相关的类型系统。
所有八个演算都包括最基本的抽象形式、术语根据术语，简单类型 lambda 中的普通函数结石。立方体中最丰富的微积分，全部三个抽象，就是构造的演算。所有八个演算都是强烈标准化。

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

原文

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

绿阴红影里的.如风往事 2024-12-25 13:21:59

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

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

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

data Nat : 设置在哪里
  零：纳特
  succ : 纳特 ->纳特

数据Vec(A：Set)：Nat→设置在哪里
  空：矢量为零
  缺点：（n：Nat）-> A-> Vecn-> Vec (succ n)

这在 Haskell 中是不可能的。

Scala 对类型运算符的支持比 Java 更好。因此，在 Scala 中，我们可以在类型运算符上参数化类型：
```
class Foo[T[_]] {
  值 x: T[Int]
  值：T[双]
}
```
这在 Java 中是不可能的。
Java 1.5 比 Java 1.4 对多态性有更好的支持。因此，从 Java 1.5 开始，我们可以对类型的方法进行参数化：
```
public static ;恒等式(A a) {
  返回一个；
}
```
这在 Java 1.4 中是不可能的

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

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?

These languages don't correspond directly to any system in the lambda cube, but we can still exemplify the difference between the systems in the lambda cube by the difference between these languages. Here are some examples:

Agda has dependent types but Haskell doesn't. So in Agda, we can parameterize lists with their length:

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)

This is not possible in Haskell.

Scala has better support for type operators than Java. So in Scala, we can parameterize a type on a type operator:
```
class Foo[T[_]] {
  val x: T[Int]
  val y: T[Double]
}
```
This is not possible in Java.
Java 1.5 has better support for polymorphism than Java 1.4. So since Java 1.5, we can parameterize a method on a type:
```
public static <A> A identity(A a) {
  return a;
}
```
This is not possible in Java 1.4

I think such examples can help to understand the lambda cube, and the lambda cube can help to understand these examples. But this doesn't mean that these examples capture everything there is to know about the lambda cube, or that the lambda cube captures all the differences between these languages.

回复收藏 0 原文

~没有更多了~