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

[Guido van Rossum]

On Tue, Sep 6, 2016 at 8:25 AM, Mark Shannon  wrote:
> The "smartness" of checkers is not the problem (for this example, at least)
> the problem is that checkers must conform to the rules laid down in PEP 484
> and (in whatever form it finally takes) PEP 526.
> It sounds like mypy doesn't conform to PEP 526, as it ignoring the declared
> type of x and using the inferred type.
> In fact it looks as if it is doing exactly what I proposed, which is that
> the annotation describes the type of the expression, not the variable.

IMO neither PEP requires type checkers to behave this way. Maybe you
read it between the lines when you reviewed PEP 484 and neither of us
realized that we were interpreting the text differently? The words you
have quoted previously mean different things to me than you seem to
imply.

>> I guess this is a surprise if you think of type systems like Java's
>> where the compiler forgets what it has learned, at least from the
>> language spec's POV. But a Python type checker is more like a linter,
>> and false positives (complaints about valid code) are much more
>> problematic than false negatives (passing invalid code).

> The language of PEP 526 is strongly suggestive of a type system like Java.

That suggestion is really in your mind. The PEP also quite clearly
states that it does not specify what a type checker should do with the
"declarations".

> The extensive use of the term 'variable' rather than 'expression' and
> 'assignment' rather suggests that all definitions and uses of a single
> variable have the same type.

Maybe you believe that Python's use of the word 'variable', combined
with using `=` for assignment, also implies that Python's "variables"
should behave like Java's "variables"?

> The problem with using the term "variable" is that it is *not* vague.
> Variables in python have well defined scopes and lifetimes.

So? When a type checker can prove that in the expression `f(x)`, the
type of the *expression* `x` will be compatible with the argument type
expected by f, isn't that good enough? Why would the type given for
the *variable* `x` have to be the only input to the type check for
that expression?

-- 
--Guido van Rossum (python.org/~guido)
___
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/archive%40mail-archive.com

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

[Chris Angelico]

On Wed, Sep 7, 2016 at 4:11 AM, Stephen J. Turnbull
 wrote:
> Finally, the notion of annotating expressions is incoherent:
>
> # Annotating (sub)expressions: the more the merrier!
> (x) : bool = (((y): int + (z): float) / (w): complex): quarternion
> # Ooh, an expression with no past and no future.  Annotate it!
> (y + z) / w: quarternion

Can't do that - parsing would become ambiguous.

x = {1:int, 1.5:float, 2+3j:complex}
print(type(x))

ChrisA
___
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/archive%40mail-archive.com

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

[Stephen J. Turnbull]

Mark Shannon writes:

 > The problem with using the term "variable" is that it is *not* vague. 
 > Variables in python have well defined scopes and lifetimes.

Sure, but *hints* are not well-defined by Python (except the syntax,
once PEP 526 is implemented).  A *hint* is something that the
typechecker takes note of, and then does whatever it pleases with it.

So can we do the practical thing here and agree that even though the
type hint on a variable is constant, what the typechecker does with
that type hint in different contexts might change?


The rest is tl;dr (why I want type hints on variables, and why the
term "annotating expressions" leaves me cold).

I don't see how you can interpret

z: complex = 1.0

without a notion of annotating the variable.  The RHS is clearly of
float type, and Python will assign a float to z.  What's going on
here?  Maybe this:

from math import exp

z: complex = 1.0
print(exp(z))

==> "MyPy to Steve!  MyPy to Steve!  You are confused!"

Maybe "math" was a typo for "cmath".  Maybe "complex" was a premature
generalization.  Maybe you wouldn't want to hear about it ... but I
would.  I think.  Anyway, to find out if I *really* want that or not,
I need a notion of hinting the variable.

But: "although practicality beats purity".  Like everybody else, I
want a typechecker that minds its manners and says nothing about

from math import exp

z: complex = 1.0
try:
print(exp(z))
except TypeError:
print("Oh well, complex is better than complicated.")

Finally, the notion of annotating expressions is incoherent:

# Annotating (sub)expressions: the more the merrier!
(x) : bool = (((y): int + (z): float) / (w): complex): quarternion
# Ooh, an expression with no past and no future.  Annotate it!
(y + z) / w: quarternion

Noone has any intention of annotating expressions AFAICS -- people who
talk about that really mean annotating the *value* of the expression
on the RHS, but since it will *always* be on the RHS of an assignment,
it's equivalent to annotating the value of the *target* on the LHS.

___
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/archive%40mail-archive.com

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

[Ivan Levkivskyi]

