Python from Wise Guy's Viewpoint

[Joachim Durchholz]

Don Geddis wrote:

> Dirk Thierbach <dthierbach at gmx.de> writes:
> 
>>Hindley-Milner type inference always terminates. The result is either
>>a provable mismatch, or a provable-non-mismatch.
> 
> You're completely wrong, which can be easily demonstrated.
> 
> The fact that it terminates isn't the interesting part.  Any inference
> procedure can also "always terminate" simply by having a timeout, and reporting
> "no proof" if it can't find one in time.

Now you are completely wrong.
Of course you can make any type checker terminate by such draconian 
measures, but such a type system would be near-useless: code may 
suddenly become incorrect if compiled on a smaller machine.

There are better ways of doing this, like cutting down on the size of 
some intermediate result during type checking (such as C++, where 
template nesting depth or something similar is cut off at a relatively 
small, fixed number IIRC).
Standard type systems don't have, need or want such cut-offs though :-)

> So what's interesting is whether the conclusions are correct.
> 
> Let's take as our ideal what a dynamic type system (say, a program in Lisp)
> would report upon executing the program.  The question is, can your type
> inference system make exactly the same conclusions at compile time, and predict
> all (and only!) the type errors that the dynamic type system would report at
> run time?
> 
> The answer is no.

Not precisely.
The next question, however, is whether the programs where the answers 
differ are interesting.
There's also a narrow and a broad sense here: obviously, it's not 
possible to type check all Lisp idioms, but are we allowed to present 
alternative idioms that do type check and serve the same purpose?

[Snipping the parts that are getting ad hominem-ish :-( ]

Regards,
Jo