Early Announcement: Parametricity for GADTs

TL;DR

This paper extends the concept of relational parametricity to GADTs in Haskell, proposing a categorical semantics-based workaround to address the complexities introduced by GADTs.

Contribution

It generalizes Reynolds' parametricity to GADTs, introducing a categorical semantics approach to handle their complexities.

Findings

Naive extension of parametricity to GADTs is insufficient.

A workaround based on categorical semantics of GADTs is proposed.

Discussion of applications and limitations of the approach.

Abstract

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.