> Hi,
>
> I would like to implement something similar to the type inference of
> ocaml for the python language. I have always found it very impressive
> (although I have only used caml light).
>
> I have no experience with the topic, it is just a project that seems
> cool to me :-)
>
> Do you have any hints or where I could build up my knowledge (code,
> books, article, ...) to do that kind of thing.
>
> I imagine that it works in a kind of three way pass:
>
> 1. analyse all the constraints of the code
> Ex:
> def f(a): a.append(1)
> def g(a): a=a+1; f(a)
> g('coucou')
>
> => a must support append
> => a must also be an int
>
> 2. cross-validate the constraints consistency
> => inconsistent assertions
>
> 3. validate the constraints against reality
> => g('coucou') will not work

In fact, the ML style type inference can be done in only one pass, at first
your variables are monomorphic then they're unified witht the first type
they match, creating linkages between types if needed. However in an OO
system such as Python, you need more than core ML type inference. You will
need some kind of structural subtyping, and subtyping is known to be tricky
when used together with polymorphism. There is several kind of subtyping
algorithms possible, using constraints is one of them (see work of François
Pottier on this).

I used another approach based on ocaml polymorphic variants typing scheme
(somehow reversed) to implement this feature in MTypes, but it still have a
lot of implementation holes difficult to handle. Also, the Python standard
library must be designed with dynamic typing in mind (several types possible
for arguments, variable number of arguments, operator overriding.....). It's
possible to rely on a dynamicly typed library but you'll have to constraint
the types a little more and add primitives so users can access different
kinds of features which are not usable anymore.

Good luck,
Nicolas Cannasse