[Types-sig] Implementability

[Martijn Faassen]

Tim Peters wrote:
> 
> [Tim]
> > making this [global type inference] all run efficiently (in either
> > time or space) is a Professional Pain in the Professional Ass.
> 
> [Paul Prescod]
> > According to the principle of "from each according to their
> > talents"
> 
> I'm afraid you've mistaken Benevolent Dictatorship for some variant of
> Communism <wink>.
> 
> > you should be writing this optimizing, static type checker.
> 
> Guido is the one interested in magical type inference; I'm not.  I'm happy
> to explicitly declare the snot out of everything when I want something from
> static typing.

Yay, someone on my side, and it's Tim too! (now I get to watch Tim drag
himself quickly out of this and into a position completely incompatible
with mine :)

>  Merely checking that my declared types match my usage is
> much easier (doesn't require any flow analysis).  The good news is that I
> couldn't make time to write an inferencer even if I wanted to; if I had
> time, I'd be much more likely to write something that *used* explicit
> declarations to generate faster code.

Right -- this would be the first step towards a magic inferencer anyway;
you simply let it come up with 'explicit' declarations by itself, which
you then fit into your optimizer.

[snip]
> > The types of globals from other modules should be explicitly declared.
> 
> A global type inferencer can usually figure that out on its own.  There's
> more than one issue being discussed here, alas -- blame Guido <0.9 wink>.
> 
> > If they aren't, they are presumed to have type PyObject or to return
> > PyObject. Or they just aren't available if you are in strict static
> > type check mode.
> 
> In the language of the msg to which you're replying, they're associated with
> the universal set (the set of all types) -- same thing.  Then e.g.
> 
>     declared_int = unknown
> 
> is an error, but

Or, if you're interfacing with untyped python, this could raise a
run-time exception if unknown doesn't turn out to be an integer. Or do
you disagree with this?

>     unknown1 = unknown2
> 
> is not.  Whether
> 
>     unknown = declared_int
> 
> should be an error is a policy issue.  Many will claim it should be an
> error, but the correct answer <wink> is that it should not.

This would seem to be the natural way to do it; I'm not sure why many
would claim it should be an error. Could you explain?

> Types form a
> lattice, in which "unknown" is the top element, and the basic rule of type
> checking is that the binding
> 
>     lhs = rhs
> 
> is OK iff
> 
>     type(lhs) >= type(rhs)
> 
> where ">=" is wrt the partial ordering defined by the type lattice (or, in
> English <wink>, only "widening" bindings are OK; like assigning an int to a
> real, or a subclass to a base class etc, but not their converses).

I agree.

Regards,

Martijn