Код, реализующий уникальные возможности каждого края лямбда-исчисления

Я не могу объяснить термин лямбда-куб намного лучше, чем Wikipedia:

[...] λ-куб является основой для изучения осей уточнения в Кокманное исчисление конструкций, начиная с простого ввода лямбда-исчисления как вершины куба, помещенного в начало координат, и исчисление конструкций (полиморфизм более строгого порядка лямбда-исчисления) как ее диаметрально противоположная вершина. Каждая ось куб представляет собой новую форму абстракции:

Условия в зависимости от типов или полиморфизма. Система F, иначе говоря, лямбда-исчисление второго порядка, получается путем наложения только этого свойства.

Типы в зависимости от типов или операторов типов. Просто типизированное лямбда-исчисление с операторами типа λω получается путем наложения только это свойство. В сочетании с системой F он дает систему Fω.

Типы, зависящие от терминов или зависимых типов. Наложение только этого свойства дает λΠ, систему типов, тесно связанную с LF.
Все восемь исчислений включают самую основную форму абстракции, термины в зависимости от терминов, обычные функции, как в просто типизированной лямбда исчисление. Богатейшее исчисление в кубе со всеми тремя абстракции, является исчислением конструкций. Все восемь исчислений сильно нормализуется.

Можно ли найти примеры кода на таких языках, как Java, Scala, Haskell, Agda, Coq для каждой доработки, которые невозможно было бы достичь в исчислениях, лишенных этой доработки?

Ответ 1

Можно ли найти примеры кода на таких языках, как Java, Scala, Haskell, Agda, Coq для каждой доработки, которые невозможно было бы достичь в исчислениях, лишенных этой доработки?

Эти языки не соответствуют непосредственно какой-либо системе в лямбда-кубе, но мы все же можем проиллюстрировать разницу между системами в лямбда-кубе по разнице между этими языками. Вот несколько примеров:

У 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

Я думаю, что такие примеры могут помочь понять лямбда-куб, а лямбда-куб поможет понять эти примеры. Но это не означает, что эти примеры охватывают все, что нужно знать о лямбда-кубе, или что лямбда-куб фиксирует все различия между этими языками.