Code exercising the unique possibilities of each edge of the lambda calculus

Question

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?

Answer 1

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.