GADTs meet subtyping

TL;DR

This paper explores the complex interaction between generalized algebraic datatypes (GADTs) and subtyping, focusing on variance annotations, their soundness, and providing an algorithm for checking them, with implications for ML-like languages.

Contribution

It introduces a nuanced understanding of covariance in GADTs within subtyping systems and presents a sound, complete algorithm for variance checking.

Findings

Variance annotations in GADTs can be soundly checked with the proposed algorithm.

The interaction between GADTs and subtyping involves subtle properties affecting language design.

The work applies to ML-like languages with explicit subtyping, such as OCaml.

Abstract

While generalized algebraic datatypes (\GADTs) are now considered well-understood, adding them to a language with a notion of subtyping comes with a few surprises. What does it mean for a \GADT parameter to be covariant? The answer turns out to be quite subtle. It involves fine-grained properties of the subtyping relation that raise interesting design questions. We allow variance annotations in \GADT definitions, study their soundness, and present a sound and complete algorithm to check them. Our work may be applied to real-world ML-like languages with explicit subtyping such as OCaml, or to languages with general subtyping constraints.