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

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

29 голосов
/ 27 ноября 2011

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

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

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

Все восемь исчислений включают в себя самую основную форму абстракции, термины, зависящие от терминов, обычные функции, как в простом типе лямбда-исчисления,Самым богатым исчислением в кубе, со всеми тремя абстракциями, является исчисление конструкций.Все восемь исчислений сильно нормализуются.

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

1 Ответ

4 голосов
/ 13 апреля 2014

Можно ли найти примеры кода на таких языках, как 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

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

...