PEP 526 - var annotations and the spirit of python

[Steven D'Aprano]

On Thu, 05 Jul 2018 16:09:52 +0200, Antoon Pardon wrote:

>> This is not an innovation of Mypy. It's how type inference is supposed
>> to work. If a particular type checker doesn't do that, it is doing it
>> wrong.
> 
> That is how type interference works in languages that have some kind of
> static typing like Haskell.

No, that's how type inference works in dynamically typed languages like 
Python as well. See Mypy for an example.

Do you have a counter-example? I'm happy to be corrected by facts, but 
not by suppositions about hypothetical type-checkers which might someday 
exist but don't yet.


> Sure if mypy want to impose something like
> that it can, but you can't interfere something like that for python
> programs in general.

Naturally -- that's why type-checking remains opt-in. Nobody, especially 
not me, says that if you see 

    x = 3

in a random Python program, that means that x must be an int everywhere 
in that program. That would be a foolish thing to say.

But if you opt-in to using a type-checker, the assumption is that you are 
writing in a less-dynamic, more-static style that will actually get some 
advantage from static type checking. If you're not doing so, then you're 
just annoying yourself and wasting time and you won't enjoy the 
experience one bit.

As many people -- including you, if I remember correctly -- have often 
pointed out, the amount of dynamism allowed in Python is a lot more than 
the amount typically used by most programs. Most of us, most of the time, 
treat variables as mostly statically typed. Reusing a variable for 
something completely unrelated is mildly frowned on, and in practice, 
most variables are only used for *one* thing during their lifetime.

Python remains a fundamentally dynamically typed language, so a static 
type checker (whether it has type inference or not) cannot cope. It 
requires gradual typing: a type system capable of dealing with mixed code 
with parts written in a static-like style and parts that remain fully 
dynamic.

Mypy makes pretty conservative decisions about which parts of your code 
to check. (E.g. it treats functions as duck-typed unless you explicitly 
annotate them.) But when it does infer types, it cannot always infer the 
type you, the programmer, intended. Often because there is insufficient 
information available:

    x = []  # we can infer that x is a list, but a list of what?
    x.append("hello world")  # allowed, or a type error?

And if the type checker turns out to make an overly-strict inference, and 
you want to overrule it, you can always annotate it as Any.

Type checking algorithms, whether static or gradual, are predicated on 
the assumption that the type of variable is consistent over the lifetime 
of that variable. (By type, I include unions, optional types, etc. "A 
float or a string" is considered a type for these purposes. So is 
"anything at all".) That's the only reasonable assumption to make for 
static analysis.

I'll grant you that a sufficiently clever type checking algorithm could 
track changes through time. Proof of concept is that we humans can do so, 
albeit imperfectly and often poorly, so it's certainly possible. But how 
we do it is by more-or-less running a simulated Python interpreter in our 
brain, tracking the types of variables as they change.

So *in principle* there could be a type-checker which does that, but as 
far as I know, there isn't such a beast. As far as I know, nobody has a 
clue how to do so with any sort of reliability, and I doubt that it is 
possible since you would surely need runtime information not available to 
a source-code static analyser.

We humans do it by focusing only on a small part of the program at once, 
and using heuristics to guess what the likely runtime information could 
be. The fact that we're not very good at it is provable by the number of 
bugs we let slip in.

So the bottom line is, any *practical* static type checker has to assume 
that a single variable is always the same type during its lifetime, and 
treat any assignment to another type as an error unless told differently.

(If you have counter-examples, I'm happy to learn better.)



By the way, you keep writing "interfere", the word is "infer":

infer
    v 1: reason by deduction; establish by deduction [syn: deduce,
         infer, deduct, derive]
    2: draw from specific cases for more general cases [syn:
       generalize, generalise, extrapolate, infer]
    3: conclude by reasoning; in logic [syn: deduce, infer]



> Unless you mean "A probable guess" by interfere.

No.


-- 
Steven D'Aprano
"Ever since I learned about confirmation bias, I've been seeing
it everywhere." -- Jon Ronson