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.
Type de document :
Communication dans un congrès
ACM SIGPLAN Workshop on ML, Aug 2012, Copenhague, Denmark. 2012, 〈http://www.lexifi.com/ml2012/〉
Liste complète des métadonnées

Littérature citée [3 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01093940
Contributeur : Scherer Gabriel <>
Soumis le : jeudi 18 décembre 2014 - 09:03:52
Dernière modification le : vendredi 25 mai 2018 - 12:02:07
Document(s) archivé(s) le : samedi 15 avril 2017 - 07:20:17

Fichier

scherer_remy_gadts_variance_ml...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. 2012, 〈http://www.lexifi.com/ml2012/〉. 〈hal-01093940〉

Partager

Métriques

Consultations de la notice

73

Téléchargements de fichiers

45