GADTs meet subtyping - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

GADTs meet subtyping

Résumé

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.
Fichier principal
Vignette du fichier
esop.pdf (263 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00772993 , version 1 (11-01-2013)
hal-00772993 , version 2 (14-01-2013)

Identifiants

Citer

Gabriel Scherer, Didier Rémy. GADTs meet subtyping. ESOP 2013 - 22nd European Symposium on Programming, Mar 2013, Rome, Italy. pp.554-573, ⟨10.1007/978-3-642-37036-6⟩. ⟨hal-00772993v2⟩

Collections

INRIA INRIA2
325 Consultations
776 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More