Last week, my colleague Ken Overton and I attended the IFL 2009 conference in South Orange, New Jersey.  The event was partially funded by Jane St Capital, and consisted of research on the implementation and application of “functional languages.”  The invited talk was by Benjamin Pierce (of TaPL fame), on his joint work (with Nate Foster and others) on the bidirectional programming language Boomerang.  The conference’s full range of subjects was diverse, and in this article I will summarize what I saw.

The conference took place over a three-day period.  The first and third days were broken down into four sessions.  The second day ended early, after Dr. Pierce’s presentation, and only had two sessions.  Each session consisted of two to four presentations around a common theme.  This structure worked well enough, and I’ll provide summaries in the same order.

Domain-Specific Functional Languages

First was a presentation on PICOBIT, a compact compiler and virtual machine for a Scheme language suitable for use with microcontrollers.  The Scheme compiler was a fairly straightforward mapping to C.  However, the authors also wrote another compiler for the subset of C that their first compiler produced.  In this C-language, recursion is disallowed, and function-callers pass parameters by modifying their callee’s variables directly.  There was some skepticism about this approach (versus the use of a standard C compiler), although the published performance numbers were reasonable.

Next was a presentation on “Kansas Lava,” a project from the University of Kansas which aims to embed a low-level “circuit” language in Haskell, so that either correct VHDL code can be generated, or the circuit can be tested by the Haskell evaluator.  Here, most of the interesting work in the presentation involved the type-system machinery needed to track the size (in bits) of values as they’re produced by non-trivial compositions of other sized values.  There were no interesting circuit optimizations present, and in fact the speaker demonstrated that even trivial optimizations (e.g.: “1 and X” => X) weren’t done.  Beyond the basic use-case for dependent types, the speaker also sang the praises of applicative functors in his application (twice over a win for Conor McBride).

On a similar note, the next speaker presented his work on Bluespec SystemVerilog, a commercial compiler with a Haskell-like system of Hindley-Milner type inference plus multiple-parameter type classes with functional dependencies.  Also like Kansas Lava, much of the difficult work (and the speaker’s most emotional subject) involved inching toward dependent types with type-level arithmetic and the inevitable difficulties of reasoning about arithmetic expressions.  The speaker was presented with an appeal to resort to standard “computer algebra” systems, but in fairness it’s pretty awkward to prove involved propositions about arithmetic in his type system.  There was also some interest in moving to a legitimate dependent-type system.

Finally, the last presentation in this session was called “iTasks for End-users,” which covered a web-based “task-management” application similar to FogBugz, Trac, or Mingle.  The novel aspect of this system is that the heavily Javascript-based web forms were derived automatically from the structure of the types of records representing those forms, and that the complex client/server interaction and state management involved in processing forms could be written in a straightforward monadic style.  The speaker conceded that most people found the subject of task-management unrewarding, and there was widespread agreement that he was right.

Multi-core Functional Languages

The first presentation in this session was one of Jane St. Capital’s “Summer of Code” winners – a concurrent garbage collector for O’Caml.  The O’Caml runtime system by default has a garbage collector that is particularly hostile to concurrency.  This project used the sensible approach of allocating level-one heaps distinctly to each thread in a process, and compacting to a shared heap when necessary.  Global synchronization happened only in the case where collection/compaction against the shared heap was invoked.  Overall the reported performance numbers looked promising, and the project seemed worthwhile (if you have to use O’Caml).  Unfortunately, the speaker’s accent was too difficult to understand (and ours for him, as he wasn’t able to parse audience questions) so a few good questions about performance edge-cases went unanswered.

Next was a presentation on a coordination language called “S-Nets.”  The language had explicit forms for the parallel and sequential composition of programs, as well as some type-directed dispatching logic that would decide when and how inputs would be presented to programs in these networks.  Because it was an explicit coordination language, complex concurrency scenarios translated to fairly complex expressions, but it may make a reasonable shell language, or a target for Hume (the next presentation).

