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.
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- 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 Scholar
- Daniel Fridlender and Mia Indrika. Do we need dependent types? Journal of Functional Programming, 10(4):409--415, July 2000. Google ScholarDigital Library
- 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 Scholar
- Robert Harper and Robert Pollack. Type checking with universes. Theoretical Computer Science, 89:107--136, 1991. Google ScholarDigital Library
- Ralf Hinze. Generics for the masses. Journal of Functional Programming, 16(4-5):451--483, 2006. Google ScholarDigital Library
- Ralf Hinze. Polytypic values possess polykinded types. Science of Computer Programming, 43(2-3):129--159, 2002. MPC Special Issue.Google ScholarCross Ref
- 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 Scholar
- Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis-Napoli, 1984.Google Scholar
- Conor McBride. Faking it: Simulating dependent types in haskell. Journal of Functional Programming, 12(5):375--392, 2002. Google ScholarDigital Library
- Conor McBride and James McKinna. The view from the left. Journal of Functional Programming, 14(1):69--111, 2004. Google ScholarDigital Library
- Conor McBride and Ross Paterson. Applicative programming with effects. Journal of Functional Programming, 18(1):1--13, 2008. Google ScholarDigital Library
- 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 ScholarDigital Library
- B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf's Type Theory: an introduction. Oxford University Press, 1990. Google ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- Tim Sheard. Putting Curry-Howard to work. In Proceedings of the ACM SIGPLAN 2005 Haskell Workshop. ACM Press, September 2005. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- Stephanie Weirich. Type-safe run-time polytypic programming. Journal of Functional Programming, 16(10):681--710, November 2006a. Google ScholarDigital Library
- Stephanie Weirich. RepLib: A library for derivable type classes. In Haskell Workshop, pages 1--12, Portland, OR, USA, September 2006b. Google ScholarDigital Library
Index Terms
Arity-generic datatype-generic programming
Recommendations
The right kind of generic programming
WGP '12: Proceedings of the 8th ACM SIGPLAN workshop on Generic programmingHaskell is known for its strong, static type system. A good type system classifies values, constraining the valid terms of the language and preventing many common programming errors. The Glasgow Haskell Compiler (GHC) has further extended the type ...
Arity-generic datatype-generic programming: (abstract only)
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. ...
System f-omega with equirecursive types for datatype-generic programming
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesTraversing an algebraic datatype by hand requires boilerplate code which duplicates the structure of the datatype. Datatype-generic programming (DGP) aims to eliminate such boilerplate code by decomposing algebraic datatypes into type constructor ...
Comments