Informal minutes of IFIP Working Group 2.8
25th meeting, Park City, Utah, US
June 16-20, 2008

List of attendees

Members: Arvind Lennart Augustsson Robert Cartwright Koen L. Claessen Jack P. Dennis Kathleen Fisher Robert W. Harper Fritz Henglein Ralf Hinze (secretary) Paul Hudak John Launchbury David B. MacQueen Rishiyur S. Nikhil Christopher Okasaki Simon Peyton Jones (chair) Rinus Plasmeijer Didier Remy Mary Sheeran Olin Shivers Satnam Singh Peter Thiemann Philip Wadler Stephanie Weirich

Observers: Robby Findler Matthew Flatt Andres Löh John Peterson Francois Pottier Norman Ramsey Konrad Slind Don Syme Andrew Tolmach David Walker Steve Zdancewic

Technical presentations

Bob Harper, A Programming Problem. (Mon 2008-06-16, 09:10)

By applying well-known results in proof theory it may be proved that the evaluation function for Goedel's T is definable in Girard's System F. But it is not obvious how to extract an actual interpreter for T written in F. The problem is to give the implied implementation explicitly.

Ralf Hinze, A Proof Puzzle. (Mon 2008-06-16, 09:30)

Prove that two ways of generating binary numbers are equivalent.

Koen Classen, Safe, Purely Functional APIs to Low-Level Imperative Libraries: A programming challenge. (Mon 2008-06-16, 09:35)

The challenge is to design the API of a library, where the programmer can (1) create factory objects, and (2) the factory objects can create reference objects, where the type system (a) enforces the absence of use reference objects with the wrong factory objects, and (b) pure functions can be created.

Rishiyur S. Nikhil, On "Control Adaptivity": how to sell the idea of Atomic Transactions to the HW design community. (Mon 2008-06-16, 09:50)

Bluespec sells software tools for improving productivity in hardware chip design (ASIC and FPGA). The central innovation is the BSV language (Bluespec SystemVerilog), which is founded on composable Atomic Transactions (atomic rewrite rules), and on ideas from Haskell on types and parameterization. This talk is about how we are slowly finding the vocabulary to communicate these ideas effectively to the hardware design community, by relating them to their everyday work. The core idea is to appeal to "control adaptivity". First, we show how atomic transactions are simply a higher-level way to specify control circuitry that one has to specify explicitly (and laboriously) when using RTL languages like Verilog or VHDL, and that this is valuable, in of itself, in describing circuits with complex control. Next, we demonstrate the benefits of automatic synthesis of this hardware in accommodating change. Change is an everyday requirement for a number of reasons: bug fixing; specification evolution; refinement from abstract models to implementations; reimplementation for different area, performance and power targets, and so on. Finally, control-adaptivity is also a requirement for designs that, through parameterization, unfold to different microarchitectures, each of which requires a different control regime.

Robby Findler, PLT Redex: test case generation. (Mon 2008-06-16, 10:25)

PLT Redex is a embedded domain-specific language for specifying operational semantics designed to support experimentation in the early stages of the design of a new calculus. Roughly speaking, write down a grammar and a reduction relation (possibly with a few metafunctions), given Redex a term and it will show you the graph reachable from the term. Thanks to John Hughes, I've been inspired to look into automatically generating test examples to provide a lightweight test of various properties of the reduction system. This talk gives a demo-based intro to Redex and showed the (preliminary) support for test case generation.

Norman Ramsey, Dataflow ``Optimization'' for the Semantically Inclined. (Mon 2008-06-16, 11:35)

The professional literature on code improvement (aka 'optimization') relies largely on iterative dataflow analysis and mutation of imperative data structures representing the program being improved. Little attention is paid to foundations, and the field is littered with terms of art that are confusing when not actually misleading---a real turnoff. By looking at this material through the lens of functional programming and programming-language semantics, we can make it simpler, more pleasant to talk about, and easier to implement:

• If we are suitably inspired by Hoare logic, we can explain most code-improving transformations as substitution of equals for equals. The most important other transformation is the removal of unused assignments, which is analogous to dropping a let binding in which the bound variable does not appear free in the body.

• Dataflow analysis is simply the solution of a set of recursion equations that relate assertions at nearby program points. The recursion equations involve either weakest (liberal) preconditions, which describe "backward dataflow problems", or strongest preconditions, which describe "forward dataflow problems."

