Edsko de Vries
Andres Löh
ABSTRACT
We introduce the sum-of-products (SOP) view for datatype-generic programming (in Haskell). While many of the libraries that are commonly in use today represent datatypes as arbitrary combinations of binary sums and products, SOP reflects the structure of datatypes more faithfully: each datatype is a single n-ary sum, where each component of the sum is a single n-ary product. This representation turns out to be expressible accurately in GHC with today's extensions. The resulting list-like structure of datatypes allows for the definition of powerful high-level traversal combinators, which in turn encourage the definition of generic functions in a compositional and concise style. A major plus of the SOP view is that it allows to separate function-specific metadata from the main structural representation and recombining this information later.
- Michael D. Adams and Thomas M. DuBuisson. Template your boilerplate: Using Template Haskell for efficient generic programming. In Haskell '12, pages 13--24. ACM, 2012. Google Scholar
Digital Library
- Artem Alimarine and Rinus Plasmeijer. A generic programming extension for Clean. In IFL, volume 2312 of LNCS, pages 168--185. Springer, 2001. Google ScholarDigital Library
- Thorsten Altenkirch, Conor McBride, and Peter Morris. Generic programming with dependent types. In SSDGP '06, pages 209--257. Springer, 2007. Google ScholarDigital Library
- Lennart Augustsson. geniplate: Use Template Haskell to generate Uniplate-like functions, 2011. URL http://hackage.haskell.org/package/geniplate.Google Scholar
- Patrick Bahr and Tom Hvitved. Compositional data types. In WGP '11, pages 83--94. ACM, 2011. Google ScholarDigital Library
- Marcin Benke, Peter Dybjer, and Patrik Jansson. Universes for generic programs and proofs in dependent type theory. Nordic J. of Computing, 10 (4): 265--289, December 2003. Google ScholarDigital Library
- Manuel M. T. Chakravarty, Gabriel C. Ditu, and Roman Leshchinskiy. Instant generics: Fast and easy, 2009. URL http://www.cse.unsw.edu.au/ chak/papers/CDL09.html.Google Scholar
- James Chapman, Pierre-Évariste Dagand, Conor McBride, and Peter Morris. The gentle art of levitation. In ICFP '10, pages 3--14. ACM, 2010. Google ScholarDigital Library
- Koen Claessen and John Hughes. QuickCheck: A lightweight tool for random testing of Haskell programs. In ICFP '00, pages 268--279. ACM, 2000. Google ScholarDigital Library
- Richard A. Eisenberg. Defunctionalization for the win, 2013. URL http://typesandkinds.wordpress.com/2013/04/01/defunctionalization-for-the-win/.Google Scholar
- Richard A. Eisenberg and Stephanie Weirich. Dependently typed programming with singletons. In Haskell '12, pages 117--130. ACM, 2012. Google ScholarDigital Library
- J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, and Alan Schmitt. Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem. ACM Trans. Program. Lang. Syst., 29 (3), May 2007. ISSN 0164-0925. Google ScholarDigital Library
- Ralf Hinze. Polytypic values possess polykinded types. Science of Computer Programming, 43 (2--3): 129--159, 2002.Google ScholarCross Ref
- Ralf Hinze, Andres Löh, and Bruno C. d. S. Oliveira. ''Scrap Your Boilerplate'' reloaded. In FLOPS, volume 3945 of LNCS, pages 13--29. Springer, 2006. Google ScholarDigital Library
- Stefan Holdermans, Johan Jeuring, Andres Löh, and Alexey Rodriguez Yakushev. Generic views on data types. In MPC, volume 4014 of LNCS, pages 209--234. Springer, 2006. Google ScholarDigital Library
- Patrik Jansson and Johan Jeuring. PolyP--a polytypic programming language extension. In POPL '97, pages 470--482. ACM, 1997. Google ScholarDigital Library
- Ralf Lämmel and Simon Peyton Jones. Scrap your boilerplate: a practical design pattern for generic programming. In TLDI '03, pages 26--37. ACM, 2003. Google ScholarDigital Library
- Eelco Lempsink, Sean Leather, and Andres Löh. Type-safe diff for families of datatypes. In WGP '09, pages 61--72. ACM, 2009. Google ScholarDigital Library
- Andres Löh. Exploring Generic Haskell. PhD thesis, Universiteit Utrecht, 2004.Google Scholar
- José Pedro Magalhães. The right kind of generic programming. In WGP '12, pages 13--24. ACM, 2012. Google ScholarDigital Library
- José Pedro Magalhães, Atze Dijkstra, Johan Jeuring, and Andres Löh. A generic deriving mechanism for Haskell. In Haskell '10, pages 37--48. ACM, 2010. Google ScholarDigital Library
- José Pedro Magalhães and Andres Löh. Generic generic programming, 2013. URL http://www.andres-loeh.de/GenericGenericProgramming/. Unpublished original draft ofcitetGGP.Google Scholar
- José Pedro Magalhães and Andres Löh. Generic generic programming. In PADL, volume 8324 of LNCS, pages 216--231. Springer, 2014.Google Scholar
- Per Martin-Löf. Intuitionistic type theory. Bibliopolis, 1984.Google Scholar
- Conor McBride. Ornamental algebras, algebraic ornaments. 2010. Submitted to Journal of Functional Programming.Google Scholar
- Neil Mitchell and Colin Runciman. Uniform boilerplate and list processing. In Haskell '07, pages 49--60. ACM, 2007. Google ScholarDigital Library
- Noort, Alexey Rodriguez Yakushev, Stefan Holdermans, Johan Jeuring, Bastiaan Heeren, and José Pedro Magalhes. A lightweight approach to datatype-generic rewriting. Journal of Functional Programming, 20 (ãSpecial Issue 3-4): 375--413, 2010. Google ScholarDigital Library
- Russell O'Connor. Functor is to lens as applicative is to biplate: Introducing multiplate. CoRR, abs/1103.2841, 2011.Google Scholar
- Alexey Rodriguez Yakushev, Stefan Holdermans, Andres Löh, and Johan Jeuring. Generic programming with fixed points for mutually recursive datatypes. In ICFP '09, pages 233--244. ACM, 2009. Google ScholarDigital Library
- Neil Sculthorpe, Nicolas Frisby, and Andy Gill. The Kansas University Rewrite Engine: A Haskell-embedded strategic programming language with custom closed universes. Submitted to the Journal of Functional Programming, 2014. URL http://www.cs.swan.ac.uk/ csnas/papers_and_talks/kure.pdf.Google Scholar
- Tim Sheard and Simon Peyton Jones. Template meta-programming for Haskell. In Haskell '02, pages 1--16. ACM, December 2002. Google ScholarDigital Library
- Martin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones, and Kevin Donnelly. System F with type equality coercions. In TLDI '07, pages 53--66. ACM, 2007. Google ScholarDigital Library
- Stephanie Weirich. RepLib: a library for derivable type classes. In Haskell '06, pages 1--12. ACM, 2006. Google ScholarDigital Library
- Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis, and José Pedro Magalhes. Giãving Haskell a promotion. In TLDI '12, pages 53--66. ACM, 2012. Google ScholarDigital Library
Index Terms
- True sums of products
Recommendations
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 ...
System f-omega with equirecursive types for datatype-generic programming
POPL '16Traversing 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 ...
Normalization by evaluation for sized dependent types
Sized types have been developed to make termination checking more perspicuous, more powerful, and more modular by integrating termination into type checking. In dependently-typed proof assistants where proofs by induction are just recursive functional ...
Comments