Skip to Main content Skip to Navigation
New interface
Reports (Research report)

GADT meet Subtyping

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.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [2 references]  Display  Hide  Download
Contributor : Scherer Gabriel Connect in order to contact the contributor
Submitted on : Monday, October 22, 2012 - 4:57:20 PM
Last modification on : Thursday, October 27, 2022 - 4:02:44 AM
Long-term archiving on: : Wednesday, January 23, 2013 - 3:44:02 AM


Files produced by the author(s)


  • HAL Id : hal-00744292, version 1
  • ARXIV : 1210.5935


Gabriel Scherer, Didier Rémy. GADT meet Subtyping. [Research Report] RR-8114, INRIA. 2012, pp.33. ⟨hal-00744292⟩



Record views


Files downloads