[Prev][Next][Index][Thread]

A PhD thesis on type inference with subtyping


Hello,

I am pleased to announce that my PhD thesis, entitled

  "Type inference with subtyping: from theory to practice"

is now available electronically, at the following URLs:

  French  version: http://pauillac.inria.fr/~fpottier/publis/these-fpottier.ps.gz
  English version: http://pauillac.inria.fr/~fpottier/publis/thesis-fpottier.ps.gz

Here is a summary of this work:

>From a purely theoretical point of view, type inference for a
functional language with parametric polymorphism and subtyping poses
no difficulties. 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.

Thank you very much for your interest,

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/