Workshop on Datatype-Generic Programming
The Datatype-Generic Programming project at Oxford
and Nottingham is hosting an informal workshop on 3rd and 4th June 2004.
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.
We're planning a small registration fee (15 pounds) to cover lunches and
coffees. Please let me know if you have special dietary requirements. The
workshop has been made an APPSEM-affiliated event, so those of you
with APPSEM funding can spend it on this.
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.
Thursday 3rd June
(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.)
(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.
(The thesis on
which the talk is based is also available.)
In the talk, not only positive results will be presented but also some
possible alternative solutions together with the reasons why they were not
(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.
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
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.
(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
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.
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.
(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.
(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
(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?
(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)
(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.
(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.
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.
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.)
(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.
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).
28th May 2004