Finally, the session ended with a presentation of “Hume,” a system for automatically partitioning a program across multiple cores by a “cost-directed” application of meaning-preserving program transformations, the whole body of which the authors have named the “box calculus” (“box” in this case refers to an individual process or thread of execution).  The presenter’s animation of these program transformations was compelling, although slightly dampened by the fact that Hume’s language was limited to non-recursive programs.

Functional Programming and Education

First up in this session was Andy Gill (also the presenter for the Kansas Lava project) discussing his “Chalkboard” library for writing efficient 2D image-rendering programs.  His system was inspired by Conal Elliott’s Vertigo library, a very influential and straightforward (if not inefficient) system for representing images as their sampling functions.  It qualifies as “education-related” in that it has been used to introduce problems of basic graphics programming to undergraduate students.

Next up was a presentation on “Holmes,” a system for detecting fraudulent homework submissions by a search against historical submissions.  The system worked by applying a series of heuristics, ranging from simple token list edit-distance comparison to similar functions on the control-flow-graph representation of two programs.  A project like this might generally be considered depressing, but it energized the audience like few others.

Finally, the session ended with a presentation appealing to attendees to make formal logic (as applied to proving software correctness) a required course in its own right (and not a sidebar in a general “discrete math” course).  Some statistics were used to make this case, showing that the subject can reasonably be taught to undergraduate students, and briefly surveying the results from schools that do treat the subject adequately.  No clear curricula were presented (in fact, the presenter demonstrated that the two most popular remotely-applicable textbooks only mentioned the subject of logical software verification briefly).  Some schools have taken the Coq’Art book as a starting point, although the speaker didn’t address that (it may be too early for judgment).

Parallel Programming and Reactive Programming

The “pHood” tool for analyzing the performance of parallel functional programs (especially Haskell programs) was presented in this final session of the first day.  Based on a similar tool (named “Hood”) for sequential programs, pHood allows the transparent insertion of some monitoring-annotations (presumably driven by some very cautious use of ‘unsafePerformIO’) to determine how effectively your program is making use of parallelism.

Next was a presentation on “fusion-equipped parallel skeletons,” an interesting (even useful) technique for realizing implicit data-parallelism, simultaneously eliminating redundant work by fusion.  Fusion is typically known as a compiler technique that saves work by “fusing” compositions of functions to eliminate the production of redundant intermediate structures (possibly the simplest example is the identity: map f (map g X) = map (f . g) X).  Impressively (or horrifically, depending on your political persuasion) this was achieved in C++ by a novel application of expression templates (effectively, compile-time representations of C++ parse trees realized by clever template functions, and functions operating on those trees).  For commercial users of C++, this is unquestionably a valuable technique to study.

”Liftless Functional Reactive Programming” was the subject of the next talk.  Like the “Chalkboard” talk before it, this project also traces back to the work by Conal Elliott (and others on FRP generally).  Here the speaker developed an FRP system in Scala, and sought to avoid some of the tediousness of other Haskell-based FRP systems by avoiding “lifting” – the mechanical process of mapping functions on pure values to functions on values in the context of an FRP signal.  The solution involved the manipulation of a hidden stack of widget actions, maybe a deflating approach to FRP enthusiasts (especially concurrency-minded ones), but probably effective for any users of Scala.

Finally, the last presentation of the session (and the first day) was entitled “Eventless Reactivity From Scratch,” and featured another FRP system (this one in Haskell).  The speaker briefly surveyed a few well-known FRP systems before explaining his own.  Key to this system is applicative binding (e.g.: his first example defines a lifted sum on signals using the applicative ‘liftA2’ function) and time-based signal functions (hence “eventless reactivity”).  A novel (to my eyes) use of the “mdo” syntax for recursive monadic binding within this system allowed a particularly elegant definition of the sine and cosine functions as integrals of each other.  Overall this presentation functioned as an accessible overview of FRP methods in Haskell, and as a clear roadmap for interested developers.  As with the other presentations on this subject, Conal Elliott’s FRP work was also highlighted.

Compilation

