An official website of the United States government
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.
more »
« less
GADTs Are Not (Even Lax) Functors
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.
more »
« less
- Award ID(s):
- 1906388
- PAR ID:
- 10430342
- Date Published:
- Journal Name:
- Structure Meets Power
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
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.more » « less
-
This paper considers parametricity and its consequent free theorems for nested data types. Rather than representing nested types via their Church encodings in a higher-kinded or dependently typed extension of System F, we adopt a functional programming perspective and design a Hindley-Milner-style calculus with primitives for constructing nested types directly as fixpoints. Our calculus can express all nested types appearing in the literature, including truly nested types. At the level of terms, it supports primitive pattern matching, map functions, and fold combinators for nested types. Our main contribution is the construction of a parametric model for our calculus. This is both delicate andchallenging. In particular, to ensure the existence of semantic fixpoints interpreting nested types, and thus to establish a suitable Identity Extension Lemma for our calculus, our type system must explicitly track functoriality of types, and cocontinuity conditions on the functors interpreting them must be appropriately threaded throughout the model construction. We also prove that our model satisfies an appropriate Abstraction Theorem, as well as that it verifies all standard consequences of parametricity in the presence of primitive nested types. We give several concrete examples illustrating how our model can be used to derive useful free theorems, including a short cut fusion transformation, for programs over nested types. Finally, we consider generalizing our results to GADTs, and argue that no extension of our parametric model for nested types can give a functorial interpretation of GADTs in terms of left Kan extensions and still be parametric.more » « less
-
We present a grammar for a robust class of data types that includes algebraic data types (ADTs), (truly) nested types, generalized algebraic data types (GADTs), and their higher-kinded analogues. All of the data types our grammar defines, as well as their associated type constructors, are shown to have fully functorial initial algebra semantics in locally presentable categories. Since local presentability is a modest hypothesis, needed for such semantics for even the simplest ADTs, our semantic framework is actually quite conservative. Our results thus provide evidence that if a category supports fully functorial initial algebra semantics for standard ADTs, then it does so for advanced higher-kinded data types as well. To give our semantics we introduce a new type former called Lan that captures on the syntactic level the categorical notion of a left Kan extension. We show how left Kan extensions capture propagation of a data type’s syntactic generators across the entire universe of types, via a certain completion procedure, so that the type constructor associated with a data type becomes a bona fide functor with a canonical action on morphisms. A by-product of our semantics is a precise measure of the semantic complexity of data types, given by the least cardinal λ for which the functor underlying a data type is λ-accessible. The proof of our main result allows this cardinal to be read off from a data type definition without much effort. It also gives a sufficient condition for a data type to have semantic complexity ω, thus characterizing those data types whose data elements are effectively enumerable.more » « less
-
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.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- The DOI is not currently available.
