Lambda the Ultimate

The second European Common Lisp Meeting (ECLM 2006) will be on Sunday the 30th of April in Hamburg. This is a large but informal meeting for Lispers to meet up and talk about hacking over lots of good food and beer. Last year's meeting in Amsterdam (ECLM 2005) was great!

This page has a few interesting looking papers. I stumbled here because of the paper titled "A universal characterization of the closed Euclidean interval" (PDF)*. It contains a simple categorical definition of a notion of closed
interval that has computational content.

[edit]
I want to point out the paper "Synthetic topology for data types and classical spaces" (PDF) on the above page. It describes itself roughly as "topology for computer scientists and computer science for topologists".

* The google search term I was using was actually "essential geometric morphism" which I was looking up with regards to topos theory and synthetic differential geometry.

And there's the rub: there's no way to make a Rube Goldberg language feature appear simple. Features of a programming language, whether syntactic or semantic, are all part of the language's user interface. And a user interface can handle only so much complexity or it becomes unusable.

The discussion is about multi-statement lambdas, but I don't want to discuss this specific issue. What's more interesting is the discussion of language as a user interface (an interface to what, you might ask), the underlying assumption that languages have character (e.g., Pythonicity), and the integrated view of semantics and syntax of language constructs when thinking about language usability.

I've been thinking (and reading) about dependent types and related topics (Calculus of constructions, ML type theory, and so on).

First, I'd like to say how really clear and useful I found the second chapter of ATTAPL ("Dependent Types" by Aspinall and Hofmann). Their presentation of the CoC really clarified things for me. The extra overhead of the Prf type constructor and the distinction it draws between Π-types and ∀ terms was pretty instructive to me (I'd previously seen the CoC with only λ and ∀, as it's presented here). Obviously I've hardly gotten my feet wet, but as an introduction, I highly recommend this article.

But I'm left with a question that I hope someone here can answer. I'm confused by the standard terminology for Π- and Σ-types, "dependent products" and "dependent sums," respectively. For the life of me I can't fathom what these types have to do with anything I've normally thought of as a product or a sum. The product seems to be a function type, and the sum seems (against all common sense) to be a product! And in fact, to make matters even worse, what I generally think of as a "sum" (logical disjunction or variant types) seems to be most easily defined in terms of dependent product.

I guess I'm not alone in finding this confusing. This post on the types list is relevant, but doesn't really help me understand the logic (no pun intended) behind the standard terminology, and the observation that "the dependent product type was in fact a sum type" really highlights my lack of insight.

If we were used to classical logic we would be a bit surprised here: classically, the “existential quantifier” is thought of as a generalisation of “disjunction”.

This might also be relevant (from here), but honestly I'm not even sure anymore! I really hope someone can clarify this for me, even if only from a historical perspective...

[Ehud, I'm not really sure if this kind of thing is appropriate for the front page... Any guidance?]