GADTs 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, Sep 2012, Copenhagen, Denmark. 2012, <http://www.lexifi.com/ml2012/>
Liste complète des métadonnées

https://hal.inria.fr/hal-01093816
Contributeur : Didier Rémy <>
Soumis le : jeudi 11 décembre 2014 - 11:02:31
Dernière modification le : mercredi 14 décembre 2016 - 01:07:55
Document(s) archivé(s) le : jeudi 12 mars 2015 - 10:23:22

Fichier

Scherer-Remy:gadts-subtyping@m...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01093816, version 1

Collections

Citation

Gabriel Scherer, Didier Rémy. GADTs Meet Subtyping. ACM SIGPLAN Workshop on ML, Sep 2012, Copenhagen, Denmark. 2012, <http://www.lexifi.com/ml2012/>. <hal-01093816>

Partager

Métriques

Consultations de
la notice

34

Téléchargements du document

66