Lambda the Ultimate

And Shin-Cheng Mu gives a rather accessible algebraic proof.

There's lots to say about this observation, but apart from saying I was surprised by it, I will leave comment to the comments.

Datatype-generic programs are programs that are parametrized by a datatype or type functor. There are two main styles of datatype-generic programming: the Algebra of Programming approach, characterized by structured recursion operators parametrized by a shape functor, and the Generic Haskell approach, characterized by case analysis over the structure of a datatype. We show that the former enjoys a kind of parametricity, relating the behaviours of generic functions at different types; in contrast, the latter is more ad hoc, with no coherence required or provided between the various clauses of a definition.

How could we have not mentioned this before?

The main result of this paper is that fold is a higher-order natural transformation. This means, the authors explain, that fold is a rather special kind of datatype-generic operator, both enjoying and requiring coherence between its datatype-specific instances.

We had several long discussions about the uniqueness of fold, which may serve as an introduction for those new to this sort of discussion. The tutorial on the universality of fold is, of course, on the papers page.

For some reason I feel a craving for bananas...

OCaml Light: a formal semantics for a substantial subset of the Objective Caml language.

OCaml light is a formal semantics for a substantial subset of the Objective Caml language. It is written in Ott, and it comprises a small-step operational semantics and a syntactic, non-algorithmic type system. A type soundness theorem has been proved and mechanized using the HOL-4 proof assistant, thereby ensuring that the proof is free from errors. To ensure that the operational semantics accurately models Objective Caml, an executable version of the semantics has been created (and proved equivalent in HOL to the original, relational version) and tested on a number of small test cases.

Note that while we have tried to make the semantics accurate, we are not part of the OCaml development team - this is in no sense a normative specification of the implemented language.

From a team including Peter Sewell (Acute, HashCaml, Ott).

I continue to believe that things are heating up nicely in mechanized metatheory, which, in the multicore/multiprocessor world in which we now live, is extremely good news.

Generative Code Specialisation for High-Performance Monte Carlo Simulations (Don Stewart, Hugh Chaffey-Millar, Gabriele Keller, Manuel M. T. Chakravarty and Christopher Barner-Kowollik) is a nice example of exploiting PL theory techniques (relevant keywords highlighted below) to combine a need for generality with high performance, to achieve outstanding results:

We address the tension between software generality and performance in the domain of scientific and financial simulations based on Monte-Carlo methods. To this end, we present a novel software architecture, centred around the concept of a specialising simulator generator, that combines and extends methods from generative programming, partial evaluation, runtime code generation, and dynamic code loading. The core tenet is that, given a fixed simulator configuration, a generator in a functional language can produce low-level code that is more highly optimised than a manually implemented generic simulator. We also introduce a skeleton, or template, capturing a wide range of Monte-Carlo methods and use it to explain how to design specialising simulator generators and how to generate parallelised simulators for multi-core and distributed-memory multiprocessors.

We evaluated the practical benefits and limitations of our approach by applying it to a highly relevant problem in computational chemistry. More precisely, we used a Markov-chain Monte-Carlo method for the study of advanced forms of polymerisation kinetics. The resulting implementation executes faster than all competing software products, while at the same time also being more general. The generative architecture allows us to cover a wider range of chemical reactions and to target a wider range of high-performance architectures (such as PC clusters and SMP multiprocessors).

We show that it is possible to outperform low-level languages with functional programming in domains with very stringent performance requirements if the domain also demands generality.

The project web site provides the Haskell and C source. The Haskell code generates specialized C code for specific simulations, which is then compiled and dynamically loaded.

Witnessing Side-Effects, Tachio Terauchi and Alex Aiken. ICFP 2005.

We present a new approach to the old problem of adding side effects to purely functional languages. Our idea is to extend the language with “witnesses,” which is based on an arguably more pragmatic motivation than past approaches. We give a semantic condition for correctness and prove it is sufficient.We also give a static checking algorithm that makes use of a network flow property equivalent to the semantic condition.

If I understand the idea in this paper correctly, you take a functional language with a possibly non-deterministic or parallel execution model, and then add references to it. To keep this from being impossible to reason about, you add dataflow tokens to each reference operation (assignment, allocation, reading) to ensure that they don't happen until each op's predecessors have happened -- and you make the tokens first class, so that the programmer can directly specify the amount of serial execution needed. Then you can do an analysis to ensure that the reduction is confluent, which means that you have no races.

From the 2005 ACM SIGPLAN Workshop on ML, here is An Applicative Control-Flow Graph Based on Huet's Zipper, by Norman Ramsey and João Dias.

We are using ML to build a compiler that does low-level optimization. To support optimizations in classic imperative style, we built a control-flow graph using mutable pointers and other mutable state in the nodes. This decision proved unfortunate: the mutable flow graph was big and complex, it led to many bugs. We have replaced it by a smaller, simpler, applicative flow graph based on Huet's (1997) zipper. The new flow graph is a success; this paper presents its design and shows how it leads to a gratifyingly simple implementation of the dataflow framework developed by Lerner, Grove, and Chambers (2002).

Escape from Zurg: An Exercise in Logic Programming by Martin Erwig. Journal of Functional Programming, Vol. 14, No. 3, 253-261, 2004

In this article we will illustrate with an example that modern functional programming languages like Haskell can be used effectively for programming search problems, in contrast to the widespread belief that Prolog is much better suited for tasks like these.

...

The example that we want to consider is a homework problem that we have given in a graduate level course on programming languages. The problem was one of several exercises to practice programming in Prolog. After observing that many students had problems manipulating term structures in Prolog (after already having learned to use data types in Haskell) and spending a lot of time on debugging, the question arose whether it would be as difficult to develop a solution for this problem in Haskell. This programming exercise worked well, and we report the result in this paper.

(Haskell source code)

Beyond Pretty-Printing: Galley Concepts in Document Formatting Combinators, Wolfram Kahl. 1999.

Galleys have been introduced by Jeff Kingston as one of the key concepts underlying his advanced document formatting system Lout. Although Lout is built on a lazy functional programming language, galley concepts are implemented as part of that language and defined only informally. In this paper we present a first formalization of document formatting combinators using galley concepts in the purely functional programming language Haskell.

We've talked about functional layout algorithms for mathematics before, so it seems like a good idea to link to a paper about typesetting all the text those formulas are surrounded by.

Status Report: HOT Pickles, and how to serve them, Andreas Rossberg, Guido Tack, and Leif Kornstedt. ML Workshop 2007.

The need for flexible forms of serialisation arises under many circumstances, e.g. for doing high-level inter-process communication or to achieve persistence. Many languages, including variants of ML, thus offer pickling as a system service, but usually in a both unsafe and inexpressive manner, so that its use is discouraged. In contrast, safe generic pickling plays a central role in the design and implementation of Alice ML: components are defined as pickles, and modules can be exchanged between processes using pickling. For that purpose, pickling has to be higher-order and typed (HOT), i.e. embrace code mobility and involve runtime type checks for safety. We show how HOT pickling can be realised with a modular architecture consisting of multiple abstraction layers for separating concerns, and how both language and implementation benefit from a design consistently based on pickling.

The program for CUFP 2007 is now available. The goal of CUFP is to build a community for users of functional programming languages and technology, be they using functional languages in their professional lives, in an open source project (other than implementation of functional languages), as a hobby, or any combination thereof.

This year's offering includes presentations about projects that use Caml, Erlang, Haskell, Scheme, F# and more. Domain specific embedded languages are also mentioned in the abstracts. Some of the presentations deal with projects mentioned here before, such as the Intel IXP network processor but others are new to me and sound quite intriguing.

Some of the people involved with the CUFP workshop are LtU regulars and contributors who may want to add more details and respond to questions or comments.