[ Apps, People, Papers, PolyP, PolyLib, Examples, Links, Future ]

Polytypic programming at Chalmers

This page has not been actively updated since 2004 and is kept mainly as a historic reference. More recent material can be found on the functional programming group wiki. Patrik Jansson (20090504).

General theme:

Functional Generic Programming - where type theory meets functional programming

A number of functions have to be written over and over again on different datatypes. Examples of such functions are pretty printers, parsers, equality functions, most general unifiers, pattern matchers, rewriting functions, etc. These functions are examples of so-called polytypic functions. A polytypic function is a function that is defined by induction on the structure of user-defined datatypes.

At Chalmers we have developed an extension of Haskell with which polytypic functions can be written and type checked. Furthermore, we are developing methods for writing and proving properties of polytypic functions. Currently the focus is on the border between generic programming and dependent types.

For an in-depth treatment of polytypism, see Janssons PhD thesis, Functional Polytypic Programming, or the AFP'98 tutorial.

Applications of polytypic programming

Besides a library of basic polytypic functions, which can be found in the distribution of PolyP (see below) we have developed or are developing several polytypic programs, for Pattern matching, Term rewriting, Unification, Data compression, Parsing, Genetic algorithms ...

People

Papers on polytypic programming

Ulf Norell and Patrik Jansson. Polytypic Programming in Haskell, presented at IFL'03, in press for LNCS nnnn, 2004.

Marcin Benke, Peter Dybjer and Patrik Jansson. Universes for Generic Programs and Proofs in Dependent Type Theory, In press for Nordic Journal of Computing, 2004.

Ulf Norell. Functional Generic Programming and Type Theory, Master's thesis, Computing Science, Chalmers, 2002.

Patrik Jansson and Johan Jeuring. Polytypic Data Conversion Programs, Science of Computer Programming 43(1), pages 35-75, 2002. Paper available through ScienceDirect.

François-Régis Sinot. Polytypic Programming and Dependent Types, Project report, Computing Science, Chalmers, 2001.

P. Jansson and J. Jeuring. A Framework for Polytypic Programming on Terms, with an Application to Rewriting, Workshop on Generic Programming, Utrecht University report UU-CS-2000-19, 2000.

Patrik Jansson. Functional Polytypic Programming. PhD thesis, Chalmers University of Technology and Göteborg University, 2000

Patrik Jansson and Johan Jeuring. Polytypic Compact Printing and Parsing. Presented at ESOP'99.

Roland Backhouse, Patrik Jansson, Johan Jeuring and Lambert Meertens. Generic Programming - An Introduction. Lecture notes on AFP'98. Also in LNCS, 1999.

P. Jansson and J. Jeuring. PolyLib - a library of polytypic functions. Workshop on Generic Programming, Chalmers University of Technology, 1998.

Joost Halenbeek, Comparing Approaches to Polytypic Programming MSc thesis, INF-SCR-99-02, Utrecht University, December 22, 1998.

Staffan Björk. Parsers, Pretty Printers and PolyP. Master's thesis, Göteborg University, 1997.

Måns Vestin. Genetic algorithms in Haskell with polytypic programming. Master's thesis, Göteborg University, 1997.

P. Jansson and J. Jeuring. PolyP - a polytypic programming language extension. (abstract) In Conference Record of POPL '97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 470--482, 1997.

J. Jeuring and P. Jansson. Polytypic programming. (abstract) (problem set) In J. Launchbury, E. Meijer and T. Sheard Advanced Functional Programming, LNCS 1129, pages 68--114, Springer-Verlag, 1996.

J. Jeuring. Polytypic pattern matching. (abstract) In Conference Record of FPCA '95, SIGPLAN-SIGARCH-WG2.8 Conference on Functional Programming Languages and Computer Architecture, pages 238--248, 1995.

P. Jansson. Polytypism and polytypic unification. Master's thesis, Chalmers University of Technology, 1995.

P. Jansson and J. Jeuring. Polytypic Unification (accompanying material), JFP 8 (5), September 1998.

PolyP - a polytypic programming language

We have developed a compiler, PolyP, for an extension of Haskell with which polytypic functions can be written and type checked. The source code for PolyP is freely available and is updated now and then.

PolyLib

PolyLib is a library of polytypic functions that comes with the implementation PolyP. The library is described in a paper and in Janssons thesis.

Polytypic functions

Some examples of polytypic functions.
pmap :: Regular d => (a->b) -> d a -> d b
A generalisation to all regular datatypes of the normal map on lists . Applies a function to all elements in a structure.
size :: Regular d => d a -> Int
A generalisation of length on lists. Counts the number of elements of type a in a structure of type d a.
pzip :: Regular d => (d a,d b) -> Maybe (d (a,b))
A generalisation of zip on lists. Takes a pair of structures to Just a structure of pairs if they match. Otherwise Nothing.
cata :: Regular d => ((FunctorOf d) a b -> b) -> d a -> b
A generalised fold. The catamorphism is a general recursion operator that replaces datatype constructors with supplied functions.
These functions (and many more) are available in PolyLib.

Other work on polytypism or related topics

Future plans


Last modified: . by
Patrik Jansson / NOpatrikjSP@AMchalmers.se