PADL/PEPM 2010, Day 2

Again, here are a few talks that caught my attention and I thought I would share my impressions. Enjoy!An Ode to Arrows, Hai Liu & Paul Hudak (PADL 2010)Representing the infinite tower of derivatives of a function as a lazy list has become popular in the Haskell world, the most recent example being Conal Elliott’s paper on Beautiful Differentiation at ICFP 2009. This work explores taking the same ideas and using them to express systems of Ordinary Differential Equations.A natural translation of these ideas into Haskell requires recasting the ODEs in an integral form, rather than a purely differential form, leading to a shallow embedding of the equations as recursive equations in Haskell. Unfortunately, this simple translation leads to quadratic computational complexity, in both time and space. Memoization can address this moderately well, except that one is left with the problems of managing (and freeing) the memo-tables.Moving to arrows leads to a better solution. The recursion is expressed using Paterson’s ‘loop’ construct, which puts it in the control of the programmer. When combined with Causal Commutative Arrows (http://lambda-the-ultimate.org/node/3659) the circuits can be optimized into tight iterative loops, with dramatic improvements in performance.A DSL Approach to Protocol Stack Implementation, Yan Wang & Veronica Gaspes (PADL 2010)Implementations of network code are very hard to connect with the specifications, leading to major challenges for maintenance. This is significant for embedded devices which need implementations that appropriately trade off power, speed, and memory usage. To that end, IPS is a DSL for generating network code. It allows packet formats to be defined using dependencies between fields, handles the interaction of protocol and packet, and provides a framework for constructing the protocol stacks.In a comparison exercise, IPS was used to generate code for the Rime protocol stack. Compared with the published hand-written version in C, the IPS code was 1/4 of the size of the C, but produced an executable 25% larger. The performance on sending packets was 10% worse in the IPS version, but both versions were equivalent for receiving packets.No measurements were given for ease of maintenance or design exploration between the two versions, but I know which one I would prefer to have to work with…I/O Guided Detection of List Catamorphisms, Martin Hofmann & Emanuel Kitzelmann (PEPM 2010)Having the computer write its own programs has always been appealing. You provide some input/output pairs and the machine comes up with a generalization expressed as a program that has the same behavior. Broadly, there are two ways to do this: analytical (where the structure of the data is examined to build the program), and generate & test (where many programs are produced, and their behavior improved, perhaps by evolutionary combinations).This work uses the idea of catamorphisms (also known an fold or reduce functions) as a template to explore, when the i/o pairs comes from a recursive data type (just lists at the moment, I think). Using the fact that if a function g satisfies ‘g [] = v’ and ‘g (x:xs) = f x (g xs)’ for some ‘f’ and ‘v’, then ‘g = fold f v’, the system figures out what the i/o pairs for the sub-functions would be, and then tries to deduce the definitions. It includes specific smarts that notice when the form of the function corresponds to a ‘map’ or ‘filter’.Bridging the Gap Between Symbolic and Efficient AES Implementation, Andrew Moss & Dan Page (PEPM 2010)Different implementations of AES, the standard for block encryption, run at very different speeds. The original reference implementation takes about 840 cycles per round, the Open SSL implementation takes 30, and a top performing assembly code version takes 21.6 cycles per round. The CAO DSL and compiler described in this paper takes a high-level spec and compiles it, producing code that takes 23 cycles per round. Impressive.CAO is a sequential language, designed to be easily related to the pseudo code that crypto specifications often use. A significant amount of effort in the compiler then goes into deducing what parallelism is possible and how best to balance the work. CAO has matrices as first class objects, to allow the compiler opportunity to deduce good representations. There are also optimizations to convert references from the matrices in their entirety to references to the appropriate sub-portions, so as to eliminate unnecessary additional sequential dependencies. The compiler also has some optimizations that are specific to AES.Clone Detection and Elimination for Haskell, Christopher Brown & Simon Thompson (PEPM 2010)I liked this talk partly because it reminded me to go and play with HaRe (https://www.cs.kent.ac.uk/projects/refactor-fp/hare.html). The Haskell Refactorer is an Emacs and Vim tool for manipulating Haskell 98 programs, providing structural transformation (like fold/unfold), altering data types (like adding or eliminating arguments), slicing, and now, clone elimination (cue Star Wars music).The clone eliminator finds repeated code forms above a threshold size, and deduces the least-general generalization of the code to invent new functions if necessary. Clone detection is entirely automatic, but it is up to the programmer to decide which ones to act upon — sometimes adding abstraction helps the structure of a program, and sometimes it obscures it. It works within monadic code too.HaRe works mostly at the AST level, though it does use the raw token stream for some of its discovery. It also works across modules.Making “Stricterness” More Relevant, Stefan Holdermans & Jurriaan Hage (PEPM 2010)The old approaches to strictness were all denotational, but to actually use strictness within the compiler it is better to have a syntax-driven formulation, i.e. in logic. There is a nice approach which uses the concept of ‘relevance’, where ‘x’ is relevant to ‘e’ if every evaluation of ‘e’ demands ‘x’. Clearly, relevance is equivalent to strictness.But actually it doesn’t work so well in the presence of ‘seq’. The original formulation of relevance assumed that the only time a function would be evaluated was at its point of application. Then there is no way to distinguish ‘undefined’ from ‘x->undefined’. ‘Seq’ changes all that. The paper shows how to fix relevance by tracking which lambdas are used applicatively (i.e. applied somewhere in the program in a place that will be evaluated). The definition is circular, but the least solution is the one intended.