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 :
[Research Report] RR-3483, INRIA. 1998
Liste complète des métadonnées

Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 12:11:22
Dernière modification le : vendredi 25 mai 2018 - 12:02:03
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:38:01



  • HAL Id : inria-00073205, version 1



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



Consultations de la notice


Téléchargements de fichiers