Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Wed 21 Sep 2016 10:35 - 11:00 at Noh Theater - Session 9 Chair(s): Sam Lindley

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.

Wed 21 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

10:35 - 12:15
Session 9Research Papers at Noh Theater
Chair(s): Sam Lindley University of Edinburgh, UK
10:35
25m
Talk
Ghostbuster: A Tool for Simplifying and Converting GADTs
Research Papers
Trevor L. McDonell Indiana University, USA, Timothy A. K. Zakian Oxford University, UK, Matteo Cimini Indiana University, USA, Ryan R. Newton Indiana University, USA
DOI
11:00
25m
Talk
Indexed Codata Types
Research Papers
David Thibodeau McGill University, Canada, Andrew Cave McGill University, Canada, Brigitte Pientka McGill University, Canada
DOI
11:25
25m
Talk
Disjoint Intersection Types
Research Papers
Bruno C. d. S. Oliveira University of Hong Kong, China, Zhiyuan Shi University of Hong Kong, China, João Alpuim University of Hong Kong, China
DOI
11:50
25m
Talk
Set-Theoretic Types for Polymorphic Variants
Research Papers
Giuseppe Castagna Paris Diderot University & CNRS, Tommaso Petrucciani University of Genoa, France, Kim Nguyễn University of Paris-Sud, France
DOI