Ghostbuster: a tool for simplifying and converting GADTs

Abstract

Generalized Algebraic Dataypes, or simply GADTs, can encode non-trivial properties in the types of the constructors. Once such properties are encoded in a datatype, however, all code manipulating that datatype must provide proof that it maintains these properties in order to typecheck. In this paper, we take a step towards gradualizing these obligations. We introduce a tool, Ghostbuster, that produces simplified versions of GADTs which elide selected type parameters, thereby weakening the guarantees of the simplified datatype in exchange for reducing the obligations necessary to manipulate it. Like ornaments, these simplified datatypes preserve the recursive structure of the original, but unlike ornaments we focus on information-preserving bidirectional transformations. Ghostbuster generates type-safe conversion functions between the original and simplified datatypes, which we prove are the identity function when composed. We evaluate a prototype tool for Haskell against thousands of GADTs found on the Hackage package database, generating simpler Haskell'98 datatypes and round-trip conversion functions between the two.

References

1. M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin. Dynamic typing in a statically-typed language. POPL’98: Principles of Programming Languages, pages 237–268, 1989.
2. M. Abadi, L. Cardelli, B. Pierce, and D. Rémy. Dynamic typing in polymorphic languages. Journal of Functional Programming, 5:111– 130, 1995.
3. T. Altenkirch and B. Reus. Monadic Presentation of Lambda Terms Using Generalised Inductive Types. In J. Flum and M. Rodriguez-Artalejo, editors, CSL’99: Computer Science Logic, pages 453–468, 1999.
4. A. I. Baars and S. D. Swierstra. Typing dynamic typing. ICFP’02: International Conference on Functional Programming, pages 157–166, 2002.
5. E. Brady, C. McBride, and J. McKinna. Inductive families need not store their indices. In TYPES’03: Types for Proofs and Programs, pages 115–129. Springer, 2004.
6. C. Casinghino, V. Sjöberg, and S. Weirich. Combining proofs and programs in a dependently typed language. In POPL’14: Principles of Programming Languages, pages 33–45, 2014.
7. M. M. T. Chakravarty, G. Keller, and S. Peyton Jones. Associated type synonyms. In POPL’05: Principles of Programming Languages, pages 241–253, 2005.
8. M. M. T. Chakravarty, G. Keller, S. Lee, T. L. McDonell, and V. Grover. Accelerating Haskell array codes with multicore GPUs. In DAMP’11: Declarative Aspects of Multicore Programming, pages 3–14, 2011.
9. J. Cheney and R. Hinze. First-class phantom types. Technical report, Cornell University, 2003.
10. P.-E. Dagand and C. McBride. Transporting functions across ornaments. In ICFP’12: International Conference on Functional Programming, pages 103–114, 2012.
11. C. V. Hall, K. Hammond, S. Peyton Jones, and P. L. Wadler. Type classes in Haskell. TOPLAS’96: Transactions on Programming Languages and Systems, 18(2):109–138, Mar. 1996.
12. H.-S. Ko and J. Gibbons. Relational algebraic ornaments. In DTP’13: Dependently-Typed Programming, pages 37–48, 2013.
13. X. Leroy and M. Mauny. Dynamics in ML. In Functional Programming Languages and Computer Architecture, pages 406–426, 1991.
14. C. McBride. Type-Preserving Renaming and Substitution. Journal of Functional Programming, 2006.
15. C. McBride. Ornamental algebras, algebraic ornaments. Journal of Functional Programming, to appear.
16. T. L. McDonell, M. M. T. Chakravarty, G. Keller, and B. Lippmeier. Optimising purely functional GPU programs. In ICFP’13: International Conference on Functional Programming, pages 49–60, 2013.
17. T. L. McDonell, M. M. T. Chakravarty, V. Grover, and R. R. Newton. Type-safe Runtime Code Generation: Accelerate to LLVM. In Haskell Symposium, pages 201–212, 2015.
18. X. Ou, G. Tan, Y. Mandelbaum, and D. Walker. Dynamic typing with dependent types (extended abstract). In TCS’04: International Conference on Theoretical Computer Science, pages 437–450, August 2004.
19. J. Peterson and M. Jones. Implementing type classes. In PLDI’93: Programming Language Design and Implementation, pages 227–236, June 1993.
20. T. Schrijvers, S. Peyton Jones, M. M. T. Chakravarty, and M. Sulzmann. Type checking with open type functions. In ICFP’08: International Conference on Functional Programming, pages 51–62, 2008.
21. T. Schrijvers, S. Peyton Jones, M. Sulzmann, and D. Vytiniotis. Complete and decidable type inference for GADTs. In ICFP’09: International Conference on Functional Programming, pages 341–352, 2009.
22. T. Sheard and S. Peyton Jones. Template meta-programming for Haskell. In Haskell Workshop, pages 1–16, 2002.
23. M. Shields, T. Sheard, and S. Peyton Jones. Dynamic typing as staged type inference. In POPL’98: Principles of Programming Languages, pages 289–302, 1998.
24. V. Simonet and F. Pottier. A constraint-based approach to guarded algebraic data types. TOPLAS’07: Transactions on Programming Languages and Systems, 29(1):1, 2007.
25. Z. Somogyi, F. J. Henderson, and T. C. Conway. Mercury, an efficient purely declarative logic programming language. Australian Computer Science Communications, 17:499–512, 1995.
26. D. Syme, K. Battocchi, K. Takeda, D. Malayeri, and T. Petricek. Themes in information-rich functional programming for internet-scale data sources. In DDFP’13: Data Driven Functional Programming, pages 1–4, 2013.
27. D. Vytiniotis, S. Peyton Jones, and J. P. Magalhães. Equality Proofs and Deferred Type Errors: A Compiler Pearl. In ICFP’12: International Conference on Functional Programming, pages 341–352, 2012.
28. T. Williams, P.-E. Dagand, and D. Rémy. Ornaments in practice. In WGP’14: Workshop on Generic Programming, pages 15–24, 2014.

Index Terms

• Software and its engineering

  • Software notations and tools

    • General programming languages

      • Language types

        • Functional languages