Lambda the Ultimate

While teaching programming languages courses, we have discovered that an extension to PLT Scheme allows the system to accommodate both lazy and strict evaluation in the same system. Moreover, the extension is simple and transparent. Finally, the simple nature of the extension means that the resulting system provides a rich environment for both lazy and strict programs without modification.

A nice thing about this paper (aside from the fact that it uses the PLT module system) is the careful attention to the relationship between features of the language defined by the interpreter and the features of the defining language.

We justify reasoning about non-total (partial) functional languages using methods seemingly only valid for total ones; this permits "fast and loose" reasoning without actually being loose...

Functional languages satisfy many pleasing equational laws, such as curry o uncurry = id, (fst x, snd x) = x and fst(x,y) = x and many others inspired by category theory. Such laws can be used to perform very pleasant proofs of program equality... There is just one problem. In real programming languages such as Haskell and ML, they do not hold.

However, not to worry: The authors show that if two closed terms have the same semantics for total functions, they have related semantics for partial functions.

The website of Hutton's introductory Programming in Haskell book, now includes eleven powerpoint presentations covering most of the chapters in the book. Each set of slides is intended to be used for a one hour lecture.

A Concurrent Lambda Calculus with Futures

We introduce a new concurrent lambda calculus with futures, lambda(fut), to model the operational semantics of Alice, a concurrent extension of ML. lambda(fut) is a minimalist extension of the call-by-value lambda-calculus that yields the full expressiveness to define, combine, and implement a variety of standard concurrency constructs such as channels, semaphores, and ports. We present a linear type system for lambda(fut) by which the safety of such definitions and their combinations can be proved: Well-typed implementations cannot be corrupted in any well-typed context.

To all the fans of Mozart and especially Stockhausen :-)

Anyway. So, I ordered a bunch of books online including TaPL and ATTaPL so I could learn more about mysterious things like Category Theory and Type Inference and Curry-Howard Correspondence.

A rather amusing interview about Pugs, the Perl 6 implementation written in Haskell.

In short: take Scheme, remove mutations, add isolated processes with mailboxes, add message sending and receiving operations and an addressing mechanism.

Termite is a Lisp for distributed computing (PDF paper and PDF presentation), providing an Erlang like model on top of Scheme.

As the presentation says, the powerful abstraction facilities provided by Scheme made impelementing Termite rather easy and the implementation doesn't require much code.

[Edit: here's a working link for the PDF paper]

A Formulae-as-Types Interpretation of Subtractive Logic

We present a formulae-as-types interpretation of Subtractive Logic (i.e. bi-intuitionistic logic). This presentation is two-fold: we first define a very natural restriction of the lambda-μ-calculus which is closed under
reduction and whose type system is a constructive restriction of the Classical Natural Deduction. Then we extend this deduction system conservatively to Subtractive Logic. From a computational standpoint,
the resulting calculus provides a type system for first-class coroutines (a restricted form of first-class continuations).

Yet another connection between subtractive logic and control. I remember the author mentioned on LtU, but I cannot find any citations.

The results are in for the 2005 Glasgow Haskell Compiler user survey, with a summary and all the raw data. The comments were the highlight for me; see for instance Applications I use GHC for.

(Previous LtU mention)

We design and implement a library for adding backtracking computations to any Haskell monad. Inspired by logic programming, our library provides, in addition to the operations required by the MonadPlus interface, constructs for fair disjunctions, fair conjunctions, conditionals, pruning, and an expressive top-level interface. Implementing these additional constructs is well-known in models of backtracking based on streams, but not known to be possible in continuation-based models. We show that all these additional constructs can be generically and monadically realized using a single primitive which we call msplit. We present two implementations of the library: one using success and failure continuations; and the other using control operators for manipulating delimited continuations.

As you can expect from the author list, this is cool stuff. Enjoy!

A type-indexed function is a function that is defined for each member of some family of types. Haskell's type class mechanism provides open type-indexed functions, in which the indexing family can be extended at any time by defining a new type class instance. The purpose of this paper is to present TypeCase: a design pattern that allows the definition of closed type-indexed functions. It is inspired by Cheney and Hinze's work on lightweight approaches to generic programming. We generalise their techniques as a design pattern. Furthermore, we show that type-indexed functions with type-indexed types, and consequently generic functions with generic types, can also be encoded in a lightweight manner, thereby overcoming one of the main limitations of the lightweight approaches.

A new paper in a field we follow quite closely (i.e., generic programming).

The paper starts with a useful summary of important previous results, which is worth reading even if you don't plan on studying the whole paper.