Pytype’s Type System

Pytype’s Type System

Why do pytype’s semantics differ from mypy’s?

This FAQ refers to “pytype” rather than “python” because typing semantics in the python world are a property of the type checker rather than of the language. There are several python type checkers, and while they do aim for consistency with the relevant PEPs, they do not behave identically. For more information, check out:

A PyCon lightning talk comparing pytype and mypy, another popular type checker. The slides are here.
A more detailed written discussion in a Lobste.rs post.
A paper detailing pytype and mypy’s differing views of python’s type system.

As the primary open source type checker, mypy tends to de facto define the semantics of what people think of as “python typing” in areas not formally covered by a PEP. Pytype does try to be consistent with mypy, and with other type checkers like pyre and pyright; not counting bugs the primary source of differences is the desire to not break existing, unannotated code that follows valid python idioms.

Why does pytype allow adding multiple types to a container?

One somewhat surprising behaviour is illustrated by the following snippet:

xs = [1, 2, 3]
reveal_type(xs)  # => List[int]
xs.append('hello')  # no error!
reveal_type(xs)  # => List[int | str]

Given that xs is correctly inferred as List[int] in line 2, it could be expected that adding a string to it would be a type error. However, this is perfectly valid python code, and in this case pytype chooses to be descriptive rather than prescriptive, modifying the type of xs to match the actual contents.

Explicitly annotating xs with a type will indeed raise a container-type-mismatch error:

xs: List[int] = [1, 2, 3]
xs.append('hello')  # ! container-type-mismatch

Why is Optional[Optional[T]] the same as Optional[T]?

Note: Starting in Python 3.10, the preferred way to write the above types is None | None | T and None | T, which makes the equivalence between the two types almost obvious by inspection.

Consider the following code:

x: Dict[str, Optional[str]] = {'a': 'hello', 'b': None}
a = x.get('a')
b = x.get('b')
c = x.get('c')

Since the signature of dict.get is

class Mapping(Generic[K, V]):
  def get(key: K) -> Optional[V]

an ML-based language would indeed have a return type of Optional[Optional[str]], and be able to distinguish a value of None from a missing value. This comes down to the fact that python has union rather than sum types; Optional[T] is an alias for Union[T, None], and therefore, by a series of expansions,

Optional[Optional[T]]
= Union[Union[T, None], None]
= Union[T, None, None]
= Union[T, None]
= Optional[T]

Note that this is simply a difference of behaviour, not a flaw in either python or pytype; in particular Optional being a sum type would mean Optional[T] was an alias for None | Some[T] rather than None | T, which would mean every dictionary key access would need to be unwrapped before being used.

Why is pytype not more like $other_language?

We often get questions about why pytype’s typing semantics differ from C++/Java/ML/Haskell/etc. – common issues include containers being heterogeneous, and Unions being untagged (“union types” as opposed to “sum types”). The primary reason is that all those languages are statically typed; python is dynamically typed, and type checkers like pytype add gradual typing on top of that. While gradual typing may resemble static typing, it has a very different foundation and emphasis, which is to augment a dynamic language with optional types.

When discussing pytype’s design and limitations, it is important to distinguish type-theoretical properties like soundness and completeness (this is a good overview) from the expectation of static typing behaviour in a gradually typed language. It is more useful to compare pytype to other gradually typed languages like TypeScript (adding gradual types to JavaScript), Typed Racket (adding gradual types to Racket) and Stanza (designed with a gradual type system), and look at python typing in the light of some of the decisions those other languages made.

Note that gradual typing is not a poor approximation to static typing, it simply makes a different set of tradeoffs between type safety, expressiveness, ergonomics and performance. And within the realm of gradual typing (an active area of research) different languages select different tradeoffs; for instance typed racket does emphasise soundness, but requires more explicit boundaries between typed and untyped code, and run-time contracts to enforce some invariants.

Stanza’s author explains the rationale behind union types, for instance:

We have found union types to be an absolute necessity for being able to add types to untyped code without necessitating a structural change.

As an interesting aside, proper support for untagged union types also allows Stanza to omit the concept of a null value. A common idiom that is used to indicate that a variable may be “uninitialized” is to assign it the value false. Thus a variable holding a possibly uninitialized integer could be declared with type

var x: Int|False = false

indicating that x might have the value false, and any usages of x as an Int must first be checked. This elegantly sidesteps what Hoare called his “billion-dollar mistake”, and Stanza has no analogue to Java’s notorious NullPointerException.

and the TypeScript documentation has an explicit note on soundness:

TypeScript’s type system allows certain operations that can’t be known at compile-time to be safe. When a type system has this property, it is said to not be “sound”. The places where TypeScript allows unsound behavior were carefully considered, and throughout this document we’ll explain where these happen and the motivating scenarios behind them.

Some other interesting writing on the topic: