The rise of functional programming

I have returned from Copenhagen were last week I attended ICFP 2012, the principal scientific conference on functional programming and related topics. This year's conference was very busy with a record number of participants and very high quality presentations (which, by the way, you can watch on YouTube by courtesy of Malcom Wallace).

I was quite surprised by high number of people from industry, both small and large: Google, Jane Street, Standard Chartered, Galois, Well-Typed, Basho, among others. It seems that functional programming is a hot topic for real software developers - not just academics.

The discussion at the end of the Haskell Symposium on Thursday was also a turning point for the language and for FP in general. Aaron Contorer addressed the participants to put forward his view for his new company called FPComplete: get a lot more users in the software industry to adopt Haskell by providing the tools and support that the open-source community can't provide. FPComplete aims to fill this gap in much the same way as RedHat did for Linux in the enterprise. By the way, Aaron is not an FP geek - he headed the developer productivity tools at Microsoft, for example. That someone comming from the software business says that it's now time for FP is a great endorsement for the Haskell language and community.

This is great news for Haskell and wish FPComplete great success!

Predicting the costs of lazy evaluation

For quite some time there have been very compelling arguments for non-strict functional programming in the style made popular by Haskell; here are some more recent ones.  In a nutshell: non-strict semantics is a very powerful "glue" to aid the modular decomposition of programs. And, as software gets more complex, modularity matters most. (Types are arguably even more important, but they are orthogonal to the strict versus non-strict debate).

The most serious critique of non-strict semantics is that the time and space behavior of its implementation (lazy evaluation) are difficult to reason about. In other words: non-strict functional programming allows reasoning about denotational properties but hinders reasoning about operational ones. And how something is computed is often as important as what is computed: for example, all sorting algorithms (when seen as pure functions) have the same denotation, yet their differences are extremely relevant.

However, I don't think the situation is hopeless; two things are required to improve this state of affairs: 1) a language-level operational model of lazy evaluation; and 2) a compositional method for assigning costs derived from the execution model to language fragments.

There has been a good solution for the first part for some time now, namely, Launchbury's natural semantics for lazy evaluation. The key idea is to consider an abstract model of heap as a mapping from variables to expressions (thunks); the evaluation of let x=e1 in e2 extends the heap with a mapping from x to e1 and proceeds to evaluate e2. To model call-by-need (i.e. graph reduction with update in-place) rather than call-by-name we also need to update a thunk with its result when evaluating a variable. (I'm glossing over many technical points for simplicity; go and read the paper for the details).

I have been working with Kevin Hammond, Steffen Jost, Mário Florido and Hugo Simões on a new approach for the second problem based on amortised static analysis. The use of amortisation with lazy evaluation goes back to Okasaki's "Purely functional data-structures"; unlike the later, our approach is type-based and fully automatic. Simplifying slightly many technical details to focus on the intuitions, the key ideas are:

1. for concreteness, we consider the number of allocations in a semantics similar to Launchbury's as our measure of cost;
2. we annotate thunk costs in types, e.g. in a context x:T^q(A) the variable x is a thunk which costs q to evaluate to whnf and whose value has type A;  
3. we also annotate the overall evaluation cost in type judgments, e.g. Gamma |-p- e:B means that evaluation of e to whnf costs p (and admits type B);
4. the type rule for variables requires paying the full cost annotated in the type (i.e. as if evaluation was call-by-name);
5.  we recover the cost of call-by-need by a structural type rule that allows prepaying part or all of the cost of thunks (amortisation allows decoupling the accounting of the cost from the dynamic moment when evaluation actually occurs).

We have written a paper describing the analysis that will be presented at ICFP 2012 conference next week; the full soundness proof is available in a draft extended version of the paper. Moreover, the analysis is fully automatic (it generates a linear program that can be feed to an LP solver to determine the type annotations) and we have built a prototype implementation which we have used to accurately determine the costs of simple examples (but you most likely need to read the paper to understand the output). 

