Informal minutes of IFIP Working Group 2.8
28th meeting, Marble Falls, Texas, US
March 7-11, 2011

List of attendees

Members: Arvind Lennart Augustsson Jack P. Dennis Conal Elliott Kathleen Fisher Robert Harper Fritz Henglein Ralf Hinze John M. Hughes John Launchbury David B. MacQueen Simon Peyton Jones Benjamin Pierce Rinus Plasmeijer Norman Ramsey Mary Sheeran Olin Shivers Satnam Singh Stephanie Weirich Steve Zdancewic

Observers: Matthias Blume Jean-Christophe Filliâtre Matthew Flatt Matthew Fluet Jeremy Gibbons Simon Marlow Conor McBride Ulf Norell Don Stewart Bjarne Stroustrup Dimitrios Vytiniotis

Note: many of the links are dead, which simply means that I haven't yet received the material.

Technical presentations

Fritz Henglein, Regular expressions as types: Bit-coded regular expression parsing. (Mon 2011-03-07, 09:20-10:05)

(joint work with Lasse Nielsen, DIKU) Regular expression parsing is the problem of producing a parse tree of a string for a given regular expression. We show that a compact bit representation of a parse tree can be produced efficiently, in time linear in the product of input string size and regular expression size.

Bjarne Stroustrup, Concepts for C++1y: The Challenge - Why C++0x Concepts failed and what to do about it. (Mon 2011-03-07, 10:05-11:05)

One of the major goals of the language part of C++0x is to provide better support for generic programming. I see that as a key to both better library development and to better support of “C++ novices” of all backgrounds. I present the fundamental mechanisms and basic idioms of C++ generic programming using C++98, then I present the support for template argument requirement specification for template arguments designed for C++0x. I critique that design based on experience gained from its specification, implementation, and use leading to some ideas for a redesign.

Matthew Flatt, Impersonators and Chaperones: Run-time Support for Higher-Order Contracts. (Mon 2011-03-07, 11:30-12:30)

Racket’s impersonator and chaperone language constructs provide the run-time support needed to implement higher-order contracts on mutable structures and abstract datatypes. Using impersonators and chaperones, contracts on mutable data can be enforced without requiring all accesses to pass through expensive accessor functions; contracts on objects and classes can be implemented with lower overhead; and contracts on mutable values can properly ascribe blame when checks fail. These properties of contracts are vital to provide a basis for building robust abstractions. In particular, Typed Racket relies on contracts to interoperate smoothly with untyped code, where con- tracts enforce type requirements at the boundary between typed and untyped code.

Steve Zdancewic, Puzzle: Loco! Game. (Mon 2011-03-07, 14:00-14:05)

The Game of Loco by Reiner Knizia

Game Pieces:

5 chips in each of 5 colors (red, blue, yellow, green, purple); 6 cards numbered 0..5 in each color (30 total).

Setup:

1. Shuffle the cards
2. Hide two of the cards (for the duration of the game)
3. Deal the cards (each player gets 7)

Play: (Starting with a randomly determined player and continuing clockwise.)

Each player in turn:

1. Plays a card to the stack of the appropriate color
2. Takes a chip of any color

Ending:

The game ends after any stack has all 6 cards of its color. (The player who completes the stack still gets to take a chip for that turn.)

Scoring:

The value of a chip is the number of the card on the top of the stack of the same color. The winner is the player whose chips are worth the most points. (Ties are possible.)

Jean-Christophe Filliâtre, Memo Tables. (Mon 2011-03-07, 14:05-14:50)

This talk discusses an implementation issue regarding memoization tables. The context is that of the Why deductive software verification platform, where various transformations are applied to turn verification conditions into suitable input for automated theorem provers. The results of these transformations are memoized, for greater efficiency. Both transformation arguments and transformations themselves are likely to be reclaimed by the garbage-collector at any point. Thus it raises the question of implementing memoization tables where entries can be reclaimed as soon as either the argument or the memoized function is reclaimed, in a completely symmetric way.

Conal Elliott, Deriving work-efficient in-place parallel scan. (Mon 2011-03-07, 14:50-15:45)

This talk begins with a CUDA implementation of parallel prefix sum (see Example 39–2 for code) and then explores how this code might have arisen via program derivation beginning with an elegant, purely functional specification.

After spending quite some time teasing out the hidden beauty behind the clever, low-level code, I’ve encountered some fun and reusable techniques for connecting between the purely functional world of Haskell (mathematically precise, safe, simple & composable) and the imperative & parallel world of CUDA, including the following:

