[TYPES] papers about type inference with subtyping

[Michal Moskal]

Hello,

I'm working on the type inference engine in Nemerle (http://nemerle.org/).
This is going to be a complete redesign. I'm willing to write a technical
paper with theoretical foundations along with the implementation.

Our type system is embedded in the .NET one (Java-like object oriented,
with parametric polymorphism, type variables can be constrained),
though enriched with the function types and possibly co/contravariance
(how this is going to be compiled is another matter).

There are a few requirements for the type inference engine. The most
important one is that I'm going to trade completeness for simplicity.
Error messages are also particularly important.

There are also some additional issues making type inference harder,
or at least different then in OO ML extensions -- static overloading,
mutability, nominal type system (no structural subtyping) and local
functions to name a few.

I'm asking for pointers to papers. I did some googling, and citeseer
traversing, read about type inference through constraint solving, local
type inference and so on. I'm just willing to make sure I did not miss
something.

I'm leaning toward some restricted form of constraint solving. The current
solution is a variant of the Cardelli's greedy algorithm from F<: --
it unifies variables once and for all. This is a problem, since given:

	class C1 : C {}
	class C2 : C {}

the list [C1, C2] fails to type (while it have the list<C> type).

Another issue is that "List.Map (some_list, fun (x) { x.foo })" does not
type. "fun (x) { x.foo }"  cannot, since the `foo' field can be in several
classes, and we do not have a proper type to express that. However if we
know that some_list has type list<Bar>, and Bar has the "foo" field, then
everything is OK, and we should be able to type it. However we cannot.

This two issues (and the second one in particular) turned out to be
a problem in practice. There are also some issues with overloading
resolution.

Anyway I guess I can solve the problems above with constraint propagation,
and I think I have an efficient way to solve the equations on the fly.

-- 
: Michal Moskal :: http://www.kernel.pl/~malekith :: GCS !tv h e>+++ b++
: ::: Logic is a nice contrast to the Real World. :: UL++++$ C++ E--- a?