How the checker works

Astrolabe is a plugin for mypy. mypy reads the program, keeps the types, and reports the errors. The plugin computes the types that mypy cannot compute alone: the schema of each frame, and the data type of each column.

The type of an expression holds its code

An expression such as pl.col("price") * 2 has no meaning alone: its data type depends on the frame where it runs. So the plugin gives the expression a type that holds its code.

When the expression meets a frame, for example in select or with_columns, the plugin computes the column that it gives, at the data types of that frame. The same expression gives a Float64 over a Float64 column, and an Int64 over an Int64 column.

The rules come from Polars

The plugin computes each data type with the typing rules of Polars. The rules are translated from the source of Polars, and tested against Polars itself: a test runs each rule and the real call over many data types, and compares the answers. A behavior of Polars that no statement captures is listed in Polars behaviors.

The rules match one release of Polars, 1.43.2. Another release can type some calls differently.

Calls are generic

A function over an open frame is generic in its remainder. At each call, mypy substitutes the arguments of the caller in the signature, as it does for a type variable. The plugin computes the effect of each marker on the columns of the caller. So a function written once gives the exact result for each caller.

The rules are written down

The type system has a written specification. It states what each type means and the rule of each operation. Its core theorems are proved in Lean 4, and each measured claim names the test that measures it. See the specification.