Power-of-two-sized arrays to binary complete leaf trees.

Such trees as an n-ary functor composition.

Relate bit-level manipulation of array indices to simple & composable operations on functional bit vectors.

Distinguish the two varieties of trees that correspond to big-endian vs little-endian bit vectors. The big-endian perspective leads naturally to *n log n* work, while little-endian leads to linear work.

Connect destructive (in-place) update to non-destructive “update” via “semantic editor combinators” (composable modifiers of structured data).

Capture the implicit-but-necessary constraints on array sizes and indexing via statically specified and automatically checked types (size for indices and depth for trees). My recent series of six blog posts share some of what I’ve worked out so far.

I’m going for a solid framework of theory, implementation, and examples for combining the best properties of the Haskell & CUDA worlds. (When I say “Haskell”, I mean the denotationally understood part, which excludes IO.) My intent is to exploit the functional specifications to get composability, understandability, and correctness, preserve these properties by systematic transformation of high-level specifications into into a semantically equivalent form, and then generate correct & efficient CUDA code. Thus the CUDA code is a sort of low-level (compared with Haskell) intermediate language, correct by construction. Rather than try to understand, modify and compose at the CUDA level, one would change the high-level spec and perhaps the derivation. For instance, in deriving the parallel CUDA exclusive scan algorithm, the motivation for the particular choice of element additions & swaps became clear to me. With that understanding, it was easy to derive a correct in-place inclusive scan algorithm as well, without an additional pass.

Dimitrios Vytiniotis, Termination. (Mon 2011-03-07, 16:20-16.55 and Mar 8, 16:15 - 16:20)

Terminator is one the most powerful tools for automatic termination analysis and relies on the disjunctive invariants method. A program is typically rewritten so that the transitive closure of the transition relation is exposed in some program variables. Showing that the transitive closure of the transition relation is contained in the union of some well-founded relations amounts to showing that the program terminates. In this talk I give a declarative specification of this method in terms of a typing rule in a refinement type system, which does not involve program rewriting. This typing rule could serve as a new method for type-based termination checking in dependently or refinement-based programming languages.

Jack Dennis, Simulation of the Fresh Breeze Storage System. (Mon 2011-03-07, 16:55-17.30)

Robert Harper, Adventures in Two-Dimensional Type Theory. (Tue 2011-03-08, 09:05-09.45)

Simon Marlow, A monad for deterministic parallelism. (Tue 2011-03-08, 09:45-10.40)

In this talk I introduce the Par monad, a programming model for parallelism in Haskell that offers the programmer greater control than the traditional par/pseq and Strategies models, while retaining a deterministic and pure interface. Furthermore, Par is implemented entirely in a Haskell library using monadic concurrency, and I give (almost) the full implementation of a work-stealing scheduler. There are some preliminary results suggesting that the technique can achieve respectable parallel speedup even with the limited attention to performance it has received so far.

Jeremy Gibbons, Simple Monadic Equational Reasoning. (Tue 2011-03-08, 11:15-12:15)

(joint work with Ralf Hinze) Lazy functional programming is attractive, because it supports simple equational reasoning (among other reasons); but still useful, because important computational effects can be captured via monads. Nevertheless, it is not immediately obvious how to combine equational reasoning with computational effects. We present a simple axiomatic approach to equational reasoning about effectful programs, based on algebraic theories - that is, the additional operations providing the specific effects of a monad, and the equations that these operations are required to satisfy.

John Hughes, Work we haven't done yet. (Tue 2011-03-08, 12:15-12:30)

Software development is of national importance for the Swedish economy but competition from low-wage economies is murderous. To compete in to future, Swedish software developers must become mud more productive. Resource aware functional programming is a promising way to adders this, We see a major opportunity for Fp research, and plan to work in this area in the coming year.

Matthias Blume, Paying for a "free" theorem. (Tue 2011-03-08, 14:00-14.55)

A "free" theorem lost due to the addition of non-termination effects can be recovered via a syntactic restriction (the CPS restriction). But the resulting theorem is not "free", i.e., it does not follow from parametricity.

Rinus Plasmeijer, Getting a Grip on Task that Coordinate Tasks. (Tue 2011-03-08, 14:55-15:40)