• A key technique is to use only very simple, inexpressive logics, so that a fixed point always exists and can be reached quickly. For example, the logic for "constant propagation" can express only conjunctions of claims that a variable is equal to a constant; the logic for "copy propagation" can express only conjunctions of claims that two variables are equal. When control flow requires the disjunction of two assertions (e.g., at a join point in the control-flow graph), the disjunction is weakened to the strongest expressible predicate implied by the disjunction. For example, (x = y and z = w) or (x = z and z = w) is weakened to z = w.

Rinus Plasmeijer, Ajax and Client-Side Evaluation of i-Tasks. (Mon 2008-06-16, 14:00)

The iTask system is a recently developed toolkit with which workflows can be defined declaratively on a very high level of abstraction (see ICFP 2007). It offers functionality which cannot be found in commercial workflow systems: workflows are constructed dynamically depending on the outcome of earlier work, workflows are strongly typed, and they can be of higher order. From the specification, a web-based multi-user workflow system is generated. Up until now we could only generate thin clients. All information produced by a worker triggers a round trip to the server. For real world workflows this is unsatisfactory. Modern Ajax web technology to update part of a web page is required, as well as the ability to execute tasks on clients. The architecture of any system that supports such features is complex: it manages distributed computing on clients and server which generally involves the collaboration of applications written in different programming languages. The new version of iTasks allows to integrate partial updates of web pages and client side task evaluation within the iTask system, while retaining its approach of a single language and declarative nature. The workflow designer uses light-weight annotations to control the run-time behavior of work. The iTask implementation takes care of all the hard work under the hood. Arbitrary tasks (functional programs) can be evaluated at web clients. When such a task cannot be evaluated on the client for some reason, the system automatically switches to server side evaluation. All communication and synchronization issues are handled by the extended iTask system.

Kathleen Fisher, Improving Undergraduate Programming Language Curriculum. (Mon 2008-06-16, 14:50)

In this talk, I summarize the results of the two-day Programming Language Curriculum Workshop held May 29-30 at Harvard University in Boston. The 30 workshop participants discussed the questions of 1) what we teach undergraduate computer science majors about programming languages, 2) why that material is important to a broad audience, and 3) how we recommend it should be taught. Participants recommended that the current ACM curriculum be amended to replace 10 hours of required programming fundamentals and programming language topics with 10 hours of functional programming. The ACM has tentatively adopted this recommendation, which has been published to the ACM community for comment until July 1st. If the proposal is adopted, there will be a large number of schools needing to modify their curriculum to include functional programming. I argue that this circumstance presents an opportunity for us in the functional programming community to provide appropriate materials to help ensure that these 10 hours of functional programming instruction are of high quality. Workshop participants will publish a report on their findings in the November 2008 issue of SIGPLAN Notices. In addition, SIGPLAN will be forming an education board to continue the process of building community consensus on the topic of undergraduate programming language education. The participation of community members is crucial to make this entire effort a success. The url for the workshop is: http://www.sigplan.org/pl-workshop. The url for the ACM page soliciting comments on the curriculum proposal is: http://wiki.acm.org/cs2001/index.php.

Matthew Flatt, Leveraging Macros for Documentation. (Mon 2008-06-16, 16:05)

