Lambda the Ultimate

Not really the PL-applicable sort of topology, but I think it will be interest to a fair few folks here: there's a PDF scan of James Munkres (2000) Topology available.

Postscript: Not anymore. I guess it was not a legitimate distribution of the text.

Postscript #2: Or maybe it does still, for some...

I've been reading about the Lambda cube type scheme of Henk Barendregt and found it interesting if a little obscure. Does anyone know of any languages that implement the "full cube" (the 8th corner of the cube). I'm familiar with Haskell but I don't think it has dependent types (axis 2 IIRC).