Python from Wise Guy's Viewpoint

[Don Geddis]

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

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.

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.

> A provable mismatch means that there is an execution branch that will crash
> if you ever get there. If for some reason this branch will never get
> executed, either because it's (non-provably) dead code

That's one obvious case, so even you know that your claim of a "provable
mismatch" is incorrect.  There are programs that will never have run-time
errors, but your static type inference will claim a type error.

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

So haven't you just contradicted yourself?  Perhaps you think this "implicit
restriction" is unfair, because you've kept information from the system.
But the real problem is that all the information might be there, but the
system isn't capable of making sufficient inferences to figure it out.

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.

In case the code isn't clear; FOO is a function that increments a number by
one.  Its domain is [0,10], and its range is [1,11].  FIB is the Fibonacci
sequence, with domain [0,infinity] and range [1,infinity].

Are you allowed to call FOO with the output of FIB?  In general, no, because
the range of FIB is much greater than the domain of FOO.

However, in the particular case of the particular code in this program, it
turns out that only (FIB 5) is called, which happens to compute to 8, well
within the domain of FOO.  Hence, no run-time type error.  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.  (And if you do
happen to find one, I'm sure I can come up with a version of the halting
problem that will break that system too.)

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"?

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.  Nobody
objects to doing compile-time type inference (e.g. as the CMUCL compiler for
Common Lisp does) -- especially just to generate warnings -- but many people
object to refusing to compile programs that can not be proven type-safe at
compile time (by your limited type inference systems).

        -- Don
_______________________________________________________________________________
Don Geddis                  http://don.geddis.org/               don at geddis.org