Type Inference in the Presence of Subtyping: from Theory to Practice

Abstract : From a purely theoretical point of view, type inference for a functional language with parametric polymorphism and subtyping poses little difficulty. Indeed, it suffices to generalize the inference algorithm used in the ML language, so as to deal with type inequalities, rather than equalities. However, the number of such inequalities is linear in the program size-whence, from a practical point of view, a serious efficiency and readability problem. To solve this problem, one must simplify the inferred constraints. So, after studying the logical properties of subtyping constraints, this work proposes several simplification algorithms. They combine seamlessly, yielding a homogeneous, fully formal framework, which directly leads to an efficient implementation. Although this theoretical study is performed in a simplified setting, numerous extensions are possible. Thus, this framework is realistic, and should allow a practical appearance of subtyping in languages with type inference. This document is the English version of the author's PhD thesis.
Type de document :
Rapport
[Research Report] RR-3483, INRIA. 1998
Liste complète des métadonnées

https://hal.inria.fr/inria-00073205
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 12:11:22
Dernière modification le : samedi 17 septembre 2016 - 01:27:26
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:38:01

Fichiers

Identifiants

  • HAL Id : inria-00073205, version 1

Collections

Citation

François Pottier. Type Inference in the Presence of Subtyping: from Theory to Practice. [Research Report] RR-3483, INRIA. 1998. 〈inria-00073205〉

Partager

Métriques

Consultations de la notice

493

Téléchargements de fichiers

2474