GADT meet subtyping

Abstract : While generalized abstract datatypes 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 and involves new semantic properties of types that raise interesting design questions. We allow variance annotations in GADT definitions, present a sound and effective algorithm to check such declarations, and describe its application in a real-world language.
Document type :
Conference papers
Complete list of metadatas

Cited literature [3 references]  Display  Hide  Download

https://hal.inria.fr/hal-01093940
Contributor : Scherer Gabriel <>
Submitted on : Thursday, December 18, 2014 - 9:03:52 AM
Last modification on : Tuesday, November 20, 2018 - 11:06:03 PM
Long-term archiving on : Saturday, April 15, 2017 - 7:20:17 AM

File

scherer_remy_gadts_variance_ml...
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01093940, version 1

Collections

Relations

Citation

Gabriel Scherer, Didier Rémy. GADT meet subtyping. ACM SIGPLAN Workshop on ML, Aug 2012, Copenhague, Denmark. ⟨hal-01093940⟩

Share

Metrics

Record views

90

Files downloads

55