Lambda the Ultimate

Haskell is not not ML. Ben Rudiak-Gould, Alan Mycroft, and Simon Peyton Jones. European Symposium on Programming 2006 (ESOP'06).

We present a typed calculus IL ("intermediate language") which supports the embedding of ML-like (strict, eager) and Haskell-like (non-strict, lazy) languages, without favoring either. IL's type system includes negation (continuations), but not implication (function arrow). Within IL we find that lifted sums and products can be represented as the double negation of their unlifted counterparts. We exhibit a compilation function from IL to AM --- an abstract von Neumann machine --- which maps values of ordinary and doubly negated types to heap structures resembling those found in practical implementations of languages in the ML and Haskell families. Finally, we show that a small variation in the design of AM allows us to treat any ML value as a Haskell value at runtime without cost, and project a Haskell value onto an ML type with only the cost of a Haskell deepSeq. This suggests that IL and AM may be useful as a compilation and execution model for a new language which combines the best features of strict and non-strict functional programming.

The authors start from the claim that most of the differences between SML and Haskell are independent of evaluation order. Is it possible, they wonder, to design a hybrid language which in some way abstracts over possible evaluation orders?

This papers leaves the language design for future work, and concentrates on the implementation costs. The results seem positive, so one hopes this project will mature and end the civil war between lazy and eager functional programming...

More information on this project is likely to appear here.

Xavier Leroy's contribution to POPL'06 is Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, which describes a fairly realistic mini-compiler from a subset of C, called Cminor, to PPC assembler.

So what? It's written entirely in Coq, which pretty much makes a certified compiler for free, and all done in a particularly easy way to leverage if you want to show particular implementations correct.

He's got a resource page up with the implementation (which he calls CompCert), and some further notes.

Impossible? Had we not designed compilers, operating systems, and document editors in small teams? And had I not repeatedly experienced that an inadequate and frustrating program could be programmed from scratch in a fraction of source code used by the original design? Our brain-storming continued, with many intermissions, over several weeks, and certain shapes of a system structure slowly emerged through the haze. After some time, the preposterous decision was made: we would embark on the design of an operating system for our workstation (which happened to be much less powerful than the one used for my rectangle-pushing) from scratch.

Download the PDF edition of this classic book today!

via Heiko Wengler in the discussion forum. (Thanks!!)

Java Subtype Tests in Real-Time. Krzysztof Palacz and Jan Vitek.

Dynamic subtype tests are frequent operations in Java programs. Naive implementations can be costly in space and running time. The techniques that have been proposed to reduce these costs are either restricted in their ability to cope with dynamic class loading or may suffer from pathological performance degradation penalizing certain programming styles. We present R&B, a subtype test algorithm designed for time and space constrained environments such as Real-Time Java which require predictable running times, low space overheads and dynamic class loading. Our algorithm is constant-time, requires an average of 10.8 bytes per class of memory and has been shown to yield an average 2.5% speedup on a production virtual machine. The Real-Time Specification for Java requires dynamic scoped memory access checks on every reference assignment. We extend R&B to perform memory access checks in constant-time.

I don't recall this paper or this subject being discussed here.

Also see this paper and this presentation.

(via Lemonodor)

This looks cool.

I am not sure about the details of how these bricks are to be programmed, but from the Slashdot dicussion is seems that there is some kind of dataflow language. Even more interesting is the claim that the VM is going to be documented, so third party language developers can target this low end robotics platform.

Accelerator: simplified programming of graphics processing units for general-purpose uses via data-parallelism. David Tarditi, Sidd Puri, and Jose Oglesby.

GPUs are difficult to program for general-purpose uses. Programmers must learn graphics APIs and convert their applications to use graphics pipeline operations. We describe Accelerator, a system that simplifies the programming of GPUs for general-purpose uses. Accelerator provides a high-level data-parallel programming model as a library that is available from a conventional imperative programming language. The library translates the data-parallel operations on-the-fly to optimized GPU pixel shader code and API calls.

A library provides programmers with a new type of array, a data-parallel array. Data-parallel arrays differ from conventional arrays in two ways. First, the only operations available on them are aggregate operations over entire input arrays. The operations are a subset of those found in languages like APL. They include element-wise arithmetic and comparison operators, reductions to compute min, max, product, and sum, and transformations on entire arrays. Second, the data-parallel arrays are functional: each operation produces an entirely new data-parallel array.

Module Mania: A Type-Safe, Separately Compiled, Extensible Interpreter

To illustrate the utility of a powerful modules language, this paper presents the embedded interpreter Lua-ML. The interpreter combines extensibility and separate compilation without compromising type safety. Its types are extended by applying a sum constructor to built-in types and to extensions, then tying a recursive knot using a two-level type; the sum constructor is written using an ML functor. The initial basis is extended by composing initialization functions from individual extensions, also using ML functors.

This is an excellent example of how the ML module language doesn't merely provide encapsulation but also strictly adds expressive power. It also demonstrates how a dynamic language (Lua) can be embedded in the statically-typed context of ML. Finally, it demonstrates that none of this need come at the expense of separate compilation or extensibility. Norman Ramsey's work is always highly recommended.

Classic Java

This collection is an implementation of (most of) ClassicJava, as defined
in "A Programmer's Reduction Semantics for Classes and Mixins," by Matthew
Flatt, Shriram Krishnamurthi, and Matthias Felleisen; in _Formal Syntax and
Semantics of Java_, Springer-Verlag LNCS 1523, pp. 241-269, 1999. A
tech-report version of the paper is also available at
<http://www.ccs.neu.edu/scheme/pubs/#tr97-293. The implementation is
written in PLT Redex, also available through PLaneT. Please consult that
package's documentation for further details.

This might be interesting to folks curious about how to formalize a real language, or about how PLT Redex works in practice.

There's a neat thread about strong normalization happening on The Types Forum.

If you've ever wondered Why is it useful to have {type systems,reductions,operations,...} that always terminate? this may Illuminate you.
Here are some snippets to give you a feel for the discussion:

I think it is clearer to split Gérard's original question in two:

1. Is strong normalization useful for programming languages ?
2. Is the proof of strong normalization via type systems applicable for programming languages?

-- François-Régis Sinot

Termination is good:

If a program is a solution to a problem then knowing that it terminates
for any input is an important aspect of it being a solution. Often the
best way to see that it is terminating is expressing it in a language
where all programs terminate. The programming language Epigram is an
example of an experimental language which is intended to be terminating
(even though not all conditions are enforced in the current version), see
http://www.e-pig.org/ for more information.

-- Thorsten Altenkirch

Termination is good!

I think the moral sense of strong normalization is that a program
in a strictly-typed language can only diverge as a result of some
programming construct, which _explicitly_ permits looping, like
iteration, recursion etc. My favourite example here is that the
"big Omega" can be written in Algol 60, because procedure types
in this language are not fully specified.

-- Pawel Urzyczyn

Termination is good and with fixpoints is turing complete?

Another way to put this is that data structures should be definable in a
strongly-normalising language so that data access, etc. is guaranteed to
terminate. Then add fixpoints or loops to describe arbitrary computations.

-- Barry Jay

Terminating reductions allows exhaustive applications of optimizations:

In a compiler, if a set of reductions is strongly normalizing, then the compiler can apply them exhaustively to an intermediate-language term without fear of looping. (We rely on this in the MLj and SML.NET compilers' "simplify" compilation phases, which apply simple reductions and directed commuting conversions until a normal form is reached. Though it has to be said that it's not the classical SN results that are relevant here, but something more specific to our intermediate language and the simplifying reductions that we employ).

-- Andrew Kenney

Rene Vestergaard also gave a link to a 2004 discussion of strong normalization on the rewriting list.

Extensible Records With Scoped Labels
Daan Leijen

Records provide a safe and flexible way to construct data structures. We describe a natural approach to typing polymorphic and extensible records that is simple, easy to use in practice, and straightforward to implement. A novel aspect of this work is that records can contain duplicate labels, effectively introducing a form of scoping over the labels. Furthermore, it is a fully orthogonal extension to existing type systems and programming languages...

Last time one of Daan's papers was mentioned, there was a very positive response (after Frank reminded us a couple of times). This is equally good: clever, elegant, and clearly presented.

(Between this and the Sheard paper, it's a good week for practical type systems...)