Workshop on Datatype-Generic Programming

The scope of the workshop is the scope of the project, namely, techniques for reasoning about and implementing programs that are parametrized by a datatype. Think Algebra of Programming, PolyP, Generic Haskell, Scrap your Boilerplate, Template MetaHaskell, Dependent Types, etc.

Participation is by invitation only, but let me know if you think you should be invited.

Details

If you need accommodation, I recommend booking it soon-ish. Details are available online. The workshop itself will take place in Room 051 at OUCL.

Those who are around can meet on the Wednesday evening before the workshop, in the Royal Oak pub at 44 Woodstock Road; I'll be there from about 8pm. (They serve decent food, too, if you're looking for dinner.) We plan to go out to Chez Gaston (a creperie) on North Parade Avenue on the Thursday evening; I'll circulate information nearer the time.

Timetable

Thursday 3rd June

09:00-09:45

Ralf Hinze (University of Bonn): Typed type representations

The recent years have seen a number of proposals for embedding generic definitions in mainstream programming languages. Type representations are at the heart of these embeddings. A type representation is simply a type whose elements represent types. This talk reviews several type representations and shows how to simulate generic definitions within Haskell 98 (sans any extensions).

(There is also a paper available.)

09:45-10:30

Ondrej Rypacek (Charles University, Prague): Polytypic Programming in the Context of Logic Programming

This talk introduces a language extension of a parametrically typed Prolog for writing polytypic predicates over the large class of regular types. Polytypic predicates are defined as templates for predicates, which are similar to predicates over some sort of generic datatype. From the template, a specific variant (instance) of the predicate can be generated by induction on the structure of the type, which is modeled in a dedicated type system. The generated predicate is a standard Prolog predicate over the type similar to what the programmer would have written by hand. Polytypic instances are thus expanded and type-checked at compile-time with no overhead at runtime and can be subject to further program transformation and optimization. The extension allows for writing both purely generic polytypic predicates, such as maps or folds, and also specific polytypic predicates over a limited set of data types.

In the talk, not only positive results will be presented but also some possible alternative solutions together with the reasons why they were not found appropriate.

(The thesis on which the talk is based is also available.)

10:30-11:00

Coffee

11:00-11:45

Pablo Nogueira (University of Nottingham): Polytypic Programming and Data Abstraction

I will give a briefing of ongoing work on my thesis. The main thread is reconciling polytypic programming with data abstraction. Polytypic programs work over the definitional structure of concrete type definitions. As expected, polytypic functions are sensible to implementation changes, to junk, and can break the implementation invariants and the semantics of abstract data types (ADTs). One traditional solution is for the ADT implementor to provide some form of traversal (eg, Iterators in the C++ STL). Another possibility is for the ADT implementor to provide views a la Wadler, though views have their own problems. Alternatively, we can also construct other sorts of views by means of the operations of the ADT's interface. Polytypic functions would work over this abstract definitional structure (which provides a "shape") and would be instantiated for specific ADTs. These views can be provided by the ADT users, not implementor, based on the signature and laws (the latter play an important role in correctness).

A second thread is the possible uses and applications of our syntax formalism EONF to generic programming. EONF is a sort of first-order context-free grammar defining simultaneously language-independent types (accurate abstract syntax), parsers (concrete syntax) and traversal definitions.

11:45-12:30

Annabelle McIver (Macquarie University): Probabilistic program algebra

The specification and analysis of probabilistic distributed algorithms is particularly difficult because of the interaction between nondeterminism (due to underspecification of an "adversary scheduler") and probablistic choice. Current methods of analysis are often based on model checking, and consequently suffer from the "state-space explosion" problem.

An attractive alternative is the use of algebraic methods which can establish equivalences of the original system with a "serialised" specification in which complex distributed actions can essentially be treated as atomic. The overall effect is to simplify an analysis of a system to checking small "commutativity" type assumptions needed for the algebraic proofs.

In this talk we will show how a suitable weakening of Kozen's axiomatic system for Kleene algebra with tests can be used to prove such general theorems about probabilistic systems. We shall explain why the axioms need to be weakened, and illustrate the resulting probabilistic axiom system with some examples.

12:30-14:00

Lunch

14:00-14:45

Bruno Oliveira (University of Oxford): The Algebra of Programming in Haskell

In the Algebra of Programming book we are shown how to calculate programs with an approach based on a categorical calculus of relations. The theory presented in the book is general enough to capture interesting recursion patterns, which can be parameterized by a datatype.

In this work, we will present a Haskell library that can be used to implement some of the theory presented. In particular, we will show how could we implement the morphisms (ana, cata, hylo) for regular types without restriction on the kind.

14:45-15:30

Manuel Alcino Cunha (University of Minho): Point-free Programming with Hylomorphisms

The objective of this paper is twofold. First, we present, in the category Cpo, an unified approach to the definition of recursion patterns based on the concept of hylomorphism. Using this recursion operator, we show how folds, unfolds, and other less known recursion patterns can be defined, and how to derive the fundamental laws that characterize them without resorting to fixpoint induction. We also show how to implement a library in Haskell that enables a straightforward encoding of all these definitions in a truly point-free and polytypic style.

15:30-16:00

Tea

16:00-16:45

Conor McBride (University of Durham): Introduction to Epigram