An extensible programming language offers special challenges and opportunities for documentation. The central challenge is that bindings --- even seemingly core bindings like `lambda' --- can mean different things in contexts that use different language extensions. At the same time, rich extensibility confers the opportunity to write documentation itself in a language that is adapted to the needs of writing prose, specifying language constructs, showing examples, and cross-referencing extensively --- and if more facilities are needed, then the documentation language itself is extensible. In this talk, we describe Scribble, which is a tool and an extensible language that is used to document libraries and languages with PLT Scheme.

Mary Sheeran, Finding good prefix networks using Haskell. (Mon 2008-06-16, 17:00)

Prefix networks are important both in circuits and in parallel programming. They give a way to perform an apparently sequential computation quickly by exploiting parallelism. Prefix networks are, for example, used to compute the carries in fast adders, and such adders are often the hot spots in microprocessors. We need new ways to design these networks, taking power consumption into account. There are many standard prefix networks, usually named by the two authors who invented them (Ladner Fischer, Brent Kung, Kogge Stone). I presented my attempts at using dynamic programming (in Haskell) to find fast, low power, prefix networks. Initially, I minimised number of operators for a given depth, and with constrained fanout. A first approach produced depth-size optimal (DSO) networks by construction. A further generalisation produced networks with few operators and minimum depth, even in cases where DSO networks do not exist. The presented method gives networks that are in many cases better (that is have fewer operators or smaller fanout for a given depth) than those currently known. Using depth as a measure of circuit speed, and number of operators as a measure of power consumption turns out to be a good first approximation. The accuracy of estimation of speed and power could then be improved by repeated calls. during the search, to the recently developed Wired system (Axelsson's wire-aware design system, embedded in Haskell). In the search, we now minimise speed along the critical path of the network, and power elsewhere. The use of Wired allows the production of real standard-cell based circuit layouts via a link to a commercial CAD tool. We have not produced any break-through results here yet, but it is now very easy to explore the design space. Yet more physical details (such as buffering of long wires and sizing of cells) must be included to give truly practical VLSI circuits. So much work remains to be done. I suspect, though, that the search method could be used in other contexts, for instance in generating data parallel programs.

Chris Okasaki, Gembots - A Programming Game. (Tue 2008-06-17, 08:30)

I've developed a board game called Gembots that is intended to help teach simple programming skills, including loops and conditionals. Players program robots to maneuver around the board, picking up gems along the way. I hope to hold a small tournament at the meeting, with a copy of the game Monad, by Sid Sackson, as the grand prize.

Andres Löh, NixOS. (Tue 2008-06-17, 09:10)

Existing package and system configuration management tools suffer from an imperative model, where system administration actions such as upgrading packages or changes to system configuration files are stateful: they destructively update the state of the system. This leads to many problems, such as the inability to roll back changes easily, to run multiple versions of a package side-by-side, to reproduce a configuration deterministically on another machine, or to reliably upgrade a system. We can overcome these problems by moving to a purely functional system configuration model. This means that all static parts of a system (such as software packages, configuration files and system startup scripts) are built by pure functions and are immutable, stored in a way analogously to a heap in a purely function language. We have implemented this model in NixOS, a non-trivial Linux distribution that uses the Nix package manager to build the entire system configuration from a purely functional specification.

Andrew Tolmach, Proof Technology for High-Assurance Run-time Systems. (Tue 2008-06-17, 10:35)

It seems obvious that the reliability of critical software can be improved by using high-level, memory-safe languages (Haskell, ML, Java, C#, etc.). But most existing implementations of these languages rely on large, complex run-time systems coded in C. Using such an RTS leads to a large "credibility gap" at the heart of the assurance argument for the overall system. To fill this gap, we are working to build a new high-assurance run-time system (HARTS), using an approach grounded in machine-assisted verification. A primary goal of the HARTS project is to produce mechanized correctness proofs for realistic garbage collector implementations. To achieve this goal, we need practical tools for mechanized reasoning about low-level, pointer-based, imperative programs. This talk is about our experience searching for, evaluating, and ultimately building our own versions of such tools within the Coq proof assistant. In particular, we are currently developing a new proof framework (based on recent work at Yale and INRIA) that supports separation logic on a deep embedding of the implementation language. We are successfully using this framework to verify collectors that can be integrated with an existing certified compiler (developed at INRIA) and linked against code generated from Haskell-like source languages. The talk will describe our framework, integration approach, and collector proofs. (This is joint work with Andrew McCreight.)

Konrad Slind, Compiling from Higher Order Logic. (Tue 2008-06-17, 11:40)

We discuss a proof-producing compiler that translates a subset of HOL to ARM machine code.

Phil Wadler, Well-typed programs can't be blamed. (Tue 2008-06-17, 14:10)

We introduce the blame calculus, which adds the notion of blame from Findler and Felleisen's contracts to a system similar to Siek and Taha's gradual types and Flanagan's hybrid types. We characterise where positive and negative blame can arise by decomposing the usual notion of subtype into positive and negative subtyping, and show that these recombine to yield naive subtyping. Naive typing has previously appeared in type systems that are unsound, but we believe this is the first time naive subtyping has played a role in establishing type soundness. (Philip Wadler and Robby Findler)

Arvind, Discussion: Why formal verification remains on the fringes of commercial development. (Tue 2008-06-17, 15:05)

Francois Pottier, Hiding local state in direct style: a higher-order anti-frame rule. (Tue 2008-06-17, 16:15)

Separation logic involves two dual forms of modularity: local reasoning makes part of the store invisible within a static scope, whereas hiding local state makes part of the store invisible outside a static scope. In the recent literature, both idioms are explained in terms of a higher-order frame rule. I point out that this approach to hiding local state imposes continuation-passing style, which is impractical. Instead, I introduce a higher-order anti-frame rule, which permits hiding local state in direct style.

Steve Zdancewic, Aura: A Programming Language with Authorization and Audit. (Tue 2008-06-17, 17:15)

Existing mechanisms for authorizing and auditing the flow of information in networked computer systems are insufficient to meet the security requirements of high-assurance software systems. Current best practices typically rely on operating-system provided file permissions for authorization and an ad-hoc combination of OS and network-level (e.g. firewall-level) logging to generate audit trails. This talk will describe ongoing work on a security-oriented programming language called Aura that attempts to address this problem of auditable information flows in a more principled way. Aura supports a built-in notion of principal and its type system incorporates ideas from authorization logic and information-flow constraints. These features, together with the Aura run-time system, enforce strong information-flow policies while generating good audit trails. These audit trails record access-control decisions (such as uses of downgrading or declassification) that influence how information flows through the system. Aura's programming model is intended to smoothly integrate information-flow and access control constraints with the cryptographic enforcement mechanisms necessary in a distributed computing environment.

Don Syme, F# Asynchronous Reactive Programming. (Wed 2008-06-18, 08:30)

Koen Classen, A Library Approach to Information Flow Security in Haskell. (Wed 2008-06-18, 09:30)

We present a monad-based library for information-flow security in Haskell.

Dave Walker, Language support for processing distributed ad hoc data. (Wed 2008-06-18, 10:45)

The term ad hoc data refers to the untold billions upon billions of bytes of non-standard, unreliable, and continuously evolving data spread across all computer systems. This sort of data includes such varied sources as server logs, distributed systems performance and debugging data, automated billing systems information, telephone call records, financial data and online repositories of scientific data including genetic information, cosmology data and global weather systems data. This talk describes a system for automatic generation of monitoring, analysis and transformation tools for such distributed ad hoc data. Our generated tools include data archiving system, a database loading system, a system for tracking the statistical profile of the data and generating alerts under customizable error conditions, an RSS feed generator, and a simple query tool. The system also generates a number of libraries for application developers, including those for parsing, printing, error management, data traversal and transformation. Software developers can use the programming framework to create their own new application-specific tools or more general generic tools that can be applied to any collection of data sources. The tool suite is generated from high-level data descriptions written in a domain-specific programming language called PADS/D. To use the language, programmers specify where their ad hoc data is located, when to get it, how to obtain it, and what preprocessing the system should do when it arrives. As its name suggests, PADS/D is layered on top of the PADS sublanguage, developed in previous research efforts, for specification of the {\em format} of the data sources. We illustrate the expressiveness of PADS by providing descriptions for several different distributed systems including CoMon, PlanetLab's node and experiment monitoring system, and AT&T's web hosting service.

John Peterson, Functional Reactive Python: On Introducing CS to High School Students. (Wed 2008-06-18, 11:35)

This talk describes an implementation of FRP (Functional Reactive Programming) in Python for a game engine. This is used in a camp for high school students.

Ralf Hinze, Category-Partial Orders and Proof Principles. (Thu 2008-06-19, 08:30)

We introduce category-partial orders, a blend of categories and partial orders, and study proof principles in this setting. In particular, we show that `case analysis' and `induction' follow from the universal property of initial objects.

