research-article

Parametric datatype-genericity

Authors:

Jeremy Gibbons,

Ross PatersonAuthors Info & Claims

WGP '09: Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming

Pages 85 - 93

https://doi.org/10.1145/1596614.1596626

Published: 30 August 2009 Publication History

Abstract

Datatype-generic programs are programs that are parametrized by a datatype or type functor: whereas polymorphic programs abstract from the "integers" in "lists of integers",datatype-generic programs abstract from the "lists of". There are two main styles of datatype-generic programming: the Algebra of Programming approach, characterized by structured recursion operators arising from initial algebras and final coalgebras, and the Generic Haskell approach, characterized by case analysis over the structure of a datatype. We show that the former enjoys a kind of higher-order naturality, relating the behaviours of generic functions at different types; in contrast, the latter is ad~hoc, with no coherence required or provided between the various clauses of a definition. Moreover, the naturality properties arise "for free", simply from the parametrized types of the generic functions: we present a higher-order parametricity theorem for datatype-generic operators.

References

[1]

Matthew H. Austern. Generic Programming and the STL. Addison-Wesley, 1999.

[2]

Roland Backhouse and Jeremy Gibbons, editors. Summer School on Generic Programming, volume 2793 of Lecture Notes in Computer Science. Springer-Verlag, 2003.

Digital Library

[3]

Roland Backhouse, Jeremy Gibbons, Ralf Hinze, and Johan Jeuring, editors. Spring School on Datatype-Generic Programming, volume 4719 of Lecture Notes in Computer Science. Springer-Verlag, 2007.

Digital Library

[4]

Richard Bird and Oege de Moor. Algebra of Programming. Prentice-Hall, 1996.

Digital Library

[5]

Richard Bird, Jeremy Gibbons, and Geraint Jones. Program optimisation, naturally. In J. W. Davies, A. W. Roscoe, and J. C. P. Woodcock, editors, Millenial Perspectives in Computer Science. Palgrave, 2000.

[6]

Luca Cardelli and Peter Wegner. On understanding types, data abstraction and polymorphism. ACM Computing Surveys, 17(4):471--522, December 1985.

Digital Library

[7]

Roy L. Crole. Categories for Types. Cambridge University Press, 1994.

[8]

Jeremy Gibbons. Origami programming. In Jeremy Gibbons and Oege de Moor, editors, The Fun of Programming, Cornerstones in Computing, pages 41--60. Palgrave, 2003.

[9]

Jeremy Gibbons. Datatype-generic programming. In Backhouse et al. {3}.

[10]

Jeremy Gibbons and Geraint Jones. The under-appreciated unfold. In International Conference on Functional Programming, pages 273--279, Baltimore, Maryland, September 1998.

Digital Library

[11]

Jean-Yves Girard. Interprétation Fonctionnelle et Élimination des Coupures de l'Arithmétique d'Ordre Supérieur. PhD thesis, Université de Paris VII, 1972.

[12]

Cordelia Hall, Kevin Hammond, Simon Peyton Jones, and Philip Wadler. Type classes in Haskell. ACM Transactions on Programming Languages and Systems, 18(2):19--138, 1996.

Digital Library

[13]

Robert Harper and Greg Morrisett. Compiling polymorphism using intensional type analysis. In Principles of Programming Languages, 1995.

Digital Library

[14]

Ralf Hinze. A generic programming extension for Haskell. In Erik Meijer, editor, Third Haskell Workshop, 1999.

[15]

Ralf Hinze. Polytypic values possess polykinded types. In Roland Backhouse and José Nuno Oliveira, editors, Mathematics of Program Construction, volume 1837 of Lecture Notes in Computer Science, pages 2--27. Springer-Verlag, 2000.

Digital Library

[16]

Ralf Hinze and Johan Jeuring. Generic Haskell: Applications. In Backhouse and Gibbons {2}, pages 57--97.

[17]

Ralf Hinze and Johan Jeuring. Generic Haskell: Practice and theory. In Backhouse and Gibbons {2}, pages 1--56.

[18]

Ralf Hinze, Johan Jeuring, and Andres Löh. Comparing approaches to generic programming in Haskell. In Backhouse et al. {3}.

[19]

Paul Hoogendijk. A Generic Theory of Datatypes. PhD thesis, Technische Universiteit Eindhoven, 1997.

