[Types-sig] recursive types, type safety, and flow analysis

[Guido van Rossum]

[me]
> > Hm...  Since type checking is essentially a compile time activity, I
> > think it would be better if the run time order of events didn't
> > matter.

[Greg]
> But runtime order does matter.
> 
>    a = 1
>    func_taking_int(a)
>    a = "foo"
>    func_taking_string(a)
> 
> I can come up with all kinds of variants, but that's the basic pattern.
> The code is perfectly type-safe, and depends on the order of events. If we
> waited until the end, then "a" will either have type "String," or type
> "Int or String." Either way, it produces false errors.

If this pattern occurs locally (a is a local variable), fine.  The
flow analyzer will have no problem with this, and shouldn't find any
type errors.

But if a were a global, I'd say this was bad taste and asking for
trouble.

I'm giving up on responding point-by-point -- let's just agree that we
differ in opinion on this matter.

> But: it still doesn't allow for the recursive type declarators. To be
> clear, it allows:
> 
> def f() -> String:
>   return g()
> def g() -> String:
>   return "abc"
> 
> But it does not allow:
> 
> def f(x: Foo):
>   ...
> class Foo:
>   ...

If there's only one Foo (which is usually the case) I still think this
is too strict, and I don't see a technical reason why it would be
necessary.

> I believe the compiler should be recording information about the function
> arguments' typedecls. Unless the compiler is going to have multiple passes
> then the name should be defined before usage.
> 
> Or rather, let's assume that the function argument information is
> constructed and recorded at runtime (as part of the standard function
> object construction at runtime). Then you really have to ensure that name
> is available, so the appropriate value can be stored into the function
> object.

OK, this is why we disagree.  I am only interested in compile time
type checking; I can admit that some run time checking is necessary,
but only in order to assert certain invariants that are assumed by the
compile time checker.  E.g. if I'm deducing that global X is a
constant, I'm going to make sure at run time it really won't change.
This catches several things: (1) dynamically loaded or generated code
that surreptitiously tries to change the value of a constant (memories
of Fortran...:); (2) other cases where (e.g. through unexpected
aliasing) the constant might be changed.

A form of type checking that happens completely at run time (the way
you describe it) is uninteresting to me, and using such a system as
the semantic basis for a type checker seems to be a mistake.  Yes,
this follows Python's semantics closer than what I am proposing.  But
I don't think that it is closer to what the user expects the type
checker to do.

Here's the crux of my argument:

    Python's dynamic semantics can often be surprising.  Compile time
    checking should warn the user about these surprises, it shouldn't
    try to assume that these surprises are what the user wanted!

(I've skipped the rest of what you wrote, because of the agreement to
disagree.)

--Guido van Rossum (home page: http://www.python.org/~guido/)