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. © 2013 Springer-Verlag.
CITATION STYLE
Scherer, G., & Rémy, D. (2013). GADTs meet subtyping. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7792 LNCS, pp. 554–573). https://doi.org/10.1007/978-3-642-37036-6_30
Mendeley helps you to discover research relevant for your work.