skip to main content
10.1145/1707790.1707799acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Arity-generic datatype-generic programming

Published:19 January 2010Publication History

ABSTRACT

Some programs are doubly-generic. For example, map is datatype-generic in that many different data structures support a mapping operation. A generic programming language like Generic Haskell can use a single definition to generate map for each type. However, map is also arity-generic because it belongs to a family of related operations that differ in the number of arguments. For lists, this family includes repeat, map, zipWith, zipWith3, zipWith4, etc. With dependent types or clever programming, one can unify all of these functions together in a single definition.

However, no one has explored the combination of these two forms of genericity. These two axes are not orthogonal because the idea of arity appears in Generic Haskell: datatype-generic versions of repeat, map and zipWith have different arities of kind-indexed types. In this paper, we define arity-generic datatype-generic programs by building a framework for Generic Haskell-style generic programming in the dependently-typed programming language Agda 2.

References

  1. Thorsten Altenkirch and Conor McBride. Generic programming within dependently typed programming. In Proceedings of the IFIP TC2 Working Conference on Generic Programming, Dagstuhl, Germany, July 2003. Google ScholarGoogle ScholarDigital LibraryDigital Library
  2. Marcin Benke, Peter Dybjer, and Patrik Jansson. Universes for generic programs and proofs in dependent type theory. Nordic Journal of Computing, 10(4):265--289, 2003. Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. Manuel M.T. Chakravarty, Gabriele Keller, and Simon Peyton Jones. Associated type synonyms. In ICFP '05: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming, pages 241--253, New York, NY, USA, 2005. ACM. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. Adam Chlipala. A certified type-preserving compiler from lambda calculus to assembly language. In PLDI '07: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 54--65, New York, NY, USA, 2007. ACM. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. Dave Clarke, Ralf Hinze, Johan Jeuring, Andres Löh, and Jan de Wit. The Generic Haskell user's guide. Technical Report UU-CS-2001-26, Utrecht University, 2001.Google ScholarGoogle Scholar
  6. Bruno C.d.S. Oliveira, Ralf Hinze, and Andres Loeh. Extensible and modular generics for the masses. In Henrik Nilsson, editor, Trends in Functional Programming (TFP 2006), April 2007.Google ScholarGoogle Scholar
  7. Daniel Fridlender and Mia Indrika. Do we need dependent types? Journal of Functional Programming, 10(4):409--415, July 2000. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. Jean-Yves Girard. Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université Paris VII, 1972.Google ScholarGoogle Scholar
  9. Robert Harper and Robert Pollack. Type checking with universes. Theoretical Computer Science, 89:107--136, 1991. Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. Ralf Hinze. Generics for the masses. Journal of Functional Programming, 16(4-5):451--483, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. Ralf Hinze. Polytypic values possess polykinded types. Science of Computer Programming, 43(2-3):129--159, 2002. MPC Special Issue.Google ScholarGoogle ScholarCross RefCross Ref
  12. Ralf Hinze and Johan Jeuring. Generic Haskell: Practice and theory. In Roland Backhouse and Jeremy Gibbons, editors, Generic Programming, Advanced Lectures, volume 2793 of Lecture Notes in Computer Science, pages 1--56. Springer-Verlag, 2003.Google ScholarGoogle Scholar
  13. Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis-Napoli, 1984.Google ScholarGoogle Scholar
  14. Conor McBride. Faking it: Simulating dependent types in haskell. Journal of Functional Programming, 12(5):375--392, 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  15. Conor McBride and James McKinna. The view from the left. Journal of Functional Programming, 14(1):69--111, 2004. Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. Conor McBride and Ross Paterson. Applicative programming with effects. Journal of Functional Programming, 18(1):1--13, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. Peter Morris, Thorsten Altenkirch, and Neil Ghani. Constructing strictly positive families. In CATS '07: Proceedings of the Thirteenth Australasian Symposium on Theory of Computing, pages 111--121, Darlinghurst, Australia, Australia, 2007. Australian Computer Society, Inc. Google ScholarGoogle ScholarDigital LibraryDigital Library
  18. B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf's Type Theory: an introduction. Oxford University Press, 1990. Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden, September 2007.Google ScholarGoogle Scholar
  20. Simon Peyton Jones et al. The Haskell 98 language and libraries: The revised report. Journal of Functional Programming, 13(1):0--255, Jan 2003. http://www.haskell.org/definition/. Google ScholarGoogle ScholarDigital LibraryDigital Library
  21. Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Simple unification-based type inference for GADTs. In ICFP '06: Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming, pages 50--61, Portland, OR, USA, September 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  22. Tim Sheard. Generic programming programming in omega. In Roland Backhouse, Jeremy Gibbons, Ralf Hinze, and Johan Jeuring, editors, Datatype-Generic Programming, volume 4719 of Lecture Notes in Computer Science, pages 258--284. Springer, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  23. Tim Sheard. Putting Curry-Howard to work. In Proceedings of the ACM SIGPLAN 2005 Haskell Workshop. ACM Press, September 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. T. Stephen Strickland, Sam Tobin-Hochstadt, and Matthias Felleisen. Practical variable-arity polymorphism. In ESOP '09: Proceedings of the Eighteenth European Symposium On Programming, pages 32--46, March 2009. Google ScholarGoogle ScholarDigital LibraryDigital Library
  25. The Coq Development Team. The Coq Proof Assistant Reference Manual, Version 8.1. LogiCal Project, 2006. Available from http://coq.inria.fr/V8.1beta/refman/.Google ScholarGoogle Scholar
  26. Wendy Verbruggen, Edsko de Vries, and Arthur Hughes. Polytypic programming in Coq. In WGP '08: Proceedings of the ACM SIGPLAN Workshop on Generic Programming, pages 49--60, New York, NY, USA, 2008. ACM. Google ScholarGoogle ScholarDigital LibraryDigital Library
  27. Wendy Verbruggen, Edsko de Vries, and Arthur Hughes. Polytypic properties and proofs in Coq. In WGP '09: Proceedings of the 2009 ACM SIGPLAN Workshop on Generic Programming, pages 1--12, New York, NY, USA, 2009. ACM. Google ScholarGoogle ScholarDigital LibraryDigital Library
  28. Stephanie Weirich. Type-safe run-time polytypic programming. Journal of Functional Programming, 16(10):681--710, November 2006a. Google ScholarGoogle ScholarDigital LibraryDigital Library
  29. Stephanie Weirich. RepLib: A library for derivable type classes. In Haskell Workshop, pages 1--12, Portland, OR, USA, September 2006b. Google ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. Arity-generic datatype-generic programming

        Recommendations

        Comments

        Login options

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

        Sign in
        • Published in

          cover image ACM Conferences
          PLPV '10: Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification
          January 2010
          70 pages
          ISBN:9781605588902
          DOI:10.1145/1707790

          Copyright © 2010 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]

          Publisher

          Association for Computing Machinery

          New York, NY, United States

          Publication History

          • Published: 19 January 2010

          Permissions

          Request permissions about this article.

          Request Permissions

          Check for updates

          Qualifiers

          • research-article

          Acceptance Rates

          Overall Acceptance Rate18of25submissions,72%

          Upcoming Conference

          POPL '25

        PDF Format

        View or Download as a PDF file.

        PDF

        eReader

        View online with eReader.

        eReader