Search for: All records

Abstract Generalized Algebraic Data Types(GADTs) are a syntactic generalization of the usual algebraic data types (ADTs), such as lists, trees, etc. ADTs’ standard initial algebra semantics (IAS) in the category$$\mathit{Set}$$of sets justify critical syntactic constructs – such as recursion, pattern matching, and fold – for programming with them. In this paper, we show that semantics for GADTs that specialize to the IAS for ADTs are necessarily unsatisfactory. First, we show that the functorial nature of such semantics for GADTs in$$\mathit{Set}$$introducesghostelements, i.e., elements not writable in syntax. Next, we show how such ghost elements break parametricity. We observe that the situation for GADTs contrasts dramatically with that for ADTs, whose IAS coincides with the parametric model constructed via their Church encodings in System F. Our analysis reveals that the fundamental obstacle to giving a functorial IAS for GADTs is the inherently partial nature of their map functions. We show that this obstacle cannot be overcome by replacing$$\mathit{Set}$$with other categories that account for this partiality. 

Relational parametricity was first introduced by Reynolds for System F. Although System F provides a strong model for the type systems at the core of modern functional programming languages, it lacks features of daily programming practice such as complex data types. In order to reason parametrically about such objects, Reynolds’ seminal ideas need to be generalized to extensions of System F. Here, we explore such a generalization for the extension of System F by Generalized Algebraic Data Types (GADTs) as found in Haskell. Although GADTs generalize Algebraic Data Types (ADTs) — i.e., simple recursive types such as lists, trees, etc. — we show that naively extending the parametric treatment of these recursive types is not enough to tackle GADTs. We propose a tentative workaround for this issue, borrowing ideas from the categorical semantics of GADTs known as “functorial completion”. We discuss some applications, as well as some limitations, of this solution. 

We show that GADTs' inherent partiality is incompatible with functoriality in categories equipped with structures of computational partiality. 

We expose a fundamental incompatibility between GADTs’ function-mapping operations and function composition. To do this, we consider sound and complete semantics of GADTs in a series of natural categorical settings. We first consider interpreting GADTs naively as functors on categories interpreting types. But GADTs’ function-mapping operations are not total in general, so we consider semantics in categories that allow partial morphisms. Unfortunately, however, GADTs’ function-mapping operations do not preserve composition of partial morphisms. This compels us to relax functors’ composition preserving property, and thus to interpret GADTs as lax functors. This exposes yet another behavior of GADTs that is not computationally reasonable: if G interprets a GADT, then G(f) can be defined on more elements than G(g) even though f is defined on fewer elements than g. 

It is well-known that GADTs do not admit standard map functions of the kind supported by ADTs and nested types. In addition, standard map functions are insufficient to distribute their data-changing argument functions over all of the structure present in elements of deep GADTs, even just deep ADTs or nested types. This paper develops an algorithm that characterizes those functions on a (deep) GADT’s type arguments that are mappable over its elements. The algorithm takes as input a term t whose type is an instance of a (deep) GADT G, and returns a set of constraints a function must satisfy to be mappable over t. This algorithm, and thus this paper, can in some sense be read as defining what it means for a function to be mappable over t: f is mappable over an element t of G precisely when it satisfies the constraints returned when our algorithm is run on t and G. This is significant: to our knowledge, there is no existing definition or other characterization of the intuitive notion of mappability for functions over GADTs.