[20]

Paul Hoogendijk and Roland Backhouse. When do datatypes commute? In Eugenio Moggi and Guiseppe Rosolini, editors, Category Theory and Computer Science, volume 1290 of Lecture Notes in Computer Science, pages 242--260. Springer-Verlag, September 1997.

Digital Library

[21]

Johan Jeuring and Patrick Jansson. Polytypic programming. In John Launchbury, Erik Meijer, and Tim Sheard, editors, Advanced Functional Programming, volume 1129 of Lecture Notes in Computer Science. Springer--Verlag, 1996.

Digital Library

[22]

Mark P. Jones. Functional programming with overloading and higher--order polymorphism. In Johan Jeuring and Erik Meijer, editors, LNCS 925: Advanced Functional Programming. Springer-Verlag, 1995. Lecture notes from the First International Spring School on Advanced Functional Programming Techniques, Båstad, Sweden.

Digital Library

[23]

Ralf Lämmel and Simon Peyton Jones. Scrap your boilerplate: A practical design pattern for generic programming. In Types in Language Design and Implementation, 2003.

Digital Library

[24]

Ralf Lämmel and Simon Peyton Jones. Scrap more Boilerplate: Reflection, zips, and generalised casts. In International Conference on Functional Programming, pages 244--255. ACM Press, 2004.

Digital Library

[25]

Ralf Lämmel and Simon Peyton Jones. Scrap your Boilerplate with class: Extensible generic functions. In International Conference on Functional Programming, pages 204--215. ACM Press, September 2005.

Digital Library

[26]

Andres Löh. Exploring Generic Haskell. PhD thesis, Utrecht University, 2004.

[27]

Saunders Mac Lane. Categories for the Working Mathematician. Springer-Verlag, 1971.

[28]

Lambert Meertens. Paramorphisms. Formal Aspects of Computing, 4(5):413--424, 1992.

[29]

Erik Meijer, Maarten Fokkinga, and Ross Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In John Hughes, editor, Functional Programming Languages and Computer Architecture, volume 523 of Lecture Notes in Computer Science, pages 124--144. Springer-Verlag, 1991.

Digital Library

[30]

John C. Mitchell and Albert R. Meyer. Second-order logical relations. In Rohit Parikh, editor, Logics of Programs, volume 193 of Lecture Notes in Computer Science, pages 225--236, 1985.

Digital Library

[31]

Ross A. Paterson. Reasoning about Functional Programs. PhD thesis, University of Queensland, 1987.

[32]

Simon Peyton Jones. The Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, 2003.

[33]

John C. Reynolds. Towards a theory of type structure. In B. Robinet, editor, Colloque sur la Programmation, volume 19 of Lecture Notes in Computer Science, pages 408--425. Springer-Verlag, 1974.

Digital Library

[34]

Jeremy G. Siek, Lie-Quan Lee, and Andrew Lumsdaine. The Boost Graph Library. Addison-Wesley, 2002.

[35]

Neil J. A. Sloane. On-line encyclopedia of integer sequences. http://www.research.att.com/~njas/sequences/. Accessed May 2007.

[36]

Michael B. Smyth and Gordon D. Plotkin. The category-theoretic solution of recursive domain equations. SIAM Journal on Computing, 11(4):761--783, November 1982.

Digital Library

[37]

Walid Taha. A gentle introduction to multi-stage programming. In Christian Lengauer, Don Batory, Charles Consel, and Martin Odersky, editors, Domain-Specific Program Generation, number 3016 in Lecture Notes in Computer Science, pages 30--50. Springer-Verlag, 2004.

[38]

Tarmo Uustalu, Varmo Vene, and Alberto Pardo. Recursion schemes from comonads. Nordic Journal of Computing, 2001.

Digital Library

[39]

Varmo Vene and Tarmo Uustalu. Functional programming with apomorphisms (corecursion). Proceedings of the Estonian Academy of Sciences: Physics, Mathematics, 47(3):147--161, 1998. 9th Nordic Workshop on Programming Theory.

[40]

Philip Wadler. Theorems for free! In Functional Programming Languages and Computer Architecture, pages 347--359. ACM, 1989.

Digital Library

Cited By

