Papers

Papers accepted for WGP 2009 (including prel. abstracts)

Papers are in the order of the Programme and the Proceedings.

Wendy Verbruggen, Edsko de Vries and Arthur Hughes.
Abstract: We formalize proofs over Generic Haskell-style polytypic programs in the proof assistant Coq. This makes it possible to do fully formal (machine verified) proofs over polytypic programs with little effort. Moreover, the formalization can be seen as a machine verified proof that polytypic proof specialization is correct with respect to polytypic property specialization.

Jyrki Katajainen and Bo Simonsen.
Abstract: The CPH STL is a special edition of the STL, the containers and algorithms part of the C++ standard library. The specification of the generic components of the STL is given in the C++ standard. Any implementation of the STL, e.g.~the one that ships with your standard compliant C++ compiler, should provide at least one realization for each container that has the specified characteristics with respect to speed and safety. In the CPH STL project, our goal is to provide several alternative realizations for each STL container. For example, for associative containers we can provide almost any kind of balanced search tree. Also, we do provide safe and compact versions of each container. To easy the maintenance of this large collection of implementations, we have developed component frameworks for the STL containers. In this paper, we describe the design and implementation of a component framework for vector, which is the most useful container in the C++ standard library. In particular, we specify the details of a vector implementation that is safe with respect to referential integrity and strong exception safety. Additionally, we report the experiences and lessons learnt from the development of component frameworks which we hope to be of benefit to persons engaged in the design and implementation of generic software libraries.

Daniel Lincke and Sibylle Schupp.
Abstract: Higher-order functions are essential for generic programming. While they are naturally supported in functional programming languages, there are no higher-order functions in C++. There, various function datatypes exist that simulate the effect of higher-order programming in different ways---as classes designed in the imperative, object-oriented, or meta-programming spirit. With the recent addition of concepts, another alternative for supporting parameterization by functions has yet become available. No guidelines exist, however, whether, or when, to prefer a concept for functions over any of the existing function datatypes; nor have the function datatypes themselves been compared. We provide an empirical study that assesses performance, expressivity, and convenience. The study shows that the concept is faster and at least as expressive as the best function datatype, but, due to the principal difference between concept- and type-based approaches, also less convenient to use.

Meng Wang and Bruno Oliveira.
Abstract: Aspect-Oriented Programming (AOP) aims at modularising crosscutting concerns that show up in software. The success of AOP has been almost viral and nearly all areas in Software Engineering and Programming Languages (SE&PLs) have become `infected' by the AOP bug in one way or another. Interestingly the functional programming community (and, in particular, the pure functional programming community) seems to be resistant to the pandemic. The goal of this paper is to debate the possible causes of the functional programming community resistance and to raise awareness and interest by show casing the benefits that could be gained from having a functional AOP language. At the same time, we identify the main challenges and explore the possible design-space.

Yu David Liu, Christian Skalka and Scott Smith.
Abstract: Staging is a powerful language construct that allows a program at one stage to manipulate and specialize a program at the next. We propose <ML> as a new staged calculus designed with novel features for staged programming in modern computing platforms such as embedded systems. A distinguishing feature of <ML> is a model of process separation, whereby different stages of computation are executed in different process spaces. Our language also supports dynamic type specialization, via type abstraction, dynamic type construction, and a limited form of type dependence. <ML> is endowed with a largely standard metatheory, including type preservation and type safety results. We discuss the utility of our language via code examples from the domain of wireless sensor network programming.

Eelco Lempsink, Sean Leather and Andres Loeh.
Abstract: We present patch and diff functions that are generic over families of datatypes. The edit scripts are represented as values in a type-indexed datatype, and both computing and applying edit scripts is entirely type-safe. Our approach extends classic string diff and tree diff algorithms by providing more informative types. We have working implementations in Agda and Haskell.

Roland Backhouse, Richard Bird and Paul Hoogendijk.
Abstract: The "fan" of a datatype F is a relation that holds between a value x and an arbitrary F structure in which the only stored value is x. Fans make precise the notion of the shape of a data structure. We formulate two different representations of shape selectors and exploit the properties of fans to prove that the two representations are order isomorphic and that shape selectors are closed under set intersection. For arbitrary datatypes F, G and H, we consider six different ways of composing their fans in order to construct F structures of G structures of H structures; each of the six imposes a different requirement on the shape of the substructures. We catalogue the relation between different combinations of the constructions. We apply the result to a problem that arose in a generic theory of dynamic programming concerning the shape properties of a natural transformation from G structures to FG structures.

Jeremy Gibbons and Ross Paterson.
Abstract: Datatype-generic programs are programs that are parametrized by a datatype or type functor: whereas polymorphic programs abstract from the "integers" in "lists of integers", datatype-generic programs abstract from the "lists of". There are two main styles of datatype-generic programming: the Algebra of Programming approach, characterized by structured recursion operators arising from initial algebras and final coalgebras, and the Generic Haskell approach, characterized by case analysis over the structure of a datatype. We show that the former enjoys a kind of higher-order naturality, relating the behaviours of generic functions at different types; in contrast, the latter is more ad hoc, with no coherence required or provided between the various clauses of a definition. Moreover, the naturality properties arise "for free", simply from the parametrized types of the generic functions: we present a higher-order parametricity theorem for datatype-generic operators.