Of course, the general computability limitations apply, so this analysis cannot predict costs of arbitrary programs. In particular, it is limited to costs that are constant or linear functions of the number of data constructors.

A little strictness goes a long way

In a previous post, I argued that Haskell isn't always lazy because you can control strictness of data types and functions. Today I will show a little example that shows how strictness can be used to avoid problems associated with too much laziness. The good part is that you often only need a little strictness.

When implementing an two-player board game, I had to represent the board pieces and moves. For presentation purposes, let us consider Chess moves; a first aproach is to represent a move as a pair of algebraic coordinates, which in turn are pairs of column and row:

type Move = (Coord, Coord)  -- from, to
type Coord = (Char, Int)    -- column, row

For example, the king pawn opening move is represented by (('e',2),('e',4)).

The problem with this is that pairs are non-strict, and therefore the Move type is inhabited by partially defined moves, e.g.:

(bottom, bottom)  :: Move
(('e',2), bottom) :: Move
(bottom, ('e',4)) :: Move
(('e',2), ('e',bottom) :: Move

(where bottom is some expression that either fails to terminate or throws an exception).

We can rule out all these partially defined moves simply by declaring data types with strict components:

data Move = MkMove !Coord !Coord   -- from, to
data Coord = MkCoord !Char !Int    -- column, row

The advantage of the second representation is that if any of the arguments of MkMove or MkCoord is bottom then the result is also bottom, e.g.:

MkMove bottom bottom  = bottom
MkMove (MkCoord bottom 2) (MkCoord 'e' 4) = bottom 

Why is this important in practice? I can think of at least three advantages:

1. if your code is buggy and, say, throws an exception when computing move coordinates you will get the error message when the move is constructed rather than when it is used; if your program is going to fail, then it should fail fast;
2. when writing concurrent or parallel code this ensures that moves are fully evaluated at the right moment, i.e. in the right thread (I stumbled upon this bug when writing a multi-threaded GUI in Haskell);
3. finally, when compiling with optimization on, GHC will unbox strict data fields which reduces the number of allocations and increases locally; for very inner loops this can be a big performance win.

First experiences with the Raspberry Pi

Finally, my Raspberry Pi arrived last week. I had placed my order around April so this was a long wait. But it was worth it!

In case you haven't heard about it, the Raspberry Pi is a $35 bare-board computer intended for school children to learn the basics of computers and programming. It is promoted by a non-profit organization (the Raspberry Pi Foundation) and fills the void left by the demise of the small personal computers of the 80s (such as the ZX Spectrum, the BBC Micro or the C64) on which many of today's scientists and engineers (including myself) first learnt to program.

Of course time has moved on, and the Pi can now be made so cheaply by using high integration components from the mobile phone industry: a system-on-a-chip comprising a GPU, CPU and 256MB of RAM; an SD card slot for persistent storage, an ethernet port, HDMI/composite for display and USB for input devices (or more storage).

The principle difference between the Pi and a smartphone (regardless of price) is that, unlike the later, the Pi is a general purpose programmable computer running a generic GNU/Linux OS. Yes, you can buy or download an SDK for an IPhone/Android but that is a much higher entry barrier. And the higher cost and utility of a smartphone/PC discourages anyone from tinkering with it.

Because it runs an open-source OS, the Pi is remarkably agnostic regarding programming languages and environments. In a couple a days I have successfully tried C, Python, Haskell, O'Caml and Prolog.

I teach programming to first-year CS students and intend to use my Pi to show how abstraction allows running the same high-level program developed in class on both the lab's x86 PCs and the ARM-based Pi: different CPUs, different memory size and storage devices, different flavors of Linux; but by focusing on a proper level of abstraction we can re-use the same source code on vastly different devices. We already tell them such things, but the Pi makes it easy to actually show them. And, as I get older, I realize that the persuasive power hands-on experiment is often underestimated in formal education.