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
Complete list of metadatas

Cited literature [2 references]  Display  Hide  Download

https://hal.inria.fr/hal-00744292
Contributor : Scherer Gabriel <>
Submitted on : Monday, October 22, 2012 - 4:57:20 PM
Last modification on : Tuesday, November 20, 2018 - 11:06:04 PM
Long-term archiving on : Wednesday, January 23, 2013 - 3:44:02 AM

Files

RR-8114.pdf
Files produced by the author(s)

Identifiers

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

Collections

Citation

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

Share

Metrics

Record views

213

Files downloads

233