Hostname: page-component-586b7cd67f-rdxmf Total loading time: 0 Render date: 2024-11-24T23:15:37.989Z Has data issue: false hasContentIssue false
  • English
  • Français

Ghostbuster: A tool for simplifying and converting GADTs

Published online by Cambridge University Press:  22 June 2018

TIMOTHY A. K. ZAKIAN ,
TREVOR L. MCDONELL ,
MATTEO CIMINI  and
RYAN R. NEWTON
TIMOTHY A. K. ZAKIAN
Affiliation:
University of Oxford, Department of Computer Science, Oxford, UK (e-mail: [email protected])
TREVOR L. MCDONELL
Affiliation:
University of New South Wales, School of Computer Science and Engineering, Sydney, AUS (e-mail: [email protected])
MATTEO CIMINI
Affiliation:
University of Massachusetts Lowell, Department of Computer Science, Lowell, MA, USA (e-mail: [email protected])
RYAN R. NEWTON
Affiliation:
Indiana University, School of Informatics, Computing, and Engineering, Bloomington, IN, USA (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Generalized Algebraic Data Types, 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 toward 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.

Type
Research Article
Information
Journal of Functional Programming , Volume 28 , 2018 , e16
Copyright
Copyright © Cambridge University Press 2018 

References

Abadi, M., Cardelli, L., Pierce, B., & Rémy, D. (1995) Dynamic typing in polymorphic languages. J. Funct. Program. 5, 111–130.Google Scholar
Abadi, M., Cardelli, L., Pierce, B. & Plotkin, G. (1989) Dynamic typing in a statically-typed language. ACM Trans. Program. Lang. Syst. 13 (2), 237–268.CrossRefGoogle Scholar
Altenkirch, T. & Reus, B. (1999) Monadic presentation of lambda terms using generalised inductive types. In Computer Science Logic, Flum, J. & Rodriguez-Artalejo, M. (eds). Berlin, Heidelberg: Springer, pp. 453–468.Google Scholar
Appel, A. W. (2007) Compiling with Continuations. New York, NY, USA: Cambridge University Press.Google Scholar
Appel, A. W. & Jim, T. (1997) Shrinking lambda expressions in linear time. J. Funct. Program. 7 (5), 515–540.CrossRefGoogle Scholar
Baars, A. I. & Swierstra, S. D. (2002a) Typing dynamic typing. In ICFP02: International Conference on Functional Programming, pp. 157–166.Google Scholar
Baars, A. I. & Swierstra, S. D. (2002b) Typing dynamic typing. In Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming, ICFP '02. New York, NY, USA: ACM, pp. 157–166.CrossRefGoogle Scholar
Benton, N., Kennedy, A., Lindley, S. & Russo, C. (2005) Shrinking Reductions in sml.net. Berlin, Heidelberg: Springer, pp. 142–159.Google Scholar
Bernardy, J.-P., Boespflug, M., Newton, R. R., Peyton, Jones S. & Spiwack, A. (2018) Linear Haskell: Practical linearity in a higher-order polymorphic language. Proc. ACM Program. Lang. 2 (POPL), 5:1–5:29CrossRefGoogle Scholar
Brady, E., McBride, C. & McKinna, J. (2004) Inductive families need not store their indices. In Types for Proofs and Programs, Stefano, B., Mario, C. & Damiani, F. (eds). Berlin, Heidelberg: Springer, pp. 115–129.Google Scholar
Casinghino, C., Sjöberg, V. & Weirich, S. (2014) Combining proofs and programs in a dependently typed language. In POPL'14: Principles of Programming Languages, pp. 33–45.Google Scholar
Chakravarty, M. M. T., Keller, G., Lee, S., McDonell, T. L. & Grover, V. (2011) Accelerating Haskell array codes with multicore GPUs. In DAMP'11: Declarative Aspects of Multicore Programming, pp. 3–14.Google Scholar
Chakravarty, M. M. T., Keller, G. & Peyton, Jones S. (2005) Associated type synonyms. In POPL'05: Principles of Programming Languages, pp. 241–253.CrossRefGoogle Scholar
Cheney, J. & Hinze, R. (2002) A lightweight implementation of generics and dynamics. In Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell'02. New York, NY, USA: ACM, pp. 90–104.Google Scholar
Cheney, J. & Hinze, R. (2003) First-Class Phantom Types. Technical Report, Cornell University.Google Scholar
Dagand, P.-E. & McBride, C. (2012) Transporting functions across ornaments. In ICFP'12: International Conference on Functional Programming, pp. 103–114.Google Scholar
Dagand, P.-E., Tabareau, N. & Tanter, É. (2016) Partial type equivalences for verified dependent interoperability. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP'16. New York, NY, USA: ACM, pp. 298–310.CrossRefGoogle Scholar
Findler, R. B. & Felleisen, M. (2002 October) Contracts for higher-order functions. In Proceedings of the International Conference on Functional Programming, ICFP, pp. 48–59.Google Scholar
Hall, C. V., Hammond, K., Peyton Jones, S. & Wadler, P. L. (1996) Type classes in Haskell. ACM Trans. Program. Lang. Syst. 18 (2), 109–138.CrossRefGoogle Scholar
Henglein, F. (1994) Dynamic typing: Syntax and proof theory. Sci. Comput. Program. 22 (3), 197–230.Google Scholar
Knuth, D. E. (1968) Semantics of context-free languages. Math. Syst. Theory 2 (2), 127–145.Google Scholar
Ko, H.-S. & Gibbons, J. (2013) Relational algebraic ornaments. In DTP'13: Dependently-Typed Programming, pp. 37–48.Google Scholar
Leroy, X. & Mauny, M. (1991) Dynamics in ML. In Functional Programming Languages and Computer Architecture, pp. 406–426.CrossRefGoogle Scholar
McBride, C. (2005) Type-preserving renaming and substitution [online]. Accessed March 30, 2018. Available at: http://strictlypositive.org/ren-sub.pdfGoogle Scholar
McBride, C. (2010) Ornamental algebras, algebraic ornaments [online]. Accessed March 30, 2018. Available at: https://personal.cis.strath.ac.uk/conor.mcbride/pub/OAAO/Ornament.pdfGoogle Scholar
McDonell, T. L., Chakravarty, M. M. T., Keller, G. & Lippmeier, B. (2013) Optimising purely functional GPU programs. In ICFP'13: International Conference on Functional Programming, pp. 49–60.CrossRefGoogle Scholar
McDonell, T. L., Chakravarty, M. M. T., Grover, V. & Newton, R. R. (2015) Type-safe runtime code generation: Accelerate to LLVM. In Proceedings of the Haskell Symposium, pp. 201–212.Google Scholar
McDonell, T. L., Zakian, T. A. K., Cimini, M. & Newton, R. R. (2016) Ghostbuster: A tool for simplifying and converting GADTs. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP'16. New York, NY, USA: ACM, pp. 338–350.CrossRefGoogle Scholar
Ou, X., Tan, G., Mandelbaum, Y. & Walker, D. (2004 August) Dynamic typing with dependent types (extended abstract) In TCS'04: International Conference on Theoretical Computer Science, pp. 437–450.Google Scholar
Peterson, J. & Jones, M. (1993 June) Implementing type classes. In PLDI'93: Programming Language Design and Implementation, pp. 227–236.Google Scholar
PeytonJones, S. Jones, S., Weirich, S., Eisenberg, R. A. & Vytiniotis, D. (2016) A Reflection on Types. Cham: Springer International Publishing, pp. 292–317.Google Scholar
Schrijvers, T., PeytonJones, S. Jones, S., Chakravarty, M. M. T. & Sulzmann, M. (2008) Type checking with open type functions. In ICFP'08: International Conference on Functional Programming, pp. 51–62.CrossRefGoogle Scholar
Schrijvers, T., Peyton Jones, S., Sulzmann, M. & Vytiniotis, D. (2009a) Complete and decidable type inference for GADTs. In ICFP'09: International Conference on Functional Programming, pp. 341–352.CrossRefGoogle Scholar
Schrijvers, T., Peyton Jones, S., Sulzmann, M. & Vytiniotis, D. (2009b) Complete and decidable type inference for GADTs. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming, ICFP'09. New York, NY, USA: ACM, pp. 341–352.CrossRefGoogle Scholar
Sheard, T. & Peyton Jones, S. (2002) Template meta-programming for Haskell. In Proceedings of the Haskell Workshop, pp. 1–16.Google Scholar
Shields, M., Sheard, T. & Peyton Jones, S. (1998) Dynamic typing as staged type inference. In POPL'98: Principles of Programming Languages, pp. 289–302.Google Scholar
Siek, J. G. & Taha, W. (2006) Gradual typing for functional languages. In Proceedings of the Scheme and Functional Programming Workshop, vol. 6, pp. 81–92.Google Scholar
Simonet, V. & Pottier, F. (2007) A constraint-based approach to guarded algebraic data types. ACM Trans. Program. Lang. Syst. 29 (1), 1.CrossRefGoogle Scholar
Somogyi, Z., Henderson, F. J. & Conway, T. C. (1995) Mercury, an efficient purely declarative logic programming language. Aust. Comput. Sci. Commun. 17, 499–512.Google Scholar
Sulzmann, M. & Wang, M. (2004) A Systematic Translation of Guarded Recursive Data Types to Existential Types. Technical Report, National University of Singapore.Google Scholar
Syme, D., Battocchi, K., Takeda, K., Malayeri, D. & Petricek, T. (2013) Themes in information-rich functional programming for internet-scale data sources. In DDFP'13: Data Driven Functional Programming, pp. 1–4.Google Scholar
Tobin-Hochstadt, S. & Felleisen, M. (2006) Interlanguage migration: From scripts to programs. In Proceedings of the Dynamic Languages Symposium.Google Scholar
Tobin-Hochstadt, S. & Felleisen, M. (2010a) Logical types for untyped languages. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP'10. New York, NY, USA: ACM, pp. 117–128.Google Scholar
Tobin-Hochstadt, S. & Felleisen, M. (2010b) Logical types for untyped languages. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP'10. New York, NY, USA: ACM, pp. 117–128.Google Scholar
Vytiniotis, D., Peyton Jones, S. & Magalhães, J. P. (2012) Equality proofs and deferred type errors: A compiler pearl. In ICFP'12: International Conference on Functional Programming, pp. 341–352.Google Scholar
Wadler, P. & Findler, R. B. (2009 March) Well-typed programs can't be blamed. In Proceedings of the European Symposium on Programming, ESOP, pp. 1–16.Google Scholar
Weirich, S. (2000) Type-safe cast: (functional pearl). In Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming, ICFP'00. New York, NY, USA: ACM, pp. 58–67.Google Scholar
Williams, T., Dagand, P.-É. & Rémy, D. (2014) Ornaments in practice. In WGP'14: Workshop on Generic Programming, pp. 15–24.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.