Corky Cartwright, OOP as an Enrichment of FP. (Thu 2008-06-19, 09:25)

At Rice University, we have taught functional programming (FP) in Scheme in our first semester programming course for the past two decades. Over ten years ago, when we converted our second semester course from object-based programming (OBP) in C++ to object-oriented programming (OOP) in Java, we discovered that object-oriented program design and functional programming design are intimately connected. In both FP and OOP:

1. Most program data is algebraic; it has a simple inductive definition as trees.
2. The structure of a program should mirror the form of data that it processes.

Moreover, for every functional program, there is a corresponding object-oriented program derived from the functional program using appropriate design patterns. The resulting OO program is still functional in the sense that all data objects are immutable.

Since the OO programming model is more complex that the functional one, we advocate teaching the rudiments of functional programming before teaching object-oriented design. Moreover, OO design pedagogy should initially focus on programming with immutable data using the design patterns that elegantly encode standard programming techniques from functional programming. The patterns include composite, interpreter, singleton, strategy, factory method, and visitor patterns. Students should learn that there is an OO analog for every abstraction in FP. In Java and C#, the connection is particularly compelling because Java and C# supports closures in the form of anonymous inner classes and anonymous delegates, respectively. Once students have mastered ''functional programming'' in Java or C#, it is natural to introduce object mutation using the state, iterator, observer, and model-view-controller patterns.

