GADT meet Subtyping

TL;DR

This paper explores the integration of generalized algebraic datatypes (GADTs) with subtyping, focusing on variance annotations, their soundness, and providing an algorithm for checking them, relevant to ML-like languages.

Contribution

It introduces a formal analysis of variance in GADTs with subtyping, and presents a sound and complete algorithm for variance checking.

Findings

Variance annotations in GADTs are subtle and require careful handling.

A sound and complete algorithm for checking GADT variance has been developed.

The work applies to ML-like languages with explicit subtyping and constraints.

Abstract

While generalized abstract datatypes (GADT) 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.