optional static typing for Python

[Diez B. Roggisch]

> If Python could be automatically converted to Ada or Java, that could
> potentially be used as a baseline for actual operational software.
> That would capture the algorithmic details more reliably than recoding
> from scratch by hand. But such an automatic conversion is not feasible
> without explicit typing.

If python could be automatically converted to ADA or Java, it wouldn't be
python. The fundamental difference IS the lack of static type annotations.
The problem is that people often confuse type inference with dynamic
typing, because it looks similar - but it isn't the same. All typeinference
does is to take an expression like this:

a = 10 * 100

and place type-variables on it, like this:

a:t_0 = 10:int * 100:int

Actually, the multiplication also gets annotated, like this:

a:t_0 = *(10:int, 100:int):t_1

Then the unknown type variables are inferred - it is known (and that is an
important property: ALL FUNCTIONS ARE KNOWN AT THIS POINT) that there
exists a multiplication function that has this signature:

_ * _ : [int, int] -> int

so t_1 can be inferred to be int, thus t_0 can be inferred to be int as
well.

But the key-point is: each and every function declaration is and has to be
fully statically typed. And all of them have to be known at compile-time!!
And of course this extends to classes or interfaces and such.

There are some nice tricks like generic types that themselves containt
type-variables in their declaration, so that you can declcare e.g. map,
reduce, filter and so forth in generic ways. But they are _fully_ type
annotated.

And the "normal" (Henly/Millner) type inference fails to produce correct
results in cases like this:

def foo(arg):
    if arg > 10:
       return 100
    else:
       return "n/a"

Which is perfectly legal and sometimes useful in python. Yes, there is
dependent typing, but this also goes only so far.

Additionally, it can be shown that type-inferencing becomes
non-deterministic or even unsolvable in the very moment you start
introducing recursive types - so, away with lists, arrays, trees and so
forth. Which of course also means that the statically typed languages will
produce errors, unless you restrict them heavily with respect to dynamic
memory allocation and so forth (that restricted ADA variant sometimes
popping up in discussions about this is one such case)

bottom-line: type-inference doesn't do magic, fully staticly annotated
languages still fail, and efforts like shedskin are interesting but will
never grow to a full-fledged python. And adding static type-declarations to
python will make it NotPython, a totally different language.

Diez