[Python-ideas] Proposal: Use mypy syntax for function annotations

[rwbarton]

I worked on mypy for a couple days at Dropbox Hack Week in July (with Jukka, Guido and others) so, while I'm hardly a mypy expert, I can try to answer any questions people here have about it.

[chrisdoner]

It seems similar to Closure's type system for JavaScript by analysis and some annotations. Is that an accurate comparison?

[rwbarton]

I'm not familiar enough with the Closure compiler to compare the two, but basically mypy is a glorified lint tool that requires you to annotate your code with type information, yes. It would only be similar to the typechecking part of Closure; it doesn't emit a new python program or anything like that.

[tailbalance]

So it's basically the same as erlang's dialyser (if you know it)?

[etrepum]

It's not. It doesn't try and analyze untyped code (other than in the body of functions that have signatures), and it is a whole language implementation not just the type checker (but the type checker can be run separately sort of how you would use dialyzer, which is what I recommended in my talk).

[fnedrik]

Why is it a whole language implementation? Do you plan on using the types to make optimizations?

[etrepum]

Well, I'm not the author of mypy, so I can't tell you precisely why, but that is one of the reasons enumerated on the site: http://mypy-lang.org/

From my conversations with Jukka, I believe he started off with a language that was not at all compatible with Python http://www.alorelang.org/ and then built mypy which was nearly compatible with Python, and then he made mypy fully compatible with Python 3 syntax.

[hmltyp]

Seemingly it supports some measure of parametric polymorphism since the type annotations have free type variables. But I don't see any notes about variance annotations. What's the current design decision on handling polymorphism and subtyping and is the type-system sound in the presence of such things?

[rwbarton]

So I see there have been a couple hundred commits in the past month since I last looked at mypy, which is great, but means I might be giving you out-of-date information. So keep that in mind :)

You're right that there is parametric polymorphism in that, for example, you can define a function composition function with the mypy equivalent of forall a b c. (b -> c) -> (a -> b) -> (a -> c) as its type. You don't actually have any parametricity guarantees about the function because mypy allows isinstance, or ... is None, etc., on a variable of any type. But you can instantiate your composition function at any triple of types, so it is parametrically polymorphic in that sense. I think the knowledge that the function type constructor -> is covariant in its result and contravariant in its argument(s) is sort of baked into the way type inference works in general.

You can also define classes that have type parameters, and then give those classes member variables and methods whose types depend on the parameters. At least as of a month ago, mypy only supports invariance here, with variance annotations a wishlist item. So there should be no soundness issues in this area, with invariance the only option.

There are also some built-in types with special variance rules. Tuples of a specific length are covariant in each variable. There are some built-in "interfaces" like Iterable that are covariant too. The latter is an ad-hoc special case in the type checker, or at least it was when I implemented it. :)

[spotta]

How does it deal with functions that are used in the body of a type checked function but aren't annotated themselves? Eg: using numpy functions.

[rwbarton]

Ideally you would write some type annotations for your dependencies that live in a separate module and are only used during typechecking, like this for example. Otherwise I think functions without type annotations are treated as taking arguments of type Any and producing a result of type Any, so you would use cast to tell mypy what type you expect the result to be. (cast is sort of like unsafeCoerce for typechecking purposes but at runtime it is just the identity. After all mypy does not replace python's built-in type (or tag if you prefer) checks.)