30

I can't explain the term lambda cube much better than Wikipedia does:

[...] 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.

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?

soc
  • 27,983
  • 20
  • 111
  • 215
  • 5
    Possible this is more suitable for http://cstheory.stackexchange.com/ –  Nov 27 '11 at 03:17
  • 5
    @Inuyasha, although it's clearly about computer science theory, it's also about the practical realisation of that in programming languages. I don't think it's "a research level question in computer science" and so doesn't belong on cstheory. – The Archetypal Paul Nov 27 '11 at 09:14
  • All these variants are strongly normalising, and are therefore *not* Turing complete. The languages you suggested *are* Turing complete, and therefore it's going to be a bit of a square-peg/round-hole task, isn't it? – Gian Dec 01 '11 at 23:10
  • @Gian: ??? Those languages implement some or parts of the refinements mentioned above in their type systems. I would like to see code using those possibilities. – soc Dec 02 '11 at 13:35
  • I think you need to be more precise about "impossible to achieve". These systems embed one another, largely, and therefore the main properties in which they differ are tractability and the kinds of reasoning we can do about terms in these languages. I' not sure how this would map to languages like Java, Scala, Haskell etc which are different yet again in terms of these properties. – Gian Dec 04 '11 at 17:37

1 Answers1

4

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.

Toxaris
  • 7,156
  • 1
  • 21
  • 37