2012/10/22 by Gabriel Scherer, Scherer, Gabriel, Didier Rémy +1 · 1 citation
Computer Science · #FOS: Computer and information sciences #Programming Languages (cs.PL) #cs.PL
paper · pdf · doi:10.48550/arxiv.1210.5935
No. RR-8114 (2012)
arxiv created 2012/10/22 · arxiv updated 2012/10/23
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.