The second day began with a very interesting presentation on “compiling SaC for the ‘MicroGrid’ architecture.”  SaC (or “single-assignment C”) is a popular language among researchers in parallel languages, and in this case it was used to realize data-parallel programs on a novel hardware platform called the “MicroGrid.”  This architecture features a massive collection of processors, each capable of evaluating many threads of execution concurrently.  As with several other projects of this sort, it’s nested data-parallelism that poses unique challenges to compiler-writers, and although this architecture went some way toward alleviating those problems, in at least one example the presenter demonstrated sub-optimal distribution at the second level of nested parallelism (e.g.: the first pass distributes across three processors, and from there to 200 threads each).  This project is definitely an interesting work-in-progress.

”Arity raising” was the next topic; the main objective here is to optimize for large register sets by mechanically breaking one argument of a function into multiple arguments (the constituent parts of the argument that are actually used in the body of the function or, recursively, its callees) with the hope that better register usage can be achieved.  As newer processors feature ever larger register sets, the argument for this particular optimization will grow more compelling.  In this case the optimization was applied to a compiler for an ML-language, which made for a good testbed in any case (ML programs probably rely on language-level constructs for composing data more than most other languages).

A restricted form of dependent types, called “Symbiotic Expressions” by their presenters, made for the last presentation in this session.  The “expressions” meant here are actually index variable and array bounds constraints, which are “symbiotic” in that they are associated with AST nodes in the intermediate form of a SaC program.  A few associated optimizations were discussed, including an “algebraic with-loop folding” technique for flattening nested data-parallel loops.

Language Features

Here we received an interesting presentation titled “A Calculus for Coercive Subtyping.”  In fact, the aim of this project is to implement a dependently typed lambda calculus with implicit coercion (as a means of achieving subtyping).  The talk was very dense with typing rules, but overall the approach seemed amenable to the general system of qualified types (translated to an intermediate calculus with explicit witnesses of subtyping/overloading) developed by Mark Jones (though he didn’t study dependent type systems in that work).  Working in a dependently typed lambda calculus also adds some complication in the valid dependency-pairings admitted – i.e.: the presenters defined a lambda cube of overloading parallel to the standard one.  Unfortunately, the pace of the presentation made it difficult to follow, and the audience presented no questions.

A powerful application of “stream fusion” in Haskell was demonstrated next.  Stream fusion is a special case of the general principle of fusion (discussed earlier), which, with the GHC compiler, can be achieved with “rewrite rules” – directives that tell the compiler how certain terms can be simplified (and only valid due to the inherent referential transparency of Haskell terms).  Here the objective was to provide an efficient representation for Unicode strings, allowing (as with regular strings in Haskell) the normal list-functions (e.g.: map, filter, foldl, etc).  To make this work, the standard list functions must be defined in terms of streams rather than lists, and dual stream/unstream functions must be defined on data-types (in this case, on arrays of Unicode characters) in order to give them the expected interface (and to convert from that interface back to the array form).  In this way, a function removing numbers and converting to uppercase on Unicode strings can be expressed as “unstream . (map toUpper) . stream . unstream . (filter isNotDigit) . stream” and the fusion step here will be the application of the rewrite rule “stream (unstream x) = x” (which has the effect of eliminating intermediate structures, as desired).  In all, this was an ideal presentation.

“General contract boundaries” were discussed in the next presentation, in the context of PLT Scheme.  As the first audience member at question-time observed, there was a significant amount of overlap between this project and the general principle of type systems.

Finally the session ended with another gem, an embedding of a bidirectional language in Haskell.  This approach contrasted with the invited presentation by Ben Pierce (to follow) by defining a data-type for bidirectional functions, and combinators on such functions mirroring many standard functions (map, filter, etc).  Perhaps the greatest benefit from this approach, aside from the usual benefits from embedding in Haskell, was that reverse functions could be generated with their forward data trivially.  The bidirectional editor GUI was much less compelling, but it was good enough to demonstrate the basic principles.

How to Build Your Own Bidirectional Programming Language

