Lambda the Ultimate

Partial vectorisation of Haskell programs. Manuel M. T. Chakravarty, Roman Leshchinskiy, Simon Peyton Jones, and Gabriele Keller, Proc ACM Workshop on Declarative Aspects of Multicore Programming, San Francisco, Jan 2008.

Vectorisation for functional programs, also called the flattening transformation, relies on drastically reordering computations and restructuring the representation of data types. As a result, it only applies to the purely functional core of a fully-fledged functional language, such as Haskell or ML. A concrete implementation needs to apply vectorisation selectively and integrate vectorised with unvectorised code. This is challenging, as vectorisation alters the data representation, which must be suitably converted between vectorised and unvectorised code. In this paper, we present an approach to partial vectorisation that selectively vectorises sub-expressions and data types, and also, enables linking vectorised with unvectorised modules.

The idea is fairly simple, and utilizes conversion between vectorized and unvectorized representations of the datatypes. A formal translation scheme is provided.

Data Parallel Haskell papers are here.

Mark van Atten (2008). The Development of Intuitionistic Logic. Stanford Encyclopedia of Philosophy.

This article gives an excellent account of the development of intuitionistic logic, from its roots in Brouwer's theological metaphysics, through to its formal presentation by Heyting in 1956. The account is strong on the tensions between the subjectivist motif and the urge to formalise. Via Richard Zach.

Chris Oakasaki has a blog post about teaching functional programming using Ada. He says

Why, with excellent functional programming languages like Haskell or ML easily available, would I choose to do a functional programming project in Ada? (I CAN STILL HEAR YOU LAUGHING!) Partly because we use Ada in some courses at our institution, and I wanted a library that could help in teaching recursion to novices. But, honestly, mostly I just wanted to see if it could be done

The idea of crossing paradigms has been around awhile. SICP rather famously introduces object orientation by building it on top of Scheme.

What do you think about teaching or learning paradigm A in a language strongly oriented towards paradigm B? What's gained? What's lost?

Catch me if you can: Towards type-safe, hierarchical, lightweight, polymorphic and efficient error management in OCaml, by David Teller, Arnaud Spiwack, Till Varoquaux:

This is the year 2008 and ML-style exceptions are everywhere. Most modern languages, whether academic or industrial, feature some variant of this mechanism. Languages such as Java even have a degree of out-of-the-box static coverage-checking for such exceptions, which is currently not available for ML languages, at least not without resorting to external tools.

In this document, we demonstrate a design principle and a tiny library for managing errors in a functional manner, with static coverage-checking, automatically-inferred, structurally typed and hierarchical exceptional cases, all of this for what we believe is a reasonable run-time cost. Our work is based on OCaml and features simple uses of higher-order programming, low-level exceptions, phantom types, polymorphic variants and compile-time code
rewriting.

Exhaustively checked, user-friendly exception handling was a bit of an open problem for awhile. As the paper details, languages supported either cumbersome, exhaustively checked polymorphic exceptions, as in Haskell, or we had unchecked easily extensible monomorphic exceptions, as in ML, or we had checked, extensible exceptions using a universal type as in Java.

Supporting exhaustively checked, easily extensible polymorphic exceptions seemed quite a challenge, which this paper solves using monadic error handling and nested polymorphic variants. The paper also gives a good overview of current techniques of exception checking in OCaml, ie. ocamlexc.

The performance of such exceptions is understandably lower than native exceptions, given all the thunking and indirection that monads entail. The authors attempt various implementations and test their performance against native exceptions. Ultimately, monadic error management seems acceptable for actual error handling, but not for control flow as native exceptions are sometimes used in OCaml.

One interesting extension is to consider how efficient the implementations would be given more sophisticated control flow operators, such as continuations, coroutines, or delimited continuations, or whether native exceptions can be salvaged using a type and effects system in place of monads.

Just a quick reminder -- the 2008 ICFP Programming Contest starts tomorrow.

Functional Netlists, Sungwoo Park, Jinha Kim, Hyeonseung Im. ICFP 2008.

