Lambda the Ultimate

This notice comes a little late, but the latest version of OCaml, version 3.12, has been released. Surprisingly, for a point release there's a lot of interesting new language features:

Some of the highlights in release 3.12 are:

• Polymorphic recursion is supported, using explicit type declarations on the recursively-defined identifiers.
• First-class modules: module expressions can be embedded as values of the core language, then manipulated like any other first-class value, then projected back to the module level.
• New operator to modify a signature a posteriori: S with type t := tau denotes signature S where the t type component is removed and substituted by the type tau elsewhere.
• New notations for record expressions and record patterns: { lbl } as shorthand for { lbl = lbl }, and { ...; _ } marks record patterns where some labels were intentionally omitted.
• Local open let open ... in ... now supported by popular demand.
• Type variables can be bound as type parameters to functions; such types are treated like abstract types within the function body, and like type variables (possibly generalized) outside.
• The module type of construct enables to recover the module type of a given module.
• Explicit method override using the method! keyword, with associated warnings and errors.

I'm especially intrigued by first-class modules, and the destructive signature operations, both of which should make it much easier to write libraries.

Type Classes as Objects and Implicits

Type classes were originally developed in Haskell as a disciplined alternative to ad-hoc polymorphism. Type classes have been shown to provide a type-safe solution to important challenges in software engineering and programming languages such as, for example, retroactive extension of programs. They are also recognized as a good mechanism for concept-based generic programming and, more recently, have evolved into a mechanism for type-level computation. This paper presents a lightweight approach to type classes in object-oriented (OO) languages with generics using the CONCEPT pattern and implicits (a type-directed implicit parameter passing mechanism).

This paper also shows how Scala’s type system conspires with implicits to enable, and even surpass, many common extensions of the Haskell type class system, making Scala ideally suited for generic programming in the large.

Martin Odersky and team's design decisions around how to do type classes in a unified OO and FP language continue to bear fascinating fruit. Implicits look less and less like "poor man's type classes," and more and more like an improvement upon type classes, in my opinion given a quick read of this paper.

What Sequential Games, the Tychonoff Theorem, and the Double-Negation Shift have in Common, Martin Escardo and Paulo Oliva, to appear in MSFP 2010.

This is a tutorial for mathematically inclined functional programmers, based on previously published, peered reviewed theoretical work. We discuss a higher-type functional, written here in the functional programming language Haskell, which

1. optimally plays sequential games,
2. implements a computational version of the Tychonoff Theorem from topology, and
3. realizes the Double-Negation Shift from logic and proof theory.

The functional makes sense for finite and infinite (lazy) lists, and in the binary case it amounts to an operation that is available in any (strong) monad.

In fact, once we define this monad in Haskell, it turns out that this amazingly versatile functional is already available in Haskell, in the standard prelude, called sequence, which iterates this binary operation. Therefore Haskell proves that this functional is even more versatile than anticipated, as the function sequence was introduced for other purposes by the language designers, in particular the iteration of a list of monadic effects (but effects are not what we discuss here).

One of the most durable and productive analogies in semantics is the analogy between computability and continuity. Depending on how you read the history, this idea might even predate computers: Brouwer proved that all intuitonistic functions on the reals were continuous.

Over the last few years, Escardo and his collaborators have done a lot of cool stuff showing how this network of ideas can be turned into miraculous-looking little programs, so it's very nice to see a relatively accesible introduction to this work.

It has been ten years since LtU was launched. When I launched it I had no idea if anyone will read the site, let alone if people contribute new stories. The result exceeded my wildest hopes.

I got into the habit of writing a few words every year, a kind of "state of lambda" post. Somehow, this feels inappropriate for the ten year anniversary. I will possibly post something about last year later this week, but let's take a moment to celebrate our first ten years.

There are a lot of things that can be said, and a few things that perhaps should be said. I personally will say little. The thread is open.

For my part, I just want to thank all those how contributed to LtU over the years, whether by submitting new stories, by participating in the discussion, or with help with administrative and hosting issues. Some, of course, helped with any and all tasks.

It is great to see that some members that have been with LtU from its early years are still here. Some members that left have come back, and those that decided to move on to other things are still part of the ethos of LtU, as well as the archives, as we move towards the future.

Mirah is a new language from Charles Nutter, the developer of JRuby. He describes it thus:

Mirah is ... a repurposing of Ruby’s syntax to a flexible toolchain suitable for compiling to any number of type systems and runtimes with maximum performance.

Mirah’s design is centered around a few simple principals:

