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.
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.
pmap :: Regular d => (a->b) -> d a -> d b
mapon lists . Applies a function to all elements in a structure.
size :: Regular d => d a -> Int
lengthon lists. Counts the number of elements of type
ain a structure of type
pzip :: Regular d => (d a,d b) -> Maybe (d (a,b))
zipon lists. Takes a pair of structures to
Justa structure of pairs if they match. Otherwise
cata :: Regular d => ((FunctorOf d) a b -> b) -> d a -> b
Generic Programming, R. Bird, O. de Moor, J. Gibbons, G. Jones