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 binds attribute references in the AST and generates a map from AST expressions to types (the type_map attribute).

Type inference

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).

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'.

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 (but int, float and other built-in types are not special; Python has no equivalent to the primitive types in 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

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(AB):
    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.

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).