[Python-Dev] Do PEP 526 type declarations define the types of variables or not?

[Steven D'Aprano]

On Mon, Sep 05, 2016 at 04:26:17PM +0100, Mark Shannon wrote:

> In this example:
> 
>     def bar()->Optional[int]: ...
> 
>     def foo()->int:
>         x:Optional[int] = bar()
>         if x is None:
>             return -1
>         return x
>
> According to PEP 526 the annotation `x:Optional[int]`
> means that the *variable* `x` has the type `Optional[int]`.

We can change that to read:

    x = bar()

and let the type-checker infer the type of x. Introducing the annotation 
here is a red-herring: you have *exactly* the same issue whether we do 
type inference, a type comment, or the proposed variable annotation.



> So what is the type of `x` in `return x`?

The type of *the variable x* is still Optional[int]. But that's the 
wrong question.

The right question is, what's the type of the return result?

The return result is not "the variable x". The return result is the 
value produced by evaluating the expression `x` in the specific context 
of where the return statement is found.

(To be precise, it is the *inferred* return value, of course, since the 
actual return value won't be produced until runtime.)


> If it is `Optional[int]`, then a type checker is obliged to reject this 
> code. 

Not at all, because the function isn't returning "the variable x". It's 
returning the value currently bound to x, and *that* is known to be an 
int. It has to be an int, because if it were None, the function would 
have already returned -1.

The return result is an expression that happens to consist of just a 
single term, in this case `x`. To make it more clear, let's change it 
to `return x+999`.

The checker should be able to infer that since `x` must be an int here, 
the expression `x+999` will also be an int. This satisfies the return 
type. Of course `x+999` is just a stand-in for any expression that is 
known to return an int, and that includes the case where the expression 
is `x` alone.

There's really not anything more mysterious going on here than the case 
where we have a Union type with two branches that depend on which type 
x actually is:


def demo(x:Union[int, str])->int:
    # the next two lines are expected to fail the type check
    # since the checker can't tell if x is an int or a str
    x+1
    len(x)
    # but the rest of the function should pass
    if isinstance(x, int):
        # here we know x is definitely an int
        y = x + 1
    if isinstance(x, str):
        # and here we know x is definitely a str
        y = len(x)
    return y



When I run MyPy on that, it gives:

[steve at ando ~]$ mypy test.py
test.py: note: In function "demo":
test.py:6: error: Unsupported operand types for + ("Union[int, str]" and "int")
test.py:7: error: Argument 1 to "len" has incompatible type "Union[int, str]"; expected "Sized"


But all of this is a red herring. It has nothing to do with the proposed 
variable annotation syntax: it applies equally to type comments and 
function annotations.



-- 
Steve