Xue J(2016)Genericity in PAR PlatformStructured Object-Oriented Formal Language and Method10.1007/978-3-319-31220-0_1(3-14)Online publication date: 2016
https://doi.org/10.1007/978-3-319-31220-0_1
Hinze RWu NJärvi JMu S(2011)Towards a categorical foundation for generic programmingProceedings of the seventh ACM SIGPLAN workshop on Generic programming10.1145/2036918.2036926(47-58)Online publication date: 18-Sep-2011
https://dl.acm.org/doi/10.1145/2036918.2036926
Hinze R(2011)Type FusionAlgebraic Methodology and Software Technology10.1007/978-3-642-17796-5_6(92-110)Online publication date: 2011
https://doi.org/10.1007/978-3-642-17796-5_6
Show More Cited By

Index Terms

Parametric datatype-genericity
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Control structures
        Patterns
        Polymorphism
        Recursion
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Program schemes
      2. Type structures

Recommendations

Minimally strict polymorphic functions
PPDP '11: Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming

In this paper we show how to efficiently check whether a polymorphic function is minimally strict. A function is minimally strict if it is the minimal element of a specific less-strict ordering. We prove that we can check whether two polymorphic ...
Parametric quantifiers for dependent type theory

Polymorphic type systems such as System F enjoy the parametricity property: polymorphic functions cannot inspect their type argument and will therefore apply the same algorithm to any type they are instantiated on. This idea is formalized mathematically ...
Relationally-parametric polymorphic contracts
DLS '07: Proceedings of the 2007 symposium on Dynamic languages

The analogy between types and contracts raises the question of how many features of static type systems can be expressed as dynamic contracts. An important feature missing in prior work on contracts is parametricity, as represented by the polymorphic ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

WGP '09: Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming

August 2009

100 pages

ISBN:9781605585109

DOI:10.1145/1596614

Program Chairs:
Patrik Jansson
Chalmers U. of Technology and U. of Gothenburg, Sweden
,
Sibylle Schupp
Hamburg University of Technology, Germany

Copyright © 2009 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 30 August 2009

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP '09

Sponsor:

ICFP '09: ACM SIGPLAN International Conference on Functional Programming

August 30, 2009

Edinburgh, Scotland

Acceptance Rates

Overall Acceptance Rate 30 of 43 submissions, 70%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
135
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)1

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Xue J(2016)Genericity in PAR PlatformStructured Object-Oriented Formal Language and Method10.1007/978-3-319-31220-0_1(3-14)Online publication date: 2016
https://doi.org/10.1007/978-3-319-31220-0_1
Hinze RWu NJärvi JMu S(2011)Towards a categorical foundation for generic programmingProceedings of the seventh ACM SIGPLAN workshop on Generic programming10.1145/2036918.2036926(47-58)Online publication date: 18-Sep-2011
https://dl.acm.org/doi/10.1145/2036918.2036926
Hinze R(2011)Type FusionAlgebraic Methodology and Software Technology10.1007/978-3-642-17796-5_6(92-110)Online publication date: 2011
https://doi.org/10.1007/978-3-642-17796-5_6
Hinze R(2010)Adjoint folds and unfoldsProceedings of the 10th international conference on Mathematics of program construction10.5555/1886619.1886634(195-228)Online publication date: 21-Jun-2010
https://dl.acm.org/doi/10.5555/1886619.1886634
Bernardy JJansson PPaterson R(2010)Parametricity and dependent typesACM SIGPLAN Notices10.1145/1932681.186359245:9(345-356)Online publication date: 27-Sep-2010
https://dl.acm.org/doi/10.1145/1932681.1863592
Bernardy JJansson PPaterson RHudak PWeirich S(2010)Parametricity and dependent typesProceedings of the 15th ACM SIGPLAN international conference on Functional programming10.1145/1863543.1863592(345-356)Online publication date: 27-Sep-2010
https://dl.acm.org/doi/10.1145/1863543.1863592
Hinze RJames DOliveira BZalewski M(2010)Reason isomorphically!Proceedings of the 6th ACM SIGPLAN workshop on Generic programming10.1145/1863495.1863507(85-96)Online publication date: 26-Sep-2010
https://dl.acm.org/doi/10.1145/1863495.1863507
Hinze R(2010)Adjoint Folds and UnfoldsMathematics of Program Construction10.1007/978-3-642-13321-3_13(195-228)Online publication date: 2010
https://doi.org/10.1007/978-3-642-13321-3_13

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents