Workshop on Generic Programming

Thursday 26th July 2001

University of Nottingham

The Workshop on Generic Programming is an informal one-day event for the discussion of recent and ongoing developments in the area of generic programming. The workshop is open to all, and there is no charge for attending. Please contact the organiser, Graham Hutton, if you would like to attend.

Participants

The list of participants is as follows:

Thorsten Altenkirch University of Nottingham

Roland Backhouse University of Nottingham

Ian Bailey University of Oxford

Edwin Brady University of Durham

Paul Callaghan University of Durham

Kieran Clenaghan University of York

Roy Crole University of Leicester

Sharon Curtis University of Stirling

Neil Ghani University of Leicester

Jeremy Gibbons University of Oxford

Ralf Hinze University of Utrecht

Yorck Hunke University of Oxford

Graham Hutton University of Nottingham

Johan Jeuring University of Utrecht

Clare Martin Oxford Brookes University

Conor McBride University of Durham

Simon Peyton Jones Microsoft Research Cambridge

Silvija Seres University of Oxford

Joel Wright University of Nottingham

Wang Yanbing University of Nottingham

Programme

The workshop will run from 10am to around 5pm, with breaks for coffee and lunch. I've made a reservation for lunch at Cafe Terrazo on the campus, but you'll have to pay for your own lunch (around 3-5 pounds). After the workshop there will be a BBQ at Roland's house starting at around 6pm, for those who can stay a little longer or are staying overnight. Roland's house is around 10-15 minutes by taxi from the railway station.

An overhead projector and a data projector linked to a PC (with Powerpoint 97 installed) will be available for presentations, and it will also be possible to connect a laptop to the data projector.

10.00 - 10.30: Ralf Hinze, University of Utrecht
Functorial unparsing (paper, slides)
Danvy has shown how to implement a variant of C's `printf' function in a statically typed language. We present a new solution to this problem based on the notion of a functor. Our solution enjoys nice algebraic properties and is more direct than the original one. Along the way, we encounter singleton types, type-indexed values, type-indexed types, multiple-parameter type classes, and functional dependencies.

10.30 - 11.00: Thorsten Altenkirch, University of Nottingham
Towards a semantics of generic programming
I will put forward some ideas about how to model generic programs categorically. Many (but not all) generic programs can be understood as folds/unfolds in a category of families. Maybe this gives rise to the view that generic is not the same as adhoc.

11.00 - 11.30: Coffee

11.30 - 12.00: Sharon Curtis, University of Stirling
Generic greedy algorithms
Looking at how generic programming concepts do and don't help produce greedy algorithms in the world of relational programming.

12.00 - 12.30: Silvija Seres, University of Oxford
Higher-order transformation of logic programs (paper)
It has earlier been assumed that a compositional approach to algorithm design and program transformation is somehow unique to functional programming. With this talk we hope to demonstrate that some of the same techniques and results are applicable to logic programming as well.

12.30 - 14.00: Lunch

14.00 - 14.30: Jeremy Gibbons, University of Oxford
When is a function a fold or an unfold? (paper, slides)
We present necessary and sufficient conditions for when a (partial or total) function can be expressed as a fold or an unfold. An earlier version of this talk was presented at CMCS2001 in April; since then, the arguments have been simplified considerably. Curiously, the results are much easier to prove in a relational setting, even though they apply only to functions and not to relations.

14.30 - 15.00: Roland Backhouse, University of Nottingham
Generic termination (paper, slides)
Generic programming is about parameterising programs by datatypes. The introduction of such parameters in the process of program construction opens up a new dimension for reasoning about programs. In this talk we consider how termination properties of programs are parameterised by datatypes. In particular, we compare several generalisations of the notions of well-foundedness and inductivity.

15.00 - 15.30: Coffee

15.30 - 16.00: Conor McBride, University of Durham
Universe constructions as a medium for generic programming
A `universe', in the sense of this talk, is a collection of types given by a type U of `codes' and a `decoding' function T from U to types. In a dependently typed setting, we can capture many collections of types over which we wish to define generic operations by universes whose U's are datatypes coding for exactly the types we intend. Correspondingly, systematic type-level behaviour can be implemented by `ordinary' programming over the U's. I will give some motivating examples, and discuss how Haskell might be extended to support this kind of technique.

16.00 - 16.30: Johan Jeuring, University of Utrecht
Type-indexed data types (paper)
A polytypic function is a function that can be instantiated on many datatypes to obtain datatype specific functionality. Examples of polytypic functions are the functions for digital searching, pattern matching, unification, rewriting, and structure editing. For each of these problems, we not only have to define polytypic functionality, but also a type-indexed data type: a data type that is constructed in a generic way from an argument datatype. This talk shows how to define type-indexed data types, discusses some examples of type-indexed data types, and discusses the specialization of type-indexed data types.

16.30 - 17.00: Closing

Travel

The workshop will be held at the following location:

Seminar Room C1
School of Computer Science
The University of Nottingham
Jubilee Campus, Wollaton Road
Nottingham NG8 1BB
United Kingdom

Online maps and directions to the Jubilee Campus are available here.

If you are arriving by train or bus, take a taxi to the University, which will take around 10-15 minutes. Make sure to ask for the Jubilee Campus on Wollaton Road, as the University has more than one campus.