The iTask system is a combinator library for the functional language Clean to support the \emph{construction} of workflow applications. Workflows can be described in a compositional style, using pure functions and combinators as self-contained building blocks. Thanks to the expressive power of the underlying functional language, complex workflows can be defined on top of just a handful of core task combinators. However, it is not sufficient to define the tasks that need to be done. We also need to express the way these tasks are being supervised, managed and visualized. In this talk we report on our current research effort to extend the iTask system such that the coordination of work can be defined as special tasks in the system as well. We take the opportunity to redesign editors which share information and the combinators for defining GUI interfaces for tasks, such as buttons, menu's and windows. Even though the expressiveness of the resulting system increases significantly, the number of core combinators can be reduced. We argue that only two general Swiss-Army-Knife higher order functions are needed to obtain the desired functionality. This simplifies the implementation significantly and increases the maintainability of the system. We discuss the design space and decisions that lead to these two general functions for constructing tasks.

Ulf Norell, Fun with Agda - Getting rid of your Booleans. (Tue 2011-03-08, 16:20-17:20)

David B. MacQueen and Robert Harper, Discussion: Teaching Programming Languages. (Tue 2011-03-08, 17:25 - 18:30)

Conor McBride, Fun with First-Class Datatypes. (Wed 2011-03-09, 09:00-10:05)

In the setting of dependently typed programming, I demonstrate a way to replace the usual datatype declaration construct with a mechanism for first-class datatype description, turning the grammar of datatype declarations into a datatype itself. Elements of this type are decoded as endofunctors on a category of indexed sets, where the usual fixpoint construction still works. This facilitates a variety of datatype-generic constructions, implementable by ordinary programming. My motivation is to find a workable design for the treatment of datatypes in a future version of Epigram, and to this end, I use Agda as a testbed to explore the viability of the constructions.

Don Stewart, Combining Languages and SMT solvers: an EDSL study. (Wed 2011-03-09, 10:05-11:05)

SMT solvers are automated tools to solve the “Satisfiability Modulo Theories” problem — that is, determining whether a given logical formula can be satisfied. However, unlike SAT solvers, SMT solvers generalize to solving such NP-complete problems that contain not just boolean variables, but more useful types, such as lists, tuples, arrays, integers and reals. The challenge now is to make such power easily available to programmers without a formal methods background. In this talk I will describe an approach for a typed embedding of an SMT Solver into Haskell.

Ralf Hinze, Monads from Comonads - Comonads from Monads. (Wed 2011-03-09, 11:40-12:30)

Shall I structure my programs using comonads or monads? Functional programmers have embraced monads but they have not fallen in love with comonads. This is despite the fact that the simplest example of a (co)monadic structure is a comonad, the product comonad. The talk explains why the product comonad has not taken off. Along the way, I develop a little theory of program transformations.

Kathleen Fisher, Forest: Typing FileStores. (Wed 2011-03-10, 09:00 - 09:50)

Many applications use the file system as a simple persistent data store. This approach is expedient, but not robust. The correctness of such an application depends on the collection of files, directories, and symbolic links having a precise organization. Furthermore these components must have acceptable values for a variety of file system attributes such as ownership, permissions, and timestamps. Unfortunately, current programming languages do not support documenting assumptions about the file system. In addition, actually loading data from disk requires writing tedious boilerplate code. This paper describes Forest, a new domain-specific language embedded in Haskell for describing directory structures. Forest descriptions use a type-based metaphor to specify portions of the file system in a simple, declarative manner. Forest makes it easy to connect data on disk to an isomorphic representation in memory that can be manipulated by programmers as if it were any other data structure in their program. Forest generates metadata that describes to what degree the files on disk conform to the specification, making error detection easy. As a result, the system greatly lowers the divide between on-disk and in-memory representations of data. Forest leverages Haskell’s powerful generic programming infrastructure to make it easy for third-party developers to build tools that work for any Forest description. We illustrate the use of this infrastructure to build a number of useful tools, including a visualizer, permission checker, and description-specific replacements for a number of standard shell tools. Forest has a formal semantics based on classical tree logics.

Simon Peyton Jones, Termination combinators forever. (Wed 2011-03-10, 09:50 - 10:35)

I describe a Haskell combinator library to support online termination detection.

Presentation of research topics. (Wed 2011-03-10, 11:05 - 11:25)

Simon Peyton Jones:

Termination combinators

Jeremy Gibbons:

Reasoning with idiomatic traverse

Norman Ramsey:

A core calculus for CLU's type system

Matthew Fluet:

Type-flow analysis

David B. MacQueen:

Language design: ML * Haskell