This invited talk began with a summary of the kind of problem that bidirectional programming aims to solve: in essence, the “view-update” problem familiar to users and developers of relational databases.  As a running example, the presenter used an XML representation of a simple database of composers, and a projection (or “view”) of a subset of that data as simple newline-delimited text.  It should be possible then to update the newline-delimited view and have the original XML representation updated as well.  In contrast to the previous presenter’s solution to the same problem, this one was built as its own self-contained language: Boomerang.  Its primitives are finite-state transducers, just the simplest bidirectional transformations on strings (describable by regular expressions).  A tool inspired by this language is apparently used by RedHat to unify configuration of all sorts of small /etc/ configuration files.  Other applications are immediately possible as well.  For example, as my colleague Ken Overton pointed out, sharing structure representations between multiple languages (e.g.: Java/C++) can be made much simpler, without the intermediate canonical representations that many people resort to.

Theorem Provers and Testing

On this, the third and final day, the first session began with a presentation on “user-interface driven theorem prover development.”  Unfortunately, the subject of the talk was not the theorem prover itself, but just its GUI.  In essence, the presentation was about Intellisense for theorem provers (and thanks to the Curry-Howard isomorphism, the “for theorem provers” part can be dropped).  The presenter digressed at some length on the subject of highlighting sub-expressions.  I don’t remember the word “zipper” mentioned, but that was his approach, in essence.

Next up was a presentation on hygienic macros in the ACL2 theorem prover.  Actually this talk again was only incidentally related to theorem provers.  ACL2 admits a subset of Common Lisp, where higher order functions are strictly disallowed.  To get around this limitation, users of ACL2 use macros heavily (to generate first order functions from macros embodying higher order functions).  That would have been frustrating enough, but their macro system was unhygienic (it allowed macro substitution to capture variables from its enclosing scope) and so this presentation concerned the cleaning up of that mess.  In essence, this is the resolution of the same old “dynamic scope” bug under a different guise.

Finally the last presentation in this session was another gem, and (although strictly speaking it was about “testing”) this presentation came the closest to actually discussing a technique for proving theorems.  Its subject was “unifying QuickCheck and SmallCheck,” which requires some background explanation.  QuickCheck is a novel system for testing Haskell programs (and Erlang, if you need it) by requiring only the specification of straightforward logical propositions (e.g.: “reverse (xs++ys) = (reverse ys)++(reverse xs)”), after which it will randomly search the space of the quantified variables of the proposition (that’s the “xs” and “ys” variables of the last expression) until it finds a configuration that contradicts the proposition.  Having then found a contradiction, it simplifies the offending configuration until it’s as simple as possible, while still demonstrating the contradiction.  SmallCheck is a similar system, except that rather than randomly searching for a contradiction it will exhaustively search for a contradiction (up to a given size).  This presentation concerned the technical details of bringing both of these systems together into one.

Incrementalization, GADTs, Generic Programming

“Incrementalization” of datatype-centric libraries was the focus of the first presentation in this series.  As the presenter defined it, datatype-centric libraries are those where a small set of datatypes are constructed and summarized or translated only within the context of that library.  “Incrementalization” of such a library entails the addition of some accumulating data in the constructors of the relevant datatypes, and the rewriting of “deep” recursive functions over such structures (for example, recursively counting the nodes of a binary tree) to “shallow” functions of the accumulators added to those datatypes (for example, adding the count of children to a binary tree’s constructor, so that counting them is trivial and incrementally building the binary tree also incrementally computes this count from nested binary tree nodes).  This approach of “incrementalizing” libraries amounts to an embedding of attribute grammars in Haskell, which the presenter briefly touched on.

The next presenter introduced the Clean language’s “Dynamic” type (for runtime type checking) and then gave a presentation on simulating Clean’s “Dynamic” with GADTs in Haskell.  His analysis suggested that Clean’s dynamic type-information consumption is dual to an analogous type-information construction inherent in the use of GADTs.

A language (“Qube”) for efficient “rank-generic” array programs formed the basis for the next and final presentation in this session.  This presentation covered the application of dependent typing (in a limited context) to type-check “shape analyses” on array operations.  This is a subject covered in bits and pieces by several different approaches, but it has long seemed that dependent types provide an ideal way to synthesize these many disparate techniques, so I was especially happy to find this presentation.  The generalized treatment of matrix multiplication (for matrix, vector, and scalar cases in each configuration) is particularly amenable to this treatment, as are many other important functions like the inner product and so on.  The presenters covered the type-safe implementation of these functions in Qube, and demonstrated performance numbers on massively parallel hardware that were in most cases almost identical to hand-written C.  All in all, this was one of the most interesting presentations of the entire conference for those of us working in the financial sector.

