A new approach to generic functional programming

ABSTRACT

This paper describes a new approach to generic functional programming, which allows us to define functions generically for all datatypes expressible in Haskell. A generic function is one that is defined by induction on the structure of types. Typical examples include pretty printers, parsers, and comparison functions. The advanced type system of Haskell presents a real challenge: datatypes may be parameterized not only by types but also by type constructors, type definitions may involve mutual recursion, and recursive calls of type constructors can be arbitrarily nested. We show that—despite this complexity—a generic function is uniquely defined by giving cases for primitive types and type constructors (such as disjoint unions and cartesian products). Given this information a generic function can be specialized to arbitrary Haskell datatypes. The key idea of the approach is to model types by terms of the simply typed &lgr;-calculus augmented by a family of recursion operators. While conceptually simple, our approach places high demands on the type system: it requires polymorphic recursion, rank-n types, and a strong form of type constructor polymorphism. Finally, we point out connections to Haskell's class system and show that our approach generalizes type classes in some respects.

REFERENCES

• 1: M. Abadi, L. Cardelli, B. Pierce, and D. R~my. Dynamic typing in polymorphic languages. Journal of Functional Programming, 5(1):111-130, January 1995.
• 2: H. P. Barendregt. The Lambda Calculus m Its Syntax and Semantics. North-Holland, Amsterdam New York Oxford, revised edition, 1984.
• 3: H. P. Barendregt, Lambda calculi with types, Handbook of logic in computer science (vol. 2): background: computational structures, Oxford University Press, Inc., New York, NY, 1993
• 4: Richard Bird, Introduction to Functional Programming, Pearson Education, 1998
• 5: Richard S. Bird , Lambert G. L. T. Meertens, Nested Datatypes, Proceedings of the Mathematics of Program Construction, p.52-67, June 15-17, 1998
• 6: Richard S. Bird , Ross Paterson, de Bruijn notation as a nested datatype, Journal of Functional Programming, v.9 n.1, p.77-91, January 1999 [doi>10.1017/S0956796899003366]
• 7: Richard Bird and Ross Paterson. Generalised folds for nested datatypes. Formal Aspects o} Computing, 11(2):200-222, 1999.
• 8: Robin Cockett and Tom Fukushima. About Charity. Yellow Series Report 92/480/18, Dept. of Computer Science, Univ. of Calgary, June 1992.
• 9: Bruno Courcelle. Fundamental properties of infinite trees. Theoretical Computer Science, 25(2):95-169, March 1983.
• 10: Karl Crary , Stephanie Weirich , Greg Morrisett, Intensional polymorphism in type-erasure semantics, ACM SIGPLAN Notices, v.34 n.1, p.301-312, Jan. 1999
• 11: Jean-Yves Girard. Interpretation fonctionelle et dlimination des coupures dans l'ar~thdtique d'ordre supdrieur. PhD thesis, Universit~ Paris VII, 1972.
• 12: T. Hagino. Category Theoretic Approach to Data Types. PhD thesis, University of Edinburgh, 1987.
• 13: Cordelia V. Hall , Kevin Hammond , Simon L. Peyton Jones , Philip L. Wadler, Type classes in Haskell, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.2, p.109-138, March 1996 [doi>10.1145/227699.227700]
• 14: Robert Harper , Greg Morrisett, Compiling polymorphism using intensional type analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.130-141, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199475]
• 15: Ralf Hinze. Numerical representations as higher-order nested datatypes. Technical Report IAI-TR-98-12, Institut fiir Informatik III, Universit~t Bonn, December 1998.
• 16: Ralf Hinze, Generalizing generalized tries, Journal of Functional Programming, v.10 n.4, p.327-351, July 2000 [doi>10.1017/S0956796800003713]
• 17: Ralf Hinze. A generic programming extension for Haskell. In Erik Meijer, editor, Proceedings of the 3rd Haskelt Workshop, Paris, France, September 1999. The proceedings appear as a technical report of Universiteit Utrecht, UU-CS-1999-28.
• 18: Ralf Hinze. Manufacturing datatypes. In Chris Okasaki, editor, Proceedings of the Workshop on Algorithmic Aspects of Advanced Programming Languages, WAAAPL'99, Paris, France, pages 1-16, September 1999. The proceedings appear as a technical report of Columbia University, CUCS-023-99, also available from http ://www. cs. columbia, edu/~ cdo/waaapl, html.
• 19: Ralf Hinze. Polytypic functions over nested datatypes. Discrete Mathematics and Theoretical Computer Science, 3(4):159-180, 1999.
• 20: Ralf Hinze, Polytypic Programming With Ease (Extended Abstract), Proceedings of the 4th Fuji International Symposium on Functional and Logic Programming, p.21-36, November 11-13, 1999
• 21: Patrik Jansson , Johan Jeuring, PolyP—a polytypic programming language extension, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.470-482, January 15-17, 1997, Paris, France [doi>10.1145/263699.263763]
• 22: Patrik Jansson and Johan Jeuring. PolyLib--A library of polytypic functions. In Roland Backhouse and Tim Sheard, editors, Informal Proceedings Workshop on Generic Programming, WGP'98, Marstrand, Sweden. Department of Computing Science, Chalmers University of Technology and GSteborg University, June 1998.
• 23: Patrik Jansson , Johan Jeuring, Polytypic Compact Printing and Parsing, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.273-287, March 22-28, 1999
• 24: C. B. Jay , G. Bellè , E. Moggi, Functorial ML, Journal of Functional Programming, v.8 n.6, p.573-619, November 1998 [doi>10.1017/S0956796898003128]
• 25: C. Barry Jay , J. Robin B. Cockett, Shapely Types and Shape Polymorphism, Proceedings of the 5th European Symposium on Programming: Programming Languages and Systems, p.302-316, April 11-13, 1994
• 26: Johan Jeuring , Patrik Jansson, Polytypic Programming, Advanced Functional Programming, Second International School-Tutorial Text, p.68-114, August 26-30, 1996
• 27: Mark P. Jones. A system of constructor classes: overloading and implicit higher-order polymorphism. Journal of Functional Programming, 5(1):1-35, January 1995.
• 28: Mark P. Jones, Functional Programming with Overloading and Higher-Order Polymorphism, Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques-Tutorial Text, p.97-136, May 24-30, 1995
• 29: M.P. Jones and J.C. Peterson. Hugs 98 User Manual, May 1999. Available from http://www, haskell, org/ hugs.
• 30: Nancy McCracken, The typechecking of programs with implicit type structure., Proc. of the international symposium on Semantics of data types, p.301-315, July 1984, Sophia-Antipolis, France
• 31: Lambert G. L. T. Meertens, Calculate Polytypically!, Proceedings of the 8th International Symposium on Programming Languages: Implementations, Logics, and Programs, p.1-16, September 24-27, 1996
• 32: Erik Meijer , Graham Hutton, Bananas in space: extending fold and unfold to exponential types, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.324-333, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224225]
• 33: Alan Mycroft, Polymorphic Type Schemes and Recursive Definitions, Proceedings of the 6th Colloquium on International Symposium on Programming, p.217-228, April 17-19, 1984
• 34: Chris Okasaki, Purely functional data structures, Cambridge University Press, New York, NY, 1998
• 35: Chris Okasaki, From fast exponentiation to square matrices: an adventure in types, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.28-35, September 27-29, 1999, Paris, France
• 36: Simon Peyton Jones. Explicit quantification in Haskell, 1998. Available from http://research.microsoft. com/Us ers / s imonp j/Haske ii / quant if i cat i on. html.
• 37: Simon Peyton Jones and John Hughes, editors. Haskell 98 -- A Non-strict, Purely Functional Language, February 1999. Available from http://www, haskell, org/definition/.
• 38: Simon L. Peyton Jones, Compiling Haskell by Program Transformation: A Report from the Trenches, Proceedings of the 6th European Symposium on Programming Languages and Systems, p.18-44, April 22-24, 1996
• 39: Simon L. Peyton Jones and Erik Meijer. Henk: A typed intermediate language. In Proceedings of the Types in Compilation Workshop, Amsterdam, june, 1997. Available from http://~w, cs. be. edu/"muller/TIC97/.
• 40: Fritz Ruehr. Structural polymorphism. In Roland Backhouse and Tim Sheaxd, editors, Informal Proceedings Workshop on Generic Programming, WGP'98, Marstrand, Sweden, 18 June 1998. Dept. of Computing Science, Chalmers Univ. of Techn. and GSteborg Univ., June 1998.
• 41: Karl Fritz l%uehr. Analytical and Structural Polymorphism Expressed using Patterns over Types. PhD thesis, University of Michigan, 1992.
• 42: Tim Sheard, Automatic generation and use of abstract structure operators, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.4, p.531-557, Oct. 1991 [doi>10.1145/115372.115369]
• 43: Tim Sheard. Type parametric programming. Technical report CS/E 93-018, Oregon Graduate Institute of Science and Technology, Department of Computer Science and Engineering, Portland, OR, USA, November 1993.
• 44: Philip Wadler, Theorems for free!, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.347-359, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99404]
• 45: Zhe Yang, Encoding types in ML-like languages, ACM SIGPLAN Notices, v.34 n.1, p.289-300, Jan. 1999

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Design, Languages, Theory