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

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

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

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

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

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


types scala language-agnostic theory lambda-calculus
person soc    schedule 26.11.2011    source источник
comment
Возможно, это больше подходит для cstheory.stackexchange.com.   -  person    schedule 27.11.2011
comment
@Inuyasha, хотя речь явно идет о теории информатики, речь также идет о практической реализации этого в языках программирования. Я не думаю, что это вопрос исследовательского уровня в информатике, и поэтому он не относится к теории.   -  person The Archetypal Paul    schedule 27.11.2011
comment
Все эти варианты сильно нормализуются и поэтому не полны по Тьюрингу. Языки, которые вы предложили, являются завершенными по Тьюрингу, и поэтому это будет немного похоже на задачу с квадратной привязкой/круглой дырой, не так ли?   -  person Gian    schedule 02.12.2011
comment
@Джан: ??? Эти языки реализуют некоторые или части усовершенствований, упомянутых выше, в своих системах типов. Я хотел бы увидеть код, использующий эти возможности.   -  person soc    schedule 02.12.2011
comment
Я думаю, вам нужно быть более точным в отношении невозможности достижения. Эти системы в значительной степени встраивают друг друга, и, следовательно, главные свойства, по которым они различаются, — это гибкость и виды рассуждений, которые мы можем делать с терминами в этих языках. Я не уверен, как это будет отображаться на таких языках, как Java, Scala, Haskell и т. д., которые снова отличаются с точки зрения этих свойств.   -  person Gian    schedule 04.12.2011

Ответы (1)


arrow_upward
4
arrow_downward

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

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

person Toxaris    schedule 13.04.2014