Ambivalent Types for Principal Type Inference with GADTs

Abstract : GADTs, short for Generalized Algebraic DataTypes, which allow constructors of algebraic datatypes to be non-surjective, have many useful applications. However, pattern matching on GADTsintroduces local type equality assumptions, which are a source of ambiguities that may destroy principal types---and must be resolved by type annotations. We introduce ambivalent types to tighten the definition of ambiguities and better confine them, so that type inference has principal types, remains monotonic, and requires fewer type annotations.
Type de document :
Communication dans un congrès
Chung-chieh Shan. APLAS 2013 - 11th Asian Symposium on Programming Languages and Systems, 2013, Melbourne, Australia. 8301, pp.257-272, 2013, Lecture Notes in Computer Science; Programming Languages and Systems - 11th Asian Symposium. <10.1007/978-3-319-03542-0_19>
Liste complète des métadonnées


https://hal.inria.fr/hal-00914560
Contributeur : Didier Rémy <>
Soumis le : jeudi 5 décembre 2013 - 15:48:43
Dernière modification le : lundi 5 octobre 2015 - 16:56:18
Document(s) archivé(s) le : samedi 8 avril 2017 - 04:46:29

Fichier

Garrigue-Remy_gadts_applas2013...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Jacques Garrigue, Didier Rémy. Ambivalent Types for Principal Type Inference with GADTs. Chung-chieh Shan. APLAS 2013 - 11th Asian Symposium on Programming Languages and Systems, 2013, Melbourne, Australia. 8301, pp.257-272, 2013, Lecture Notes in Computer Science; Programming Languages and Systems - 11th Asian Symposium. <10.1007/978-3-319-03542-0_19>. <hal-00914560>

Partager

Métriques

Consultations de
la notice

125

Téléchargements du document

76