Ghostbuster: A tool for simplifying and converting GADTs

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 pap...

Full description

Saved in:
Bibliographic Details
Published in:Journal of functional programming 2018-01, Vol.28, Article e16
Main Authors: ZAKIAN, TIMOTHY A. K., MCDONELL, TREVOR L., CIMINI, MATTEO, NEWTON, RYAN R.
Format: Article
Language:English
Subjects:
Conversion
ICFP2016 special issue
Mathematical analysis
Properties (attributes)
Trip generation
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0956-7968
1469-7653
DOI:10.1017/S0956796818000114