Barendregt's Lambda Cube
In the programming
subreddit,
Alpheccar
posted a link labeled
Lambda Calculi with Types - Barendregt, with the brief
comment "Great description of the lambda cube".
IMHO, that depends on how much time you have --
that "great description" is 190 pages long!
So I added a comment
I was just looking at this stuff a week or two ago. Barendregt's 190-page
descriptions of the type systems that inhabit the vertices of the lambda cube
is indeed very detailed, thorough, and well-presented. For those not wishing
to wade through all the math, the cube's description starts in section 5; the
illustration is on page "78" (79 of the PDF, according to Preview).
Haskell heavyweights SPJ and/or Erik M named a typed intermediate language "Henk" after HB.
That (1997) paper has
a more understandable (to me, anyway) summary of the Lambda-cube than Henk B.'s
1992 compendium. Possibly a benefit of five years of hindsight.
Here is Wikipedia's brief
entry about the lambda cube. It describes the axes as
- Terms depending on types, or polymorphism (as in System F),
- Types depending on types, or type operators, and
- Types depending on terms, or dependent types (as in LF).
And here's RBJones's
nicely drawn web page illustrating Barendregt's lambda cube.
FWIW, RBJones' cube loses Barendregt's arrowheads that represent inclusion.
Those arrows clearly indicate that the upper right back corner, lambda-P-omega,
includes all of the others. Unfortunately, RBJones doesn't explain his
boxes-and-stars notation, nor does he correlate the cube's axes with
wikipedia-style understandable explanations.
On page 89, HB defines the "sorts" star and box though not in understandable
English. The SPJ/EM paper's description is better, though the concepts remain
quite abstract.
I wanted to add the reference to
TaPL
(at the end of chapter 30); add the stuff
below the <HR> here, use real lambda's and boxes, and figure out what the
heck box really means, and what SPJ/EM mean by this (near the end of section
3.3 ("Notation") of their paper):
Each ... term has a type; each type has a kind. ...
A PTS may have >3 levels.
Lambda cube PTS's have <= 3 levels,
except that there is a solitary constant "[]" (box)
at the fourth level.
Hmmm... So, if * "means" terms and [] "means" types,
that's the place where * and [] live two levels above
their referents. Or something like that, I read, but
no longer can find that statement. Will locate it later,
and hopefully be able to explain it at that time.
(I'll use "[]" to represent a box).
Here's the connections, I think: System LF has dependent types.
System LF is at (*,[]) vertex of RBJones' cube.
Omega is the most far-out, so it's gotta be type-operators,
i.e., types depending on types.
So: [] means types, * means terms, and ( X, Y ) means
Y depending on X.
So, to expand wikipedia's axes list with RBJones' notation:
- Terms depending on types, or polymorphism (as in System F),
( [], * ) ... "2" as in "second-order lambda calculus"
The vertical axis
- Types depending on types, or type operators, and
( [], [] ) ... omega or "w"
The axis that points directly away from us.
- Types depending on terms, or dependent types (as in LF).
( *, [] ) ... P
The left-to-right axis
In in section 4 of HB's paper, lambda-> is extended in three ways, to
- L2 ("second-order", aka "polymorphic"),
- L-MU ("recursive types"),
- L-INT ("intersection types" -- a variable can have two types at the same time)
L2 (Girard/Reynolds): has other names
- polymorphic typed lambda calculus
- second-order typed lambda calculus
- second-order polymorphic typed lambda calculus
- system F
12:00:26 AM
Random radio Weblog