Python from Wise Guy's Viewpoint

[Dirk Thierbach]

Don Geddis <don at geddis.org> wrote:
>> prunesquallor at comcast.net reasonably noted:
>> > If there are three values that can arise --- provable-mismatch,
>> > provable-non-mismatch, and undecided --- then you cannot assume that
>> > ~provable-mismatch = provable-non-mismatch.
> 
> 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.

Unfortunately, I can *prove* that the HM-type inference always terminates,
without any timeout, by induction on the length of the expression.

> 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.

Yes, you can do that. But it's not done during HM-type inference.

> 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.

Right. It cannot, because that question is not decidable. 

> That's one obvious case, so even you know that your claim of a "provable
> mismatch" is incorrect.  

It's still a provable mismatch. Only that part of the code never gets
executed, so you don't have a dynamic type error. I would consider a
program which has a branch that contains an error, but fortunately
never executes that branch pretty bogus. I don't see any advantage
in admitting such a program. It's a bad program, and you should either
correct the error in the dead branch, or remove the dead branch 
completely if it isn't going to be executed anyway.

> There are programs that will never have run-time
> errors, but your static type inference will claim a type error.

Yes. But these programs will have problems, even without a run-time error. 
Rewrite them to increase the quality of your software.

>> or because you have an implicit restriction for possible arguments to this
>> expression the type system doesn't know about, than you could call it a
>> "valid program", but it will still be rejected, yes.

> For example:
>        (defun foo (x)
>          (check-type x (integer 0 10))
>          (+ 1 x) )
>        (defun fib (n)
>          (check-type n (integer 0 *))
>          (if (< n 2)
>              1
>              (+ (fib (- n 1)) (fib (- n 2))) ))
>        (print (foo (fib 5)))

> This program prints "9", and causes no run-time type errors.  Will
> it be successfully type-checked at compile time by a static system?
> Almost certainly the answer is no.

It will be successfully type checked, because the static type system
does not allow you to express assumptions about value ranges of types.
These things have to be checked dynamically, as in your program. So the
type system "doesn't get in the way": It admits the program.

> Unfortunately, the only way to figure this out is to actually
> compute the fifth Fibonacci number, which surely no static type
> inference system is going to do.

Yes. That's why you cannot express such restrictions statically.

> Do you now accept that your static type inference systems do NOT partition
> all programs into "either a provable [type] mismatch, or a provable [type]
> non-mismatch"?

No. But you probably don't understand what I mean with that. A provable
type mismatch means that the program contains a location where it can
be statically verified that executing the location will cause trouble.
It cannot statically check that this location will be indeed executed,
so it might (wrongly) reject the program. But this rejection is acceptable,
because the program is bogus. On the other hand, if there is no static 
type mismatch, that doesn't mean that the program will not crash because
of runtime errors (division by zero, or dynamically checked restrictions).

> Finally, to get back to the point of the dynamic typing fans:
> realizing that type inference is not perfect, we're annoyed to be
> restricted to writing only programs that can be successfully type
> checked at compile time.

You may not believe it, but I perfectly understand that :-) The
problem is that this is just not true (with a good static type
system): It is not a real restriction. If your program is a good
program, it will type check. If it doesn't type check, then there is
something wrong with it.

I am annoyed in the very same way if I have to write programs in a
language with a bad type system (say, C++). I cannot express myself as
abstractly as I would want to, I have to write down lots of
unnecessary type annotions, and I have to invent tricks to please the
type checker and let it allow me do what I want to do. Really
horrible.

Again, try thinking of the static type systems as an automatic testing
tool. Saying that you want to write programs that will be rejected by
the static typing is like saying that you want to write programs that
will be rejected by your unit tests. It just doesn't make any sense;
the unit tests are there to guarantee that you write good quality
software, so why would you want to ignore them? The only case when you
want to do that is if they are bad tests; when they point to problems
that are not really there. But with a good static type system, that
doesn't happen.

- Dirk