Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00073205
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 12:11:22 PM
Last modification on : Thursday, October 22, 2020 - 12:22:01 PM
Long-term archiving on: : Sunday, April 4, 2010 - 11:38:01 PM

Identifiers

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

Share

Metrics

Record views

834

Files downloads

4825