Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 12:11:22 PM
Last modification on : Thursday, February 3, 2022 - 11:14:06 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:38:01 PM


  • 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⟩



Record views


Files downloads