If you are arriving by car, use the Wollaton Road entrance to the Jubilee Campus, and ask the security staff at the entrance to direct you to the free visitors car park nearby. Make sure not to park elsewhere, as all other spaces require a parking permit and are subject to stickering or clamping.

Accomodation

If you would like accomodation before or after the workshop, below are four suggestions, all of which are around 10-15 minutes by taxi from the train/bus stations and have availability on the 25th and 26th July. The first two are just a few minutes walk from the Jubilee Campus, while the remaining two are just a few minutes by taxi. If you require accomodation, please make your own arrangements.

P&J Hotel
227-229 Derby Road
Nottingham
Cost: approx 48 pounds per night
Tel : 0115-978 3998

Lucieville St James Hotel
349 Derby Road
Nottingham
Cost: approx 55 pounds per night
Tel : 0115-978 7389

The Hylands Hotel
307 Queens Road
Beeston
Nottingham
Cost: approx 40 pounds per night
Tel : 0115-925 5472

Priory Toby Hotel
Derby Road
Wollaton Vale
Nottingham
Cost: approx 52 pounds per night
Tel : 0115-922 1691

Thorsten Altenkirch	University of Nottingham
Roland Backhouse	University of Nottingham
Ian Bailey	University of Oxford
Edwin Brady	University of Durham
Paul Callaghan	University of Durham
Kieran Clenaghan	University of York
Roy Crole	University of Leicester
Sharon Curtis	University of Stirling
Neil Ghani	University of Leicester
Jeremy Gibbons	University of Oxford
Ralf Hinze	University of Utrecht
Yorck Hunke	University of Oxford
Graham Hutton	University of Nottingham
Johan Jeuring	University of Utrecht
Clare Martin	Oxford Brookes University
Conor McBride	University of Durham
Simon Peyton Jones	Microsoft Research Cambridge
Silvija Seres	University of Oxford
Joel Wright	University of Nottingham
Wang Yanbing	University of Nottingham

10.00 - 10.30:	Ralf Hinze, University of Utrecht Functorial unparsing (paper, slides) Danvy has shown how to implement a variant of C's `printf' function in a statically typed language. We present a new solution to this problem based on the notion of a functor. Our solution enjoys nice algebraic properties and is more direct than the original one. Along the way, we encounter singleton types, type-indexed values, type-indexed types, multiple-parameter type classes, and functional dependencies.
10.30 - 11.00:	Thorsten Altenkirch, University of Nottingham Towards a semantics of generic programming I will put forward some ideas about how to model generic programs categorically. Many (but not all) generic programs can be understood as folds/unfolds in a category of families. Maybe this gives rise to the view that generic is not the same as adhoc.
11.00 - 11.30:	Coffee
11.30 - 12.00:	Sharon Curtis, University of Stirling Generic greedy algorithms Looking at how generic programming concepts do and don't help produce greedy algorithms in the world of relational programming.
12.00 - 12.30:	Silvija Seres, University of Oxford Higher-order transformation of logic programs (paper) It has earlier been assumed that a compositional approach to algorithm design and program transformation is somehow unique to functional programming. With this talk we hope to demonstrate that some of the same techniques and results are applicable to logic programming as well.
12.30 - 14.00:	Lunch
14.00 - 14.30:	Jeremy Gibbons, University of Oxford When is a function a fold or an unfold? (paper, slides) We present necessary and sufficient conditions for when a (partial or total) function can be expressed as a fold or an unfold. An earlier version of this talk was presented at CMCS2001 in April; since then, the arguments have been simplified considerably. Curiously, the results are much easier to prove in a relational setting, even though they apply only to functions and not to relations.
14.30 - 15.00:	Roland Backhouse, University of Nottingham Generic termination (paper, slides) Generic programming is about parameterising programs by datatypes. The introduction of such parameters in the process of program construction opens up a new dimension for reasoning about programs. In this talk we consider how termination properties of programs are parameterised by datatypes. In particular, we compare several generalisations of the notions of well-foundedness and inductivity.
15.00 - 15.30:	Coffee
15.30 - 16.00:	Conor McBride, University of Durham Universe constructions as a medium for generic programming A `universe', in the sense of this talk, is a collection of types given by a type U of `codes' and a `decoding' function T from U to types. In a dependently typed setting, we can capture many collections of types over which we wish to define generic operations by universes whose U's are datatypes coding for exactly the types we intend. Correspondingly, systematic type-level behaviour can be implemented by `ordinary' programming over the U's. I will give some motivating examples, and discuss how Haskell might be extended to support this kind of technique.
16.00 - 16.30:	Johan Jeuring, University of Utrecht Type-indexed data types (paper) A polytypic function is a function that can be instantiated on many datatypes to obtain datatype specific functionality. Examples of polytypic functions are the functions for digital searching, pattern matching, unification, rewriting, and structure editing. For each of these problems, we not only have to define polytypic functionality, but also a type-indexed data type: a data type that is constructed in a generic way from an argument datatype. This talk shows how to define type-indexed data types, discusses some examples of type-indexed data types, and discusses the specialization of type-indexed data types.
16.30 - 17.00:	Closing