(original) (raw)

I would take the opposite approach from Greg Ewing, namely that the annotation is not a permission of values but a starting point for the type inferencer; and the type checker/inferencer can complain if there's an inconsistency (for some definition of "inconsistency", which is not defined in the PEP). In most cases, this distinction doesn't matter, but it does affect what kinds of errors or warnings are generated.

But ... perhaps people are overthinking these things? If we go back to the example without variable annotation:
def bar()->Optional\[int\]: ...

def foo():
x = bar()
if x is None:
return -1
return x

then a straightforward flow-tracing type inferencer can \*infer\* all the annotations in foo:

def foo() -> int: # \*not\* Optional\[int\] - see below
x:Optional\[int\] = bar() # derived from definition of bar
if x is None: # consistent with x:Optional\[int\]
return -1 # implies return type of foo
return x # implies return type of foo as Union\[int, None\] minus None, that is: int

That is, the type annotations add no information in this example, but might be useful to a human. Perhaps they wouldn't show in the source code at all, but would instead be put into a database, for use by development tools - for example, Kythe-flavored tools, where the type data (and other usage information) are used for code search, editing, refactoring, etc. (Or the type information could be kept in a .pyi stub file, with an automated "merge" tool putting them into the .py file as desired.)

On the other hand, a non-flow-tracing inferencer would derive 'def foo() -> Optional\[int\]' ... it would be a design choice of the type checker/inferencer as to whether that's an error, a warning, or silently allowed ... I can see arguments for all of these choices.

In most cases, there's seldom any need for the programmer to add annotations to local variables. Global variables and class/instance attributes, however, can benefit from annotation.

(As to my credentials, which some people seem to crave: I worked on an earlier version of Google's Python type inferencer (pytype) and I'm currently working on pykythe (to be open-sourced), which takes the function-level information and propagates it to the local variables, then adds that information (together with call graph information) to a Kythe database.)



On 5 September 2016 at 15:16, Greg Ewing <greg.ewing@canterbury.ac.nz> wrote:
Mark Shannon wrote:

Unless of course, others may have a different idea of what the "type of a variable" means.
To me, it means it means that for all assignments \`var = expr\`
the type of \`expr\` must be a subtype of the variable,
and for all uses of var, the type of the use is the same as the type of the variable.

I think it means that, at any given point in time, the
value of the variable is of the type of the variable or
some subtype thereof. That interpretation leaves the
type checker free to make more precise inferences if
it can. For example, in...

def foo()->int:
x:Optional\[int\] = bar()
if x is None:
return -1
return x

...the type checker could notice that, on the branch
containing 'return x', the value of x must be of type
int, so the code is okay.

\--
Greg


\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_
Python-Dev mailing list
Python-Dev@python.org
https://mail.python.org/mailman/listinfo/python-dev
Unsubscribe: https://mail.python.org/mailman/options/python-dev/pludemann%40google.com