By directly supporting the abstraction of type families over data, dependent types provide, at least in principle, a natural setting in which to program generically. Systematic activity at the type level requires no new programming technology beyond what we already use for terms. But are dependent types inevitably too complex to work with in practice? Or is it just that we need to find better ways of working?

Epigram is a dependently typed functional programming language, based on joint work with James McKinna (The view from the left, JFP 14(1)). It comes with an interactive programming environment which supports type-directed problem decomposition, exploiting the contribution made in stating a type towards developing a program which inhabits it. Problem decomposition tactics are themselves expressed by types and implemented by first-class values. Epigram is an attempt to investigate what programming can become, given a language of types articulate about programs and data. This talk provides the background for Thorsten's talk and is, besides, an invitation to join the fun.

16:45-17:30

Thorsten Altenkirch (University of Nottingham): Programming with Universes

In Type Theory a universe is given by a type of names for data, D:*, and a family of types, Val : D -> *, which assigns a type of values to the name of a type. This is a natural setting in which generic programs and proofs can be developed. Compared to conventional approaches to generic programming it has the essential advantage that we can adjust the scope of genericity by choosing different universe. We will discuss this approach based on examples developed with Conor McBride's epigram system.

Friday 4th June

09:00-09:45

Eerke Boiten (University of Kent at Canterbury): Finding Functors in Relational Abstract Data Types

Generic functional programming is based on the idea of functors for data structures. In order to import such ideas into the world of relational abstract data types, "functors" need to be identified. From how they operate on state spaces, can we extrapolate to operations and full ADTs? Most importantly, are they monotonic with respect to refinement?

09:45-10:30

Keean Schupke (Imperial College, London): Strongly typed heterogeneous collections

A heterogeneous collection is a datatype that is capable of storing data of different types. Such a datatype provides operations for look-up, update, iteration, and others. There are various kinds of heterogeneous collections, differing in representation, invariants, and access operations. We describe HList - a Haskell-based library for strongly typed heterogeneous collections. We illustrate heterogeneous collections in the context of type-safe database access in Haskell. The development of HList relies on some common extensions of Haskell 98, and it raises some interesting issues regarding Haskell's type system.

Joint work with Oleg Kiselyov (Naval Postgraduate School, Monterey) and Ralf Laemmel (CWI and Vrije Universiteit, Amsterdam)

10:30-11:00

Coffee

11:00-11:45

Huiqing Li (University of Kent at Canterbury): HaRe: The Haskell Refactorer

Refactorings are meaning-preserving source-to-source program transformations, usually with the goal to implement design-level changes at the level of program source code. HaRe, our prototype refactoring tool for Haskell, implements more than a dozen refactorings, including renaming, scope change, generalisation, moving a definition between modules and a number of others, and are module aware. In this talk, we will give a brief overview of the current status of HaRe, user-level features, implementation, current work and future directions.

11:45-12:30

Ian Lynagh (University of Oxford): Template Haskell and Generic Programming

In this talk I will first give a brief introduction to Template Haskell, an extension to Haskell for meta-programming. The introduction will not assume familiarity with Template Haskell, but I will highlight the changes from the original implementation for the benefit of those who have looked at it in the past.

I will then give a brief overview of the general styles in which Template Haskell can be used before going into some detail on how one can do datatype generic programming with Template Haskell by showing how Haskell's "deriving Show" can be implemented with it.

12:30-14:00

Lunch

14:00-14:45

Ralf Laemmel (CWI, Amsterdam): Scrap read, show, eq, and friends

The prime application of the "Scrap your boilerplate" approach to generic programming in Haskell is traversal over rich data structures, such as syntax trees or terms that represent XML documents. These traversals normally implement problem-specific transformations or queries on the data structures. The best-known applications of generic programming (such as serialisation, de-serialisation, and generic equality) are of a different kind. We show that such generic functions can be supported on the basis of a reflection API for Haskell datatypes.

This is joint work with Simon Peyton Jones. More information is available from the web site.

14:45-15:30

Simon Peyton Jones (Microsoft Research, Cambridge): Generic function extension in scrap-your-boilerplate

The scrap-your-boilerplate approach to generic programming allows the programmer to extend a generic function with arbitrary type-specific cases. However, the extension mechanism of the original paper was rather limited.

In this talk I'll explain how function extension works, and describe some interesting and (to us at least) non-obvious generalisations. In particular, I'll show how to make polymorphic function extensions.

All this is joint work with Ralf Laemmel. (The PDF file is 6Mb+; you may prefer the smaller Powerpoint file.)

15:30-16:00

Tea

16:00-16:45

Michael Abbott (University of Leicester): Categories of Containers

We introduce the notion of containers as a mathematical formalisation of the idea that many important datatypes consist of templates where data is stored. We show that containers have good closure properties under a variety of constructions including the formation of initial algebras and final coalgebras. We also show that containers include strictly positive types and shapely types but that there are containers which do not correspond to either of these. Further, we derive a representation result classifying the nature of polymorphic functions between containers.

16:45-17:30

Johan Jeuring (Utrecht University): Overview of work in the Generic Haskell project

I will give an overview of the activities within the Generic Haskell project (UUXML, type isomorphisms, partial evaluation, views, Andres Loeh's work).