On 6 September 2016 at 18:35, Nick Coghlan  wrote:

> On 7 September 2016 at 01:33, Ivan Levkivskyi 
> wrote:
> > On 6 September 2016 at 17:25, Mark Shannon  wrote:
> >>
> >> The issue is not whether the checker can tell that the type of the
> >> *expression* is int, but whether it is forced to use the type of the
> >> *variable*. The current wording of PEP 526 strongly implies the latter.
> >
> > Mark,
> > Could you please point to exact locations in the PEP text and propose an
> > alternative wording, so that we will have a more concrete discussion.
>
> Rather than trying to work that out on the list, it may make the most
> sense for Mark to put together a PR that rewords the parts of the PEP
> that he sees as constraining typecheckers to restrict *usage* of a
> variable based on its annotation, rather than just restricting future
> bindings to it.
>

Thanks Nick, this is a good idea.
Mark, I will be glad to discuss your PR to the master python/peps repo.

--
Iavn
___
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/archive%40mail-archive.com

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

[Nick Coghlan]

On 7 September 2016 at 01:33, Ivan Levkivskyi  wrote:
> On 6 September 2016 at 17:25, Mark Shannon  wrote:
>>
>> The issue is not whether the checker can tell that the type of the
>> *expression* is int, but whether it is forced to use the type of the
>> *variable*. The current wording of PEP 526 strongly implies the latter.
>
> Mark,
> Could you please point to exact locations in the PEP text and propose an
> alternative wording, so that we will have a more concrete discussion.

Rather than trying to work that out on the list, it may make the most
sense for Mark to put together a PR that rewords the parts of the PEP
that he sees as constraining typecheckers to restrict *usage* of a
variable based on its annotation, rather than just restricting future
bindings to it.

It seems to me everyone's actually in pretty good agreement on how we
want variable annotations to work (constraining future assignments to
abide by the declaration, without constraining use when inference
indicates a more specific type), but the PEP may be using some
particular terminology more loosely than is strictly correct in the
context of type theory.

Cheers,
Nick.

-- 
Nick Coghlan   |   ncogh...@gmail.com   |   Brisbane, Australia
___
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/archive%40mail-archive.com

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

[Ivan Levkivskyi]

On 6 September 2016 at 17:25, Mark Shannon  wrote:

> The issue is not whether the checker can tell that the type of the
> *expression* is int, but whether it is forced to use the type of the
> *variable*. The current wording of PEP 526 strongly implies the latter.
>

Mark,
Could you please point to exact locations in the PEP text and propose an
alternative wording, so that we will have a more concrete discussion.

--
Ivan
___
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/archive%40mail-archive.com

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

[Mark Shannon]

On 05/09/16 18:40, Guido van Rossum wrote:

On Mon, Sep 5, 2016 at 8:26 AM, Mark Shannon  wrote:

PEP 526 states that "This PEP aims at adding syntax to Python for annotating
the types of variables" and Guido seems quite insistent that the
declarations are for the types of variables.

However, I get the impression that most (all) of the authors and proponents
of PEP 526 are quite keen to emphasise that the PEP in no way limits type
checkers from doing what they want.

