一句话：提出 Ghostbuster，可省略选定类型参数来生成简化 GADT，并自动生成类型安全的往返转换函数。
GADT 可以在构造子类型中编码非平凡性质，但操作此类数据类型的代码必须提供证明以维持这些性质，才能通过类型检查。Ghostbuster 通过省略选定的类型参数来生成 GADT 的简化版本，在保留原递归结构的同时弱化保证、减少操作所需义务。与 ornament 类似，它关注信息保持的双向变换，并自动生成原类型与简化类型之间的类型安全转换函数，证明二者复合后是恒等函数。作者在 Hackage 上的数千个 GADT 上评估了 Haskell 原型，成功生成更简单的 Haskell'98 数据类型以及往返转换函数。
Abstract 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.
@article{paperbot341,
title = {Ghostbuster: A tool for simplifying and converting GADTs},
author = {TIMOTHY A. K. ZAKIAN and TREVOR L. MCDONELL and MATTEO CIMINI and RYAN R. NEWTON},
journal = {Journal of Functional Programming},
volume = {28},
year = {2018},
doi = {10.1017/s0956796818000114}
}