Ambivalent Types for Principal Type Inference with GADTs (extended version)

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 :
Pré-publication, Document de travail
2013
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00914493
Contributeur : Didier Rémy <>
Soumis le : mardi 10 décembre 2013 - 22:02:41
Dernière modification le : mardi 17 avril 2018 - 11:24:09
Document(s) archivé(s) le : samedi 8 avril 2017 - 05:43:04

Fichier

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

Identifiants

  • HAL Id : hal-00914493, version 2

Collections

Citation

Jacques Garrigue, Didier Rémy. Ambivalent Types for Principal Type Inference with GADTs (extended version). 2013. 〈hal-00914493v2〉

Partager

Métriques

Consultations de la notice

124

Téléchargements de fichiers

109