Lambda the Ultimate

We have previously mentioned these videos of a series of panel discussions that were hosted by the MIT Dynamic Languages group in 2001. I just watched them again and I thought they were great, so I'm re-posting them for people who missed them the first time around and as a reminder for anyone who'd like to watch them again.

There are three separate panels on different topics: compilation, runtime, and language design. The panelists are distinguished people mostly from the Lisp/Scheme/MIT world. These panels were a precursor to the Lightweight Languages workshop series.

The videos are in QuickTime format. To play them on Linux I used VLC. mplayer wasn't able to synchronize the audio and video.

Ivan Sutherland's famous thesis has been rereleased in a new electronic edition. This is a freely downloadable and high-quality PDF version created by Alan Blackwell and Kerry Rodden.

First-class labels for extensible rows. (draft)
Daan Leijen.
Submitted to POPL'05. (PDF, BibTeX)

Abstract: This paper describes a type system for extensible records and variants with first-class labels; labels are polymorphic and can be passed as arguments. This increases the expressiveness of conventional record calculi significantly, and we show how we can encode intersection types, closed-world overloading, type case, label selective calculi, and first-class messages. We formally motivate the need for row equality predicates to express type constraints in the presence of polymorphic labels. This naturally leads to an orthogonal treatment of unrestricted row polymorphism that can be used to express first-class patterns. Based on the theory of qualified types, we present an effective type inference algorithm and efficient compilation method. The type inference algorithm, including the discussed extensions, is fully implemented in the experimental Morrow compiler.

Always trust Daan to come up with something both elegant and practical...! However the examples involving bottom (undefined) labels left me skeptical.

The type systems thread is getting ridiculously long. Please continue the discussion here...

it's never a language designer's job to define what's a sound software engineering practice. (on the Why Are Type Systems Interesting thread)

Setting aside the discussion on static vs. dynamic type checking, I must say that I find this statement rather puzzling. Aren't PL designers suposed to make SE easier? Isn't the best way to do this to evaluate and consider SE parctices? Isn't that what happens in practice (e.g., mining patterns for language features, library building etc.)?

When I created the software engineering department on LtU I wanted it to focus on language features and language design that are directly concerned with software engineering issues. But my view is perhaps even stronger than that: I think most PL issues are ultimately about SE.

Natrually, one approach is for the language to support whatever SE practices each and every programmer or team chooses. But isn't that simply an example of one sttitude towards the best way to handle the complexity of SE?

I find it incredible that some would argue that PL designers should be agnostics when it comes to SE.

We're going to need a fabric of pervasive intermediation, and the TCP/IP of Web services -- that is, SOAP -- will enable that. But we're also going to need a whole lot of agility woven into that fabric. I want middleware that works like Indigo, but I want to program it in a language that works like Python.

Jon Udell is one of the champions of so-called dynamic languages. This item is yet another attempt to explain the importance of dynamic languages and the central role they should play in building complex networked applications.

I am sure all you guys debating static typing in the forum are going to find this worth reading (and worth debating).

Constraint-Based Type Inference for Guarded Algebraic Data Types

Quite a mouthful, but look:

Guarded algebraic data types, which subsume the concepts known in the literature as indexed types, guarded recursive datatype constructors, and phantom types, and are closely related to inductive types, have the distinguishing feature that, when typechecking a function defined by cases, every branch must be checked under different typing assumptions. This mechanism allows exploiting the presence of dynamic tests in the code to produce extra static type information.

I still have to grok this idea of "dynamic tests producing extra static type information" in its entirety, though.