GADT meet Subtyping

Résumé : Les types algébriques généralisés (\textit{Generalized Algebraic Datatypes}, \GADTs) sont maintenant bien compris, mais leur ajout à un langage équipé de sous-typage nous réservait quelques surprises. Qu'est-ce qu'être covariant pour un paramètre de \GADT? % La réponse s'avère être subtile. Elle met en jeu des propriétés fines de la relation de sous-typage qui soulèvent d'intéressantes problématiques de conception de langage. % Nous permettons des annotations de variance dans les définitions de \GADTs, étudions leur correction, et présentons un algorithme correct et complet pour les vérifier. Notre travail peut s'appliquer à un langage complet inspiré de ML et avec sous-typage explicite, tel que OCaml, ou même à des langages avec des contraintes générales de sous-typage.
Type de document :
Rapport
[Research Report] RR-8114, INRIA. 2012, pp.33
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00744292
Contributeur : Scherer Gabriel <>
Soumis le : lundi 22 octobre 2012 - 16:57:20
Dernière modification le : samedi 17 septembre 2016 - 01:37:29
Document(s) archivé(s) le : mercredi 23 janvier 2013 - 03:44:02

Fichiers

Identifiants

  • 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〉

Partager

Métriques

Consultations de
la notice

154

Téléchargements du document

181