A pedagogic IDE such as DrJava (see drjava.org) can greatly simplify the complexity of writing ''functional'' OO programs by autogenerating the methods implied in the definition of algebraic data, just as the define-struct operation in Scheme autogenerates all of the operations (constructors, selectors, and structural equality) for Scheme structures. The autogeneration process is natural because the generated code exactly matches what a competent OO programmer would produce to fully implement an algebraic data type. In fact, we believe that professional IDEs should offer similar support. As students learn more about the full Java or C# language, they easily learn to write the autogenerated code on their own (although this aspect of Java and C# adds to clerical burden involved in writing ''functional'' OO programs.

Bob Harper, Focusing on Binding and Computation. (Thu 2008-06-19, 10:45)

We present an integration of logical frameworks and functional programming using the techniques of focusing and contextual modal type theory.

Jack Dennis, Composable Parallel Programming. (Thu 2008-06-19, 11:40)

An attempt at a presentation aimed at showing how present multiprocessor computer systems fail to support the use of parallel programs to construct larger parallel programs.

Implementing Associative Memories using B-Trees.

Associative memories play an important role in the Fresh Breeze multi-core architecture. I recently noticed that the B-Tree data structure used in the database area provides an attractive approach to building large hardware associative memories. This talk explains the approach.

Stephanie Weirich, FPH: First-class polymorphism for Haskell. (Thu 2008-06-19, 14:30)

Languages suupporting polymorphism typically have ad-hoc restrictions on where polymoprhic types may occur. Supporting ''first-class'' polymorphism, by lifting those restrictions, is obviously desirable, but it is hard to achieve this without messing up type inference. We present a new type system for higher-rank and impredicative polymoprhism that improves on earlier proposals: it is an extension of Damas-Milner; it relies only on System F types; it has a simple, declarative specification; it is robust to program transformation; and we give a complete and decidable type inference algorithm.

Dave McQueen, Modules and Type Classes. (Thu 2008-06-19, 14:55)

Andrew Tolmach, Who needs call-by-need? (Thu 2008-06-19, 08:30)

There has been much recent discussion on the merits of a language that supports both call-by-value and call-by-need. But perhaps it would be better to support call-by-value and call-by-name instead.

Ralf Hinze, Solution to Puzzle. (Fri 2008-06-20, 08:35) See slides.

Didier Remy, What (Fri 2008-06-20, 08:55)

We present a variant of the explicitly-typed second-order polymorphic lambda-calculus with primitive open existential types, i.e. a collection of more atomic constructs for introduction and elimination of existential types. We equip the language with a call-by-value small-step reduction semantics that enjoys the subject reduction property. We claim that open existential types model abstract types and type generativity in a modular way. Our proposal can be understood as a logically-motivated variant of Dreyer's RTG where type generativity is no more seen as a side effect.

Fritz Henglein, What is a Sorting Function? (Fri 2008-06-20, 09:40)

Ordered abstract types should be equipped with a sorting (or discriminator) function instead of a comparison function to enable time-efficient sorting for composed types. But how we recognize that an alleged such function really defines an ordering relation? We show define the notions of parametric and stable permutation functions and demonstrate that all sorting algorithms implement parametric permutation functions. This provides an intrinsic definition of (stable) sorting function, without reference to a given ordering relation, and conversely allows deriving a comparison function (as opposed to the other way round) and ensuring that that really yields the charasteric function of an ordering relation and that the given function really is stable over that ordering.

Koen Claessen, Solution to Puzzle. (Fri 2008-06-20, 11:00) See Haskell source.

Bob Harper, Interpreter for System T in System F. (Fri 2008-06-20, 11:25)

Simon Peyton Jones, one minute plug. (Fri 2008-06-20, 11:45)

Simon and Dorothy's 100th birthday ride 500 mile cycle ride in Vietnam in November, supporting the Medical Foundation for the Care of Victims of Torture (http://www.justgiving.com/pj-vietnam).

Lennart Augustsson, Haskell binding for LLVM. (Fri 2008-06-20, 11:50)

Phil Wadler, Visual Lambda Calculus. (Fri 2008-06-20, 12:05)

Bret Victor designed a visual representation of lambda calculus called `Alligator Eggs', which has been implemented under my direction by Stuart Gundry and Francesco Figari. The implementation has seven primitives, three for lambda calculus (abstract, apply, variable) and four for creating graphics (overlay, empty, unit square, tansform). An interesting question is what set of pictures can be created with these primitives. Is it complete in some sense, or is there a similar set which is complete?