In efforts to overcome the complexity of the syntax and the lack of formal semantics of conventional hardware description languages, a number of functional hardware description languages have been developed. Like conventional hardware description languages, however, functional hardware description languages eventually convert all source programs into netlists, which describe wire connections in hardware circuits at the lowest level and conceal all high-level descriptions written into source programs.

We develop a variant of the lambda calculus, called l-lambda (linear lambda), which may serve as a high-level substitute for netlists. In order to support higher-order functions, l-lambda uses a linear type system which enforces the linear use of variables of function type. The translation of l-lambda into structural descriptions of hardware circuits is sound and complete in the sense that it maps expressions only to realizable hardware circuits and that every realizable hardware circuit has a corresponding expression in l-lambda. To illustrate the use of l-lambda as a high-level substitute for netlists, we design a simple hardware description language that extends l with polymorphism, and use it to implement a Fast Fourier Transform circuit.

Given the recent discussion about hardware synthesis languages, the appearance of this paper seems timely. The use of linear types is perhaps unsurprising from a technical point of view, but it's surprising when you consider how frequently and in how many different contexts they appear.

Also, one thing I don't understand: there's apparently a difference between a "hardware description language" and a "hardware synthesis language". If anyone could explain what the difference means, I'd appreciate it. :)

See the Dusty Decks announcement.

Non-Deterministic Recursive Ascent Parsing, Renee Leermakers. 1991 conference on European chapter of the Association for Computational Linguistics.

A purely functional implementation of LR-parsers is given, together with a simple correctness proof. It is presented as a generalization of the recursive descent parser. For non-LR grammars the time-complexity of our parser is cubic if the functions that constitute the parser are implemented as memo-functions, i.e. functions that memorize the results of previous invocations. Memo-functions also facilitate a simple way to construct a very compact representation of the parse forest. For LR(0) grammars, our algorithm is closely related to the recursive ascent parsers recently discovered by Kruseman Aretz [1] and Roberts [2]. Extended CF grammars (grammars with regular expressions at the right hand side) can be parsed with a simple modification of the LR-parser for normal CF grammars.

How LR parsers worked always confused me until I learned about their presentation in terms of recursive ascent.

via Jeff Newbern in the discussion forum comes the writeup from the winning entry in the MEMOCODE 2007 contest:

This year, the first MEMOCODE hardware/software codesign contest posed the following problem: optimize matrix-matrix multiplication in such a way that it is split between the FPGA and PowerPC on a Xilinx Virtex IIPro 30. In this paper we discuss our solution, which we implemented on a Xilinx XUP development board with 256 MB of DRAM. The design was done by the five authors over a span of approximately 3 weeks, though of the 15 possible man-weeks, about 9 were actually spent working on this problem. All hardware design was done using Bluespec SystemVerilog (BSV), with the exception of an imported Verilog multiplication unit, necessary only due to the limitations of the Xilinx FPGA toolflow optimizations.

Wow! This is much cooler than the kinds of programs I write :-)

This MIT/Bluespec team won the first contest at MEMOCODE 2007 and the second in MEMOCODE 2008. The results for 2008 are very interesting: The Bluespec team had the highest performance by an order of magnitude, the next fastest program was written by one guy in straight C without using the FPGA, and the rest were mostly in a hybrid of C and (V?)HDL.

Does this make Bluespec the programming tool of choice for discriminating hardware hackers?

Hardware Design and Functional Programming: a Perfect Match by Mary Sheeran, Journal of Universal Computer Science, Special issue devoted to the Brazilian Symposium on Programming Languages, 2005.

This is a slightly odd paper that explains why I am still as fascinated by the combination of functional programming and hardware design as I have ever been. It includes some looking back over my own research and that of others, and contains 60 references. It explains what kinds of research I am doing now, and why, and also presents some neat new results about parallel prefix circuits. It ends by posing lots of hard questions that we need to answer if we are to be able to design and verify circuits successfully in the future.