Type Checker

The mypy type checker checks if a program has type errors and infers the types of variables and expressions. It is implemented as an AST visitor.

The checker.TypeChecker class (in mypy/checker.py) takes as an input a semantically analyzed file AST (instance of nodes.MypyFile). It generates a dict from AST expression nodes to types (the type_map attribute). It also binds attribute references in the AST to the target attribute/method. This can only be done in type checking, since we need the inferred static type of receiver objects to find the target attribute.

Basic inference of types

Each subexpression AST node is assigned an inferred type. For example, for expression

  foo(bar, x.y) 

the type checker will infer types for 4 subexpressions: foo, bar, x, x.y and foo(bar, x.y). It type check arguments types against the type of foo (which is likely a CallableType), and the type of entire expression is derived from the return type of the type of foo.

Attribute expressions with Any receiver types are special, and cannot be bound during type checking. Instead, the type of expression x.y is just Any if the type of x is Any.

Type inference of generic types

TODO: describe type inference of generic types

Type checking with Any types

Type compatibility in mypy is different from languages such as Java. The Any type is compatible with every other type, and vice versa. This is in addition to normal nominal subtyping, which is similar to Java.

Examples:

• int is compatible with Any
• list[int] is compatible with list[Any]
• list[int] is compatible with Sequence[Any] (subtyping + Any types)

TODO describe type operations

More about type compatibility

int, float and other built-in types are (mostly) not special. Python has no equivalent to the primitive types in Java. However, as a special case, int is treated as compatible with float even though there is no subclass relationship (this is for convenience only).

Mypy also support structural subtyping through protocols.

Join and Meet

Inside the type checker, two important operation are performed on the types: join and meet.

Intuitively, given two types X and Y, one can think of join(X, Y) as a type that we don't know whether it is X or Y, and meet(X, Y) is a type that we know to be compatible with both X and Y. However, join and meet only approximate this notion.

The hierarchy of classes and types in Python is generally built along a lattice. Consider the following classes:

class A:
    def foo(self): pass
class B:
    def bar(self): pass
class AB(A, B):
    pass

This hierarchy can be depicted as follows (where X -> Y mean "X is a subtype of Y", often written X <: Y):

object <- A
  ^       ^
  |       |
  B  <-  AB 

Most of mypy's type system can be put into such diagrams.

Given such a structure, join(X, Y) mean "take the closest common ancestor of X and Y". meet(X, Y) mean "take the closest common descendant of X and Y". So in the above example, join(A, B) will be object. meet(A, B) is somewhat more problematic, since we don't know at every point what are all the possible classes that inherit from both A and B. Instead, we can look at a similar example, involving Union:

Union[A, B, C] <- Union[B, C]  <- C
  ^                ^
  |                |
Union[A, B]   <-   B 
  ^
  |
  A

This diagram shows that meet(Union[A, B], Union[B, C]) is simply B. (In this diagram, join(A, B) will be Union[A, B]. This is the most precise join possible, but mypy does not take this approach, since it will make type checking much slower (or even non-terminating), and will force mypy to emit long and incomprehensible error messages; Unions usually do not have direct counterpart in the source code).

The join operation is applied, for example. In list literals:

x = [A(), B()]

An element in the list x is either A or B. If there is no other common base class, it must be object (we could infer Union[A, B], but for largely historical reasons mypy doesn't do this).

The meet operation is usually related to flow of control:

def foo(x: Union[A, B, AB]):
    if isinstance(x, B):
       # here x is meet(Union[A, B, AB], B) which is Union[B, AB]
       ...

Inside mypy there's a type named UninhabitedType which is the meet of all other types combined (this type is sometimes called Bottom, Bot or Nothing in the literature). For this type, given some other type T, it holds that join(Bot, T) = T, and meet(Bot, T) = Bot.

Meet and join are commutative operations: meet(A, B) = meet(B, A) and join(A, B) = join(B, A).