Evaluation Models and Environments

Leading this session was a presentation on “Call by Effect.”  The presenter initially made the standard argument in favor of effect systems – higher order functions (like map, filter, etc) only need to be written once, and are then polymorphic in both computation types and effect types (in contrast to Haskell where there’s a pure map function and a monadic ‘mapM’).  Following that, the presenter defined “call by effect” as a method of achieving lazy evaluation when pure code is evaluated, and eager evaluation in the presence of effects.  As far as evaluation order goes, this approach allows a language with effect types to reduce terms in the same way as Haskell (lazily when possibly, eagerly when necessary) although, strictly speaking, Haskell offers more than two options.  With its ability to describe effects without special-purpose type-system extensions, Haskell still seems closer to the ideal, but its lifting functions and monad transformers are awkward enough to make effect system research like this worthwhile.  Maybe some day the two will meet somewhere in the middle.

The next presentation was titled “Very Lazy Evaluation: A New Execution Model for Functional Languages.”  It concerned a system similar to abstract machines like the SECD or STG machines, suitable as a target for compilers of functional languages (and specifically those with lazy evaluation).  The approach seemed to me to be a fairly straightforward stack machine, but further details in the post-conference paper may demonstrate more subtle features.

Finally, the last presentation in this session seemed like essentially a small FRP system for mobile devices in Scheme.  Like the other Scheme presentations, there was a fair amount of audience skepticism about basic points of practice (ad-hoc type systems being developed, unclear/inconsistent semantics of low-level OS interaction, etc).  The presenter showed a couple of amusing projects built with this system (one great video was of a group of developers shaking their phones to produce music).

Implementation and Benchmarking

”Record combinators” were the subject of the first presentation in this last session of the conference.  This presentation was also fairly dense in implementation details, but the general approach seemed to be to embed a language of record extensions/reflection in Haskell.  Here I was again reminded of Mark Jones’s work in qualified types – where qualified types are shown to unify Haskell-style type classes, O’Caml-style structural subtyping, and type systems with record constraints.  The full details were a little difficult to follow in the presentation setting, but (like the example of the inner-product function for rank generic dependent array programming) there were a few examples given that helped motivate the audience to want such a system.  These seemed to boil down to wanting to treat records generically in one case (say, sending any serializable record as a message across a network) while simultaneously verifying code against the specific structure of the record in most other cases (as when a specific field is requested from a record).  I have not personally done much work with these kinds of systems, but it seems like a interesting subject to explore.

The design and implementation of higher-order modules in SML/NJ was covered next.  Modules are ML’s principle method of organizing programs, along with functors (ML’s name for module-dependent modules).  SML/NJ also includes support for “higher-order” modules (functor-dependent modules, or modules that define functors).  The SML/NJ documentation has some useful examples (under the heading “higher-order modules”).  This presentation explored where the design of higher-order modules has worked well in SML/NJ, and clarified some issues of its static semantics for those of us who don’t work often with ML modules.

Finally, the session (and the conference overall) ended with a presentation on a project called “Unibench,” which aims to be a universal tool for benchmarking applications.  Unibench is a web application that can run several builds of arbitrary programs (where builds are organized along the usual OS/compiler groups), and automatically apply ad-hoc benchmarking scripts to keep track of each program’s performance profile over time.  Several audience members pointed out that the Unibench tool had a lot in common with build-server systems, and in fact it seemed to be a primitive version of TeamCity.

Summary

Overall the conference had several very interesting presentations, some of which have a direct impact on those of us working in the financial sector.  I hope that I haven’t mischaracterized any of the presentations (if so, I hope that the aggrieved parties will add comments here).  It was very interesting to get a chance to put faces to the names of several people whose work I’ve only encountered before in print.  At the end of the last day, I was left with a lot of ideas to think about.