Lambda the Ultimate

This just came up in the discussion group,

The OS team at Linspire, Inc. (formerly Lindows) would like to announce that we are standardizing on Haskell as our preferred language for core OS development

Interesting!

Tim Harris, Simon Peyton-Jones. Transactional memory with data invariants. March 2006. TRANSACT '06, to appear.

This paper introduces a mechanism for asserting invariants that are maintained by a program that uses atomic memory transactions. The idea is simple: a programmer writes check E where E is an expression that should be preserved by every atomic update for the remainder of the program’s execution. We have extended STM Haskell to dynamically evaluate check statements atomically with the user’s updates: the result is that we can identify precisely which update is the first one to break an invariant.

The STM approach is sometimes described as being "like A and I" from ACID database transactions; that is, atomic blocks provide
atomicity and isolation, but do not deal explicitly with consistency or durability. This paper attempts to include “C” as well, by showing how to define dynamically-checked data invariants that must
hold when the system is in a consistent state.

While the basic idea is straightforward, the discussion of the design decisions in section 3.5-3.7 is an interesting exploration of the design space.

The implementation technique and operational semantics are the main contributions.

Previous draft discussed here.

There are a variety of reasons why we haven’t implemented continuations in the JVM. High on the list: continuations are costly to implement, and they might reek havoc with Java SE security model. These arguments are pragmatic and a tad unsatisfying. If a feature is really important, shouldn’t we just bite the bullet?

Many here will not like the answer.

This issue was discussed here mnay time, of course, but I think it is of interest to know what the people at Sun are thinking...

Tim Bray's response is also worth checking out, if only for the sake of this sound bite: The worst AJAX apps are like bad Nineties VB.

What I find most interesting here is that the difference between yield and "inline" is this negligible, which explains why Ruby users are so enamored with the feature.

That stated, the runtime wonk in me would love for some Ruby expert out there to explain the underlying reasons why yield is so much faster than Proc.call.

I can guess, but I'd rather be told.

Don Box does some experimenting...

Typed Concurrent Programming with Logic Variables

We present a concurrent higher-order programming language called Plain and a
concomitant static type system. Plain is based on logic variables and computes
with possibly partial data structures. The data structures of Plain are procedures, cells, and records. Plain's type system features record-based subtyping, bounded existential polymorphism, and access modalities distinguishing between reading and writing.

You may want to compare this with The Oz Programming Model (OPM), which

... is a concurrent programming model subsuming higher-order functional and object-oriented programming as facets of a general model. This is particularly interesting for concurrent object-oriented programming, for which no comprehensive formal model existed until now. The model can be extended so that it can express encapsulated problem solvers generalizing the problem solving capabilities of constraint logic programming.

Another paper on OPM is The Operational Semantics of Oz.

In short, the model of Plain is based on that of Oz with the main differences being:

1. Plain statically types programs using a type system with subtyping, while Oz is latently typed.
2. Therefore Plain chooses to drop support for unification in favor of a single-assignment operation.

Jeremy Gibbons and Bruno C. d. S. Oliveira (2006). The Essence of the Iterator Pattern. Submitted for publication.

The Iterator pattern gives a clean interface for element-by-element access to a collection. Imperative iterations using the pattern have two simultaneous aspects: mapping and accumulating. Various functional iterations model one or other of these, but not both simultaneously. We argue that McBride and Paterson's idioms, and in particular the corresponding traverse operator, do exactly this, and therefore capture the essence of the Iterator pattern. We present some axioms for traversal, and illustrate with a simple example, the repmin problem.

The core of the solution is from McBride and Paterson's paper Applicative programming with effects, which wasn't posted to the home page before, but which was mentioned a couple of times in the LtU forum.

The context of this reseach is previous attempts to capture functional analogues of OOP design patterns:

Recently we have argued that pure datatype-generic maps are the functional analogue of the Iterator design pattern. It was partly while reflecting on that argument that we came to the (contradictory) position presented here.

All you guys waiting to implement zippers etc. in Ocaml can go right ahead: There's now a library implementation of delimited continuations.

In fact, there are two implementations. A native implementation in C that copies the relevant part of the interpreter's stack, and a pure Ocaml version that requires monadic style of writing code.

Transactional memory with data invariants
From the abstract:

This paper introduces a mechanism for asserting invariants that are maintained by a program that uses atomic memory transactions.
The idea is simple: the programmer write always E where E is an expression that should be preserved by every atomic update for the remainder of the program's execution. We have extended STM Haskell to dynamically check always statements atomically with the user's updates: the result is that we can identify precisely which update is the first one to break an invariant.

This seems connected to Typed Contracts for Functional Programming by Ralf Hinze, Johan Jeuring, and Andres Löh (noticed on the blog of Dominic Fox).
Maybe this year design-by-contract is the hot subject?

I haven't gotten far enough into either of these papers to have much opinion, but the motivational paragraph at the beginning of the Typed Functional Contracts paper grabbed my attention instantly, and I know I want more STM in my applications, so I look forward to a few enjoyable hours.

Ralf Hinze links to Generic Haskell II. It mentions some papers we've talked about here (generic views, typed contracts) and some new stuff (SYB analysis & extensions, polytypic type inference).

Jeremy Gibbons (2006). Design Patterns as Higher-Order Datatype-Generic Programs. Submitted for publication.

Design patterns are reusable abstractions in object-oriented software. However, using current programming languages, these elements can only be expressed extra-linguistically: as prose, pictures, and prototypes. We believe that this is not inherent in the patterns themselves, but evidence of a lack of expressivity in the languages of today. We expect that, in the languages of the future, design patterns will be expressible as reusable library code. Indeed, we claim that the languages of tomorrow will suffice; the future is not far away. The necessary features are higher-order and datatype-generic constructs; these features are already or nearly available now. We argue the case by presenting higher-order datatype-generic programs capturing ORIGAMI, a small pattern language of recursive data structures.

Last time this research was mentioned there were some concerns about the idea of executable patterns. Obviously, this approach is related to many older discussions about mining patterns for language features, frameworks as opposed to patterns and so on.

Hopefully, now that things are more explicit, we will be able to have a more in depth discussion.