Mypy – static type checking for Python 3 | Hacker News Reader

Mypy – static type checking for Python 3

github.com

70 pointsHerrMonnezza29 comments

Just a few days ago Guido proposed to adopt the Mypy syntax for type annotations in Python 3.5. There is a big discussion going on on the python-ideas mailing list about that and the general idea of having optional static typing in Python:

https://mail.python.org/pipermail/python-ideas/2014-August/0...

Recommended reading for those interested in the topic.

This is probably the best thing i've heard about python in the last 2 years. Guido's point are all 100% valid.

Python should take example on Typescript. It's light and smart. And that's enough to cover 99% of the cases.

Just let me specify that function foo's first parameter is an array of "stuff", and i'll be the happiest man. Leave the complicated cases for future versions.

Been using optional typing for almost a year now with Dart, and it's pretty awesome. Really hoping this comes to python!

I wrote a decorator-driven library to do optional type checking at runtime with no need for a special interpreter :)

https://github.com/kislyuk/ensure

(Having optional static type checks in the core interpreter would be nice, though Alex Gaynor's concerns linked in another comment are very valid.)

I think one of the strengths of Mypy's approach is the fact that it _doesn't_ do type checking at runtime. It may be inconvenient to have a separate step for type checking, but it also doesn't impart any runtime performance penalty.

Former HN discussion at: https://news.ycombinator.com/item?id=4561973

Although it seems that MyPy has done a lot of progress since, most notably adopting Python 3 syntax for type annotations.

Has anyone used this with Django? If it works well I might replace Ruby with Mypy.

Doing iOS (with Swift) for a while has made me dislike not having static typing.

It would be awesome to combine pypy and mypy. Pypy could probable use static typing to gain some speed.

Alex Gaynor, one of the PyPy developers said (on the mailing-list where Guido proposed this):

You're right. None of this would provide any value for PyPy.

https://mail.python.org/pipermail/python-ideas/2014-August/0...

I certainly didn't expect this, but he is right.

Why is that?

Because in a dynamically typed language like Python, it is perfectly feasible that the type declared in the code, and type-checked before the program runs, is different when the piece of code actually _runs_. Pypy uses runtime types to make decisions about optimizations, and since those may be different than the types declared at compile time, it will always have to inspect the runtime type anyway.

Then the type annotation is wrong, and it shouldn't be there. Type annotations only make sense if you know exactly what the types may be at runtime. I still don't see why correct annotations couldn't help PyPy.

Type-checking _via_ those annotations, are, like Guido said, basically a souped-up linter. With a dynamic language like Python, there is _never_ a guarantee that the types that type-checked during compilation are the types that will be observed during runtime. Type-checking Python code via function annotations is nothing like type checking a Haskell program, where you can be reasonably certain that a program that type-checks will run correctly.

Even if you write a program that you can provably show will never have any runtime types that differ from compile time types, Pypy can't assume that will be the case with every program that it tries to run. I don't have any specific knowledge of the optimizations that Pypy runs, but if one of the core contributors of Pypy says it can't be done, I'm inclined to believe him.

It is trivial to write a function that always returns a specific type, e.g., def f(): return 1

Therefore your claim that there is "_never_ a guarantee" is simply false. I was asking: what if you DO want PyPy to assume that your types are correct, why couldn't that help?

In Python you have no guarantee that that function hasn't been monkeypatched over and replaced by some other library you imported.

From what I read those things are problematic for PyPy anyway, causing it to fallback to an unoptimized interpreter. Also, the type annotations could be interpreted as a promise that what is being annotated will not be monkeypatched at runtime. What is a type annotation, if not a promise that something is not as dynamic as it could otherwise be?

Monkeypatching means that `def f(): return 1` could be turned into `def f(): return "i am now a string!"` at runtime, so I stand by my original statement.

EDIT: Here is a trivial example of a program that type checks at compile time but doesn't present the same types at runtime. Obviously you would never do this in production code, but the same effect could be accomplished simply by doing an `import somemodule`.

http://codepad.org/OarBYXfZ

Your replacing what 'f' is bound to; this would include replacing any type annotations, and triggering any system that relies on type annotations to drop/reset its optimizations for 'f'. You're not actually rewriting the original function to return something different; this would probably also be possible, but would be considered as even more of a dirty trick.

It is unfortunate that such dynamicity is the default in Python, when in reality it is rarely needed. So it would be advantageous to be able to tell the optimization system: this function is not going to change dynamically (on an opt-in basis).

You could replace the code object at runtime changing what the function does and what the type of the returned object is.

But wouldn't annotatin at least help pypy choose a better suited runtime type ?

We are out of my depth here, I have no experience or knowledge of the optimizations that Pypy does. So, I am trusting Alex Gaynor's word that it wouldn't help, since if anyone would be an expert on Pypy's optimizations, it would be him.

They wouldn't, because there is no runtime specification for enforcement of types based on type annotations. PyPy still can't assume anything about what type a value will be because a value `v` annotated as `str` could still be changed as follows:

v = 1234

Then, PyPy would crash or behave erratically since its assumptions about the value's type are false.

> a value `v` annotated as `str` could still be changed as follows:

> v = 1234

Surely at least this could be caught by a static type checker? If `v` is annotated to be of type `str`, assigning it a constant int should be a type error, though I'm sure Python provides more indirect ways of setting `v` that would be harder to catch statically (like globals()['v'] = ...).

But your comment raises an interesting question: are the annotations MyPy is relying on (static) type annotations, or value annotations?

I tend to think of the difference between static and dynamic typing as whether types attach to expressions or to values. If annotations only attach to the value to which a variable is initially bound in some context, I can see how they really wouldn't be much help in this scenario, since `v = 1234` is simply rebinding `v` to a value of a different type, and a previous annotation wouldn't preclude that. But if annotations attach to expressions, then it would be inconsistent to bind `v` to a value like 1234, since the constant "1234" is of a different type than `v` is.

"there is no runtime specification for enforcement of types based on type annotations"

Indeed, if you consider type annotation as just annotation and nothing else. But at least you "could" imagine an option to have pypy optimize based on them.

> Then the type annotation is wrong, and it shouldn't be there. Type annotations only make sense if you know exactly what the types may be at runtime.

In many (including many of the most popular) statically-typed (and not optionally so) -- particularly OO -- languages, the compile-time types in many declarations are type bounds, but not assured to be the exact runtime types. So I hardly see that it is problematic that this would be the case with optional type annotations in a dynamic language.

Yes, in Java and C# for example, compile-time type and runtime type of a variable can be different when you instantiate an object of a type that inherits from an abstract base class.

To put it crudely, you're thinking with a deity's mindset. PyPy has to accept that annotations can be wrong under this proposal. PyPy is trying to implement Python, and in Python, those annotations are strictly advisory.

PyPy can of course take that mindset, forking the language into some typed python dialect which, for well-typed programs, returns the same stuff as normal Python. Actually, you may be surprised to know that this language has already been completed (!) and a significant program has been written in it (!!). That significant program is called PyPy (wow so meta), and the language it's written in, which alters Python so that static type inference is possible, is called RPython.

But assuming that PyPy doesn't force everyone to write RPython, static type inference cannot be done easily in Python and static type annotations are strictly advisory. Given this, PyPy will keep doing its just-in-time thing. Then, we're compiling while the code is executing. But then what help is a type hint? It's run-time. We have the argument; we know what Python type it is supposed to be. The problems which PyPy has to solve are things like, "can I optimize this Python `int` into a single 64-bit word?" and those problems are not addressed at all by the type hint.

I understand static type annotations would be an extension to current Python semantics, it would require a flag such as "my type annotations are correct and please use them for optimizations" (this idea really only makes sense if PyPy can assume the annotations are not wrong, otherwise the arguments against this idea are just trivial). TypeScript is doing something similar for Javascript; it extends the language but is a strict superset. Type annotations can work together with JIT optimizations, because the annotations could simply provide a better starting point for JIT, requiring it to infer less, and perhaps providing information which would otherwise not be inferred from running the code. PyPy would still need to specialize further, e.g., from Int to int64 as you say, but already knowing that it's not float or str or list already seems useful.

Gradual typing is relevant in this regard, which makes it possible to combine static and dynamic types and do type inference. See e.g. https://github.com/tomprimozic/type-systems/tree/master/grad...

Now of course PyPy may hold the position that it's going to eschew static types on principle, but then it's a matter of ideology, not a technical reason, which causes these type annotations to "never have any value for PyPy".

Reply on news.ycombinator.com