• Platform-agnostic
• Free from concrete decisions about the back-end type system
• Code generation, or other details are specified by the outward language

I think Mirah is a bit too new to make a front-page post. It is interesting and also puzzling in that it doesn't really define a semantics. E.g. “roughly similar scripts could conceivably compile to any number of type systems and runtimes. In this sense, Mirah is more of a rough coupling of Ruby-like syntax with a pluggable type-inference and compilation pipeline.” Can you actually claim you've created a language if the semantics of the language aren't specified? I'm not sure whether to file this under interesting or quackers.

Scribble: Closing the Book on Ad Hoc Documentation Tools. Matthew Flatt, Eli Barzilay, and Robert Bruce Findler. ICFP '09.

Scribble is a new system for writing library documentation, user guides, and tutorials. Scribble builds on PLT Scheme’s technology for language extension, and at its heart is a new approach to connecting prose references with library bindings. We have built Scribble libraries that support standalone documentation and papers, JavaDoc-style API documentation, and literate programming. Thanks in large part to Scribble’s flexibility and the ease with which we can cross-reference information across different levels, the documentation that is distributed with PLT Scheme now runs into the thousands of pages. This paper reports on the use of Scribble and on its design as both an extension and extensible part of PLT Scheme.

This introduces a cute and well thought out syntax for writing technical prose and for escaping back into the PL for typesetting operations and cross-references to PL values. It looks reminiscent of TeX, but has a direct transformation to S-expressions. Scribble also makes great use of PLT Scheme's modular and polyglot programming facilities.

A nice twist on the classic Scheme ploy:

A documentation language should be designed not by piling escape conventions on top of a comment syntax, but by removing the weaknesses and restrictions of the programming language that make a separate documentation language appear necessary. Scribble demonstrates that a small number of rules for forming documentation, with no restrictions on how they are composed, suffice to form a practical and efficient documentation language that is flexible enough to support the major documentation paradigms in use today.

(P.S. To which I'd like to add, somewhat OT, that compared to PLT Scheme, Common Lisp is starting to look teeny.)

One of the future additions to C# announced by Anders Hejlsberg in this entertaining video from 2008 is Compiler as a Service. By that he means the ability to eval code strings (and I'm guessing that this will also be integrated with C#'s built-in AST objects).

He shows this off at around minute 59, to great effect and great excitement by the audience. It feels like an inflection point. There probably won't be another REPL-less language from now on.

I predict that after that, they'll add hygienic macros and quasisyntax.

From the App Inventor about page:

To use App Inventor, you do not need to be a developer. App Inventor requires NO programming knowledge. This is because instead of writing code, you visually design the way the app looks and use blocks to specify the app's behavior.

It seems we've been here before. (and I don't just mean that it's based on Open Blocks and Kawa)

Rust is systems programming languages being developed by Mozilla. It's very preliminary work, but the list of features suggests an interesting intersection of features. I'm particularly excited by the control over memory layout that Rust gives to the programmer, but it also has massive concurrency, structural typing, and the “ability to define complex invariants that hold over data structures” in its bag of tricks.

The main developer is Graydon Hoare, with contributions from heroes-to-the-Internet Dave Herman and Brendan Eich amongst others.

Matija Pretnar, Gordon Plotkin (2009) Handlers of Algebraic Effects:

We present an algebraic treatment of exception handlers and,
more generally, introduce handlers for other computational effects repre-
sentable by an algebraic theory. These include nondeterminism, interac-
tive input/output, concurrency, state, time, and their combinations; in
all cases the computation monad is the free-model monad of the theory.
Each such handler corresponds to a model of the theory for the effects
at hand. The handling construct, which applies a handler to a compu-
tation, is based on the one introduced by Benton and Kennedy, and is
interpreted using the homomorphism induced by the universal property
of the free model. This general construct can be used to describe previ-
ously unrelated concepts from both theory and practice.

Handling a computational effect, such as raising an exception, amounts to homomorphically mapping the handled computation onto another computation. So, for example, raise is interpreted as the exception handling code given to the handler.

While encompassing both returning and non-returning handlers, this idea becomes more interesting when you start to handle the other effects, such as lookup and update. Then you can get things like state rollback when an exception occurs, and others (CSS renaming and hiding, stream redirection, timeout). Thus the semantics of handlers gives rise to a new programming construct.

If you want a gentler introduction to the subject (along with Plotkin's algebraic theory of effects and Levy's Call-by-Push-Value), try Pretnar's 2010 thesis.