Ghostbuster: A tool for simplifying and converting GADTs
| Autor: | Ryan R. Newton, Trevor L. McDonell, Matteo Cimini, Timothy A. K. Zakian |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Theoretical computer science
Computer science 0102 computer and information sciences 02 engineering and technology Type (model theory) ENCODE computer.software_genre 01 natural sciences 0202 electrical engineering electronic engineering information engineering Code (cryptography) Identity function Algebraic number computer.programming_language Focus (computing) Recursion Programming language 020207 software engineering Ornaments Computer Graphics and Computer-Aided Design TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Algebraic data type Haskell Software_PROGRAMMINGLANGUAGES computer Software |
| Zdroj: | ICFP |
| ISSN: | 1469-7653 0956-7968 |
| Popis: | 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,allcode manipulating that datatype must provide proof that it maintains these properties in order to typecheck. In this paper, we take a step towardgradualizingthese 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. Likeornaments, 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|