Fritz Henglein, HIPERFIT. (Wed 2011-03-10, 11:25 - 11:30)

Norman Ramsey, Can Functional Programmers Make 'make' Make Sense? (Wed 2011-03-10, 11:30 - 12:15)

The widely used build tool 'make' offers features that might appear superficially attractive to functional programmers: specifications appear declarative, tools are supposed to behave like functions, and 'make' uses memoization in the filesystem to reuse the results of applying a function whose arguments have not changed. But a closer look reveals significant flaws: it's hard to identify all the 'arguments' of a 'function', it's not clear what to do with higher-order functions (make computes outputs by running tools that are built with make by running tools...), and the only available semantics is low-level and imperative. There appear to be some research opportunites and questions of interest, such as "what is the denotation of a Makefile" and "what might it mean for Makefiles to compose?"

Satnam Singh, Running Dynamic Agorithm on Static Hardware. (Wed 2011-03-10, 12:15 - 12:45)

Our goal is to synthesize functional programs that manipulate dynamic data structures into corresponding circuits implemented on FPGA chips. As a first step we try to solve the problem of synthesizing recursive functions which are typically not supported by conventional hardware description languages or C to gates synthesis tools. We restrict ourselves to self-recursive functions which can be implemented with a private stack (so no single large stack acts as a memory bottleneck for multiple recursive functions). We outline an initial prototype implementation that can compile simple self-recursive functions into Xilinx FPGA circuits.

Stephanie Weirich, Generic Binding and Telescopes. (Wed 2011-03-11, 09:00 - 09:45)

(joint work with Brent Yorgey, Chris Casinghino, Vilhelm Sjoeberg and Tim Sheard) In this talk, I will present an expressive specification language for binding structures that supports a variety of binding features, including list and pattern binding, recursive binding, nonbinding annotations, telescopes and multiple atom types. This specification language is implemented in the Haskell type system so that standard binding operations (free variable calculation, alpha-equivalence, substitution) can be implemented as generic functions. The intrepid can browse our implementation via "cabal install replib" (GHC 7 required) or on our (google svn code repository). All examples presented in the talk are available in the "examples" directory of the repository.

Olin Shivers, Logging side-effects and interactive parsing. (Wed 2011-03-11, 09:45 - 10:20)

John Launchbury, A Quick View of Homomorphic Encryption. (Wed 2011-03-11, 10:20 - 10:45)

Homomorphic encryption has long been a theoretical dream that many thought would be forever impossible -- the idea of performing computation on encrypted data without leaking information seemed almost contradictory. Yet recently it has been shown to be possible! The schemes that have been discovered so far are ridiculously inefficient, but there are paths forward that could potentially make it practical.

Arvind, Verification of Microarchitectural Refinements in Rule-based Systems. (Wed 2011-03-11, 11:15 - 11.50)

(joint work with Nirav Dave (MIT), Michael Katelman (UIUC), Myron King (MIT), Arvind (MIT), and Jose Meseguer (UIUC)) It is necessary to do modular refinements in complex digital systems to meet performance, area or timing constraints. Since verification is a major cost component of design, functionally correct refinements are usually restricted to changes that preserve FSM equivalence. This restriction on refinements does not allow useful Microarchitectural changes, for example, the insertion of a register in a long combinational path to meet timing. A design methodology based on guarded atomic actions or rules offers an opportunity to raise the notion of correctness to a more abstract level. In rule-based systems many refinements can be expressed by breaking down a rule into smaller rules, which accomplish the original operation in multiple steps. Since the smaller rule executions can be interleaved with other rules, the verification task is to determine that no new behaviors have been introduced by smaller rules. We formalize this notion of correctness and present a tool based on SMT solvers that can prove, automatically, that a refinement is correct, or when a refinement is not correct, provide concrete information as to why. We demonstrate its use in proving the correctness of the transformation of a processor pipeline from 4 stages to 5 stages.

Benjamin Pierce, CRASH/SAFE. (Wed 2011-03-11, 11:50 - 12:30)

I'll give a brief advertisement for the newly minted CRASH/SAFE project, which aims to replace the whole hardware/OS/PL/software stack with a significantly more secure one, using a combination of richly tagged hardware, a novel OS "zero kernel" architecture, and new programming languages incorporating strong notions of compartmentalization and information flow tracking. The technical meat of the talk is a taste of a strawman programming language, built around a CBV lambda-calculus with Liskov/Myers-style information flow labels.

WG2.8 says hello to Paul.