A Type Inference System Based on Saturation of Subtyping Constraints

Abstract : This paper presents a powerful and flexible technique for defining type inference algorithms, on an ML-like language, that involve subtyping and whose soundness can be proved. We define a typing algorithm as a set of inference rules of three distinct forms: typing rules collect subtyping constraints to be satisfied, instantiation rules instantiate type schemes, and saturation rules specify how to check the validity and consistency of collected constraints. Essentially, type inference then proceeds in two intertwined phases: one that extracts constraints and the other that saturates the sets of constraints. Our technique extends easily to the treatment of high-level features such as polymorphism, overloading, variants and pattern-matching, or generalized algebraic data types (GADTs).
Type de document :
Communication dans un congrès
Trends in Functional Programming, Jun 2016, College Park (MD), United States. Trends in Functional Programming. 16th International Symposium, TFP 2016, College Park (MD), USA, June 8-10, 2016. Revised Selected Papers (to appear)
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01413043
Contributeur : Michel Mauny <>
Soumis le : vendredi 9 décembre 2016 - 11:40:20
Dernière modification le : jeudi 16 novembre 2017 - 17:12:03
Document(s) archivé(s) le : jeudi 23 mars 2017 - 09:43:28

Fichier

article.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01413043, version 1

Citation

Benoît Vaugon, Michel Mauny. A Type Inference System Based on Saturation of Subtyping Constraints. Trends in Functional Programming, Jun 2016, College Park (MD), United States. Trends in Functional Programming. 16th International Symposium, TFP 2016, College Park (MD), USA, June 8-10, 2016. Revised Selected Papers (to appear). 〈hal-01413043〉

Partager

Métriques

Consultations de la notice

158

Téléchargements de fichiers

92