[Types-sig] Proposed Goals PEP

[Tim Peters]

[Tim Hochberg, perhaps the only person so far in this round to
 actually talk about how to spell and implement a workable type
 annotation system for Python ...
]

Good show, fellow Tim!

> THE BASICS
>
> Consider this code (syntax borrowed from one of Guido's old proposals):
>
> def spam(eggs : Integer, beans : File) -> String:
>    #....
>    return x
>
> This would be compiled to:
>
> def spam(eggs, bakedBeans):
>    if __typecheck__ and not Integer.check(eggs): raise
> TypeError("Informative message here")
>    if __typecheck__ and not File.check(beans): raise TypeError("Informative
> message here")
>    # ...
>    if __typecheck__ and not String.check(x): raise TypeError("Informative
> message here")
>    return x
>
> Note that Integer, File and String are all bound when the def is executed,
> just like default argument are now. Also, __typecheck__ is magic variable
> similar to debug so that typechecks can be omitted completely during
> compilation so that there is no speed penalty when compiled this way.

Everybody got that?  The rest (see Tim's msg) is elaboration.  Type checkers
are spelled via instances of classes with .check(object) methods.  Everything
else follows from that.  You can get all the ERR and DOC benefits anyone
could ask for within a week; and wrt ERR, anything can be checked that you
can write Python code *to* check.  OPT and GLUE aren't particularly helped at
all.  Tough.

I suggest changing the codegen like so:

def f(p1: T1, p2: T2, ..., pn: Tn) -> Tr:
    if __typecheck__:
        T1.check(p1, msg1)
        T2.check(p2, msg2)
        ...
        Tn.check(pn, msgn)

1. It's less code.

2. The compiler today isn't actually smart enough to optimize away
       if 0 and y:
           xxx
   blocks.  It is smart enough to optimize away
       if 0:
           xxx
   blocks (same deal with __debug__ today).

3. The .check() method is the proper place to raise an exception.

4. But the calling code is the proper place to construct part of the
   error message, because it has easy access to useful symbolic info
   about the function (like the names of the arguments).

return expr

needs to change into (in general)

    _unique_temp = expr
    if __typecheck__:
        Tr.check(_unique_temp, msgr)
    return _unique_temp

which is less trivial to implement via a source-to-source translator, but
still easy.

Before:

def lastelement(t: AnyType, x: SequenceOf(t)) -> t:
    return x[-1]

After:

if __typecheck__:
    # typecheck is a module containing std check objects like
    # AnyType and SequenceOf, etc.
    # Of course users can code their own check objects too.
    from typecheck import *

def lastelement(t, x):
    if __typecheck__:
        AnyType.check(t, "lastelement argument t")
        SequenceOf(t).check(x, "lastelement argument x")
    temp = x[-1]
    if __typecheck__:
        t.check(temp, "lastelement return expression x[-1]")
    return temp

Subtlety:  the "t" argument above has to be a check object itself.  That
means AnyType.check(t) has to be able to determine whether t *is* a check
object.  This would be a great time to insist that all check objects be
instances of subclasses of a base TypeCheck class, so that isinstance(t,
TypeCheck) is sufficient.  I don't see that anything would be gained by
continuing the usual dance of saying "well, if it has a .check() attribute,
then I can't prove it's *not* a typecheck object, so I'll just assume that it
is".

> ...
> SUMMARY
>
> This idea looks like a good starting point to me. It's simple, it can
> express complex types, it helps both err and doc. On the downside, it's
> unlikely to help opt, and I don't know about glue.

Take heart:  the same people who believe Python can magically infer types
can't deny that it could just as magically track down the defns of the check
objects and infer everything useful about them too <wink>.

if-the-implementation-is-easy-to-explain-it-may-be-a-good-idea-ly y'rs
    - tim