title: Code exercising the unique possibilities of each edge of the lambda calculus
body: <p>I can't explain the term <a href="http://en.wikipedia.org/wiki/Lambda_cube">lambda cube</a> much better than Wikipedia does:</p>
  
  <blockquote>
    <p>[...] 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:</p>
    
    <ul>
    <li>Terms depending on types, or polymorphism. System F, aka second order lambda calculus, is obtained by imposing only this property.</li>
    <li>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ω.</li>
    <li>Types depending on terms, or dependent types. Imposing only this property yields λΠ, a type system closely related to LF.</li>
    </ul>
    
    <p>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.</p>
  </blockquote>
  
  <p>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?</p>