This is rather contradictory. The behaviour of a typechecker is defined by
the typesystem that it implements. Whether a type annotation determines the
type of a variable or an expression alters changes what typesystems are
feasible. So, stating that annotations define the type of variables *does*
limit what a typechecker can or cannot do.

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.

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]`.
So what is the type of `x` in `return x`?
If it is `Optional[int]`, then a type checker is obliged to reject this
code. If it is `int` then what does "type of a variable" actually mean,
and why aren't the other uses of `x` int as well?


Oh, there is definitely a problem here if you interpret it that way.
Of course I assume that other type checkers are at least as smart as
mypy. :-) In mypy, the analysis of this example narrows the type x can
have once `x is None` is determined to be false, so that the example
passes.


The "smartness" of checkers is not the problem (for this example, at 
least) the problem is that checkers must conform to the rules laid down 
in PEP 484 and (in whatever form it finally takes) PEP 526.
It sounds like mypy doesn't conform to PEP 526, as it ignoring the 
declared type of x and using the inferred type.
In fact it looks as if it is doing exactly what I proposed, which is 
that the annotation describes the type of the expression, not the variable.




I guess this is a surprise if you think of type systems like Java's
where the compiler forgets what it has learned, at least from the
language spec's POV. But a Python type checker is more like a linter,
and false positives (complaints about valid code) are much more
problematic than false negatives (passing invalid code).


The language of PEP 526 is strongly suggestive of a type system like 
Java. The extensive use of the term 'variable' rather than 'expression' 
and 'assignment' rather suggests that all definitions and uses of a 
single variable have the same type.




So a Python type checker that is to gain acceptance of users must be
much smarter than that, and neither PEP 484 not PEP 526 is meant to
require a type checker to complain about `return x` in the above
example.

I'm not sure how to change the language of the PEP though -- do you
have a suggestion? It all seems to depend on how the reader interprets
the meaning of very vague words like "variable" and "type".

The problem with using the term "variable" is that it is *not* vague. 
Variables in python have well defined scopes and lifetimes.



Cheers,
Mark.


___
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/archive%40mail-archive.com

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

[Mark Shannon]

On 05/09/16 23:16, Greg Ewing 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...


How does that differ from annotating the type of the expression?




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.



The issue is not whether the checker can tell that the type of the 
*expression* is int, but whether it is forced to use the type of the 
*variable*. The current wording of PEP 526 strongly implies the latter.


Cheers,
Mark.
___
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/archive%40mail-archive.com

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

[Koos Zevenhoven]

On Tue, Sep 6, 2016 at 1:49 AM, Sven R. Kunze  wrote:
> Didn't Koos say this works more like an expression annotation?
>
> IMO, the type of the expression is what is specified but the type of the
> variable can change over time (as you demonstrated).

That's exactly the kind of semantics I'm describing in the
python-ideas thread. An that's exactly how Python works: the type of a
variable can change every time you assign a value to it (but not in
between, unless you're doing funny stuff). So in a sense you annotate
the *value* by annotating the variable at the point in the function
where the value is assigned to it.

There are open questions in this approach of course. But if you're
interested, don't hesitate to discuss or ask questions in the
python-ideas thread. I won't answer before I wake up, though ;).

-- Koos


>
> Sven
>
>
> PS: thinking this way, the new syntax is actually confusing as it annotates
> the variable not the expression. :-/
>
>
>
> On 05.09.2016 17:26, Mark Shannon wrote:
>>
>> Hi,
>>
>> PEP 526 states that "This PEP aims at adding syntax to Python for
>> annotating the types of variables" and Guido seems quite insistent that the
>> declarations are for the types of variables.
>>
>> However, I get the impression that most (all) of the authors and
>> proponents of PEP 526 are quite keen to emphasise that the PEP in no way
>> limits type checkers from doing what they want.
>>
>> This is rather contradictory. The behaviour of a typechecker is defined by
>> the typesystem that it implements. Whether a type annotation determines the
>> type of a variable or an expression alters changes what typesystems are
>> feasible. So, stating that annotations define the type of variables *does*
>> limit what a typechecker can or cannot do.
>>
>> 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.
>>
>> 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]`.
>> So what is the type of `x` in `return x`?
>> If it is `Optional[int]`, then a type checker is obliged to reject this
>> code. If it is `int` then what does "type of a variable" actually mean,
>> and why aren't the other uses of `x` int as well?
>>
>> Cheers,
>> Mark.
>> ___
>> 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/srkunze%40mail.de
>
>
>



-- 
+ Koos Zevenhoven + http://twitter.com/k7hoven +
___
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/archive%40mail-archive.com

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

[Sven R. Kunze]

Didn't Koos say this works more like an expression annotation?

IMO, the type of the expression is what is specified but the type of the 
variable can change over time (as you demonstrated).


Sven


PS: thinking this way, the new syntax is actually confusing as it 
annotates the variable not the expression. :-/



On 05.09.2016 17:26, Mark Shannon wrote:

Hi,

PEP 526 states that "This PEP aims at adding syntax to Python for 
annotating the types of variables" and Guido seems quite insistent 
that the declarations are for the types of variables.


However, I get the impression that most (all) of the authors and 
proponents of PEP 526 are quite keen to emphasise that the PEP in no 
way limits type checkers from doing what they want.


This is rather contradictory. The behaviour of a typechecker is 
defined by the typesystem that it implements. Whether a type 
annotation determines the type of a variable or an expression alters 
changes what typesystems are feasible. So, stating that annotations 
define the type of variables *does* limit what a typechecker can or 
cannot do.


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.


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]`.
So what is the type of `x` in `return x`?
If it is `Optional[int]`, then a type checker is obliged to reject 
this code. If it is `int` then what does "type of a variable" actually 
mean,

and why aren't the other uses of `x` int as well?

Cheers,
Mark.
___
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/srkunze%40mail.de



___
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/archive%40mail-archive.com

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

[Peter Ludemann via Python-Dev]

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 
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
>
___
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/archive%40mail-archive.com

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

[Greg Ewing]

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/archive%40mail-archive.com

Re: [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@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
___
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/archive%40mail-archive.com

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

[Guido van Rossum]

On Mon, Sep 5, 2016 at 8:26 AM, Mark Shannon  wrote:
> PEP 526 states that "This PEP aims at adding syntax to Python for annotating
> the types of variables" and Guido seems quite insistent that the
> declarations are for the types of variables.
>
> However, I get the impression that most (all) of the authors and proponents
> of PEP 526 are quite keen to emphasise that the PEP in no way limits type
> checkers from doing what they want.
>
> This is rather contradictory. The behaviour of a typechecker is defined by
> the typesystem that it implements. Whether a type annotation determines the
> type of a variable or an expression alters changes what typesystems are
> feasible. So, stating that annotations define the type of variables *does*
> limit what a typechecker can or cannot do.
>
> 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.
>
> 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]`.
> So what is the type of `x` in `return x`?
> If it is `Optional[int]`, then a type checker is obliged to reject this
> code. If it is `int` then what does "type of a variable" actually mean,
> and why aren't the other uses of `x` int as well?

Oh, there is definitely a problem here if you interpret it that way.
Of course I assume that other type checkers are at least as smart as
mypy. :-) In mypy, the analysis of this example narrows the type x can
have once `x is None` is determined to be false, so that the example
passes.

I guess this is a surprise if you think of type systems like Java's
where the compiler forgets what it has learned, at least from the
language spec's POV. But a Python type checker is more like a linter,
and false positives (complaints about valid code) are much more
problematic than false negatives (passing invalid code).

So a Python type checker that is to gain acceptance of users must be
much smarter than that, and neither PEP 484 not PEP 526 is meant to
require a type checker to complain about `return x` in the above
example.

I'm not sure how to change the language of the PEP though -- do you
have a suggestion? It all seems to depend on how the reader interprets
the meaning of very vague words like "variable" and "type".

-- 
--Guido van Rossum (python.org/~guido)
___
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/archive%40mail-archive.com

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

[Ryan Gonzalez]

Maybe the PEP should just say it's for "annotating variables", and it would
mention "primarily for the purpose of types"?

--
Ryan
[ERROR]: Your autotools build scripts are 200 lines longer than your
program. Something’s wrong.
http://kirbyfan64.github.io/
On Sep 5, 2016 10:27 AM, "Mark Shannon"  wrote:

> Hi,
>
> PEP 526 states that "This PEP aims at adding syntax to Python for
> annotating the types of variables" and Guido seems quite insistent that the
> declarations are for the types of variables.
>
> However, I get the impression that most (all) of the authors and
> proponents of PEP 526 are quite keen to emphasise that the PEP in no way
> limits type checkers from doing what they want.
>
> This is rather contradictory. The behaviour of a typechecker is defined by
> the typesystem that it implements. Whether a type annotation determines the
> type of a variable or an expression alters changes what typesystems are
> feasible. So, stating that annotations define the type of variables *does*
> limit what a typechecker can or cannot do.
>
> 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.
>
> 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]`.
> So what is the type of `x` in `return x`?
> If it is `Optional[int]`, then a type checker is obliged to reject this
> code. If it is `int` then what does "type of a variable" actually mean,
> and why aren't the other uses of `x` int as well?
>
> Cheers,
> Mark.
> ___
> 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/rymg19%
> 40gmail.com
>
___
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/archive%40mail-archive.com

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

[Mark Shannon]

Hi,

PEP 526 states that "This PEP aims at adding syntax to Python for 
annotating the types of variables" and Guido seems quite insistent that 
the declarations are for the types of variables.


However, I get the impression that most (all) of the authors and 
proponents of PEP 526 are quite keen to emphasise that the PEP in no way 
limits type checkers from doing what they want.


This is rather contradictory. The behaviour of a typechecker is defined 
by the typesystem that it implements. Whether a type annotation 
determines the type of a variable or an expression alters changes what 
typesystems are feasible. So, stating that annotations define the type 
of variables *does* limit what a typechecker can or cannot do.


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.


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]`.
So what is the type of `x` in `return x`?
If it is `Optional[int]`, then a type checker is obliged to reject this 
code. If it is `int` then what does "type of a variable" actually mean,

and why aren't the other uses of `x` int as well?

Cheers,
Mark.
___
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/archive%40mail-archive.com