A Formal Comparison of Approaches to Datatype-Generic Programming
Open Access
- 11 February 2012
- journal article
- Published by Open Publishing Association in Electronic Proceedings in Theoretical Computer Science
- Vol. 76, 50-67
- https://doi.org/10.4204/eptcs.76.6
Abstract
Datatype-generic programming increases program abstraction and reuse by making functions operate uniformly across different types. Many approaches to generic programming have been proposed over the years, most of them for Haskell, but recently also for dependently typed languages such as Agda. Different approaches vary in expressiveness, ease of use, and implementation techniques. Some work has been done in comparing the different approaches informally. However, to our knowledge there have been no attempts to formally prove relations between different approaches. We thus present a formal comparison of generic programming libraries. We show how to formalise different approaches in Agda, including a coinductive representation, and then establish theorems that relate the approaches to each other. We provide constructive proofs of inclusion of one approach in another that can be used to convert between approaches, helping to reduce code duplication across different libraries. Our formalisation also helps in providing a clear picture of the potential of each approach, especially in relating different generic views and their expressiveness.Comment: In Proceedings MSFP 2012, arXiv:1202.240This publication has 27 references indexed in Scilit:
- MiniAgda: Integrating Sized and Dependent TypesElectronic Proceedings in Theoretical Computer Science, 2010
- The gentle art of levitationPublished by Association for Computing Machinery (ACM) ,2010
- Subtyping, DeclarativelyLecture Notes in Computer Science, 2010
- Generic programming in 3DScience of Computer Programming, 2009
- Comparing Approaches to Generic Programming in HaskellLecture Notes in Computer Science, 2007
- Datatype-Generic ProgrammingLecture Notes in Computer Science, 2007
- Generics for the massesJournal of Functional Programming, 2006
- “Scrap Your Boilerplate” ReloadedLecture Notes in Computer Science, 2006
- A lightweight implementation of generics and dynamicsPublished by Association for Computing Machinery (ACM) ,2002
- Nested datatypesLecture Notes in Computer Science, 1998