static type checking for Polars
Catch Polars bugs before your code runs.
Astrolabe tells mypy, the Python type checker, how to track the contents of your Polars dataframes. A missing column or a wrong data type becomes a type error in your editor, not a runtime failure.
Python 3.12+ · mypy 1.13+ · Polars 1.43.2
Speed and type safety
Don’t compromise. Keep the speed and expressiveness of dataframes, with the correctness guarantees of statically typed code.
Guardrails and context
Types give people and coding agents up-to-date context and requirements, and the checker validates every refactor across all code paths.
Plain Polars, no overhead
You write ordinary Polars, and a typed frame is an ordinary DataFrame at run time. No new API, no cost to your pipeline.
how it works
Declare the schema at load time
Astrolabe reads the schema that you pass to Polars, so the frame has typed columns from the start.
- A plain
read_csvcall. Nothing here comes from Astrolabe. - The schema gives each column a data type. The checker reads it, so
tradesnow has known columns.
Typos are caught
A reference to a column that does not exist is a type error in your editor, not an exception at run time.
selectasks for a column namedprcie.tradeshasprice, notprcie, so mypy reports the line.
Every step updates the schema
Each operation produces a frame with its own schema, and every later use is checked against it.
selectkeeps two columns. The checker knows thatsymbolshas noquantity.- Later, a filter reads
quantityfromsymbols. The column is gone, and the error points at this line.
Data types are checked too
Each operation needs columns of the right data type, and a column of the wrong type is an error, like a missing one.
- A second file. Here,
symbolis anInt64code, not aString. filterkeeps the rows where a condition is true, so it needs aBooleancolumn.priceis aFloat64.- A join compares the keys on the two sides. A
Stringkey cannot match anInt64key.
New columns are typed
The checker works out the data type of each new column, as Polars does at run time.
- A
Float64times anInt64gives aFloat64.pricedhas a new column,notional. group_bykeeps the key and the aggregates. The sum stays aFloat64, andpl.len()counts rows as aUInt32.
Write generic functions
Astrolabe's rich grammar of generics lets you work with partially known schemas. Annotate a parameter with only the columns that the function reads, and let Rest stand for any others.
- A
Columnsclass names columns and their data types, like a dataclass. Reststands for all the other columns, the ones that the function does not name.- The function takes any frame with
priceandquantity. Because ofRest, the frame can have other columns too. quoteshassymbolandprice, but noquantity.- The call gives the function a frame without a column that it needs. The error is at the call, not inside the function.
Let inference track the rest
The schema of each frame becomes part of the function's signature. Declare the columns that the function adds, and inference works out what the body does to the others. Each caller gets its own columns back.
WithNotionaltakes the columns ofPricedand addsnotional.- The function promises the columns of
WithNotional.InferredRemainderstands for the other columns: the checker reads them from the body. infer(...)marks the returned value. The checker makes sure that it holdsWithNotional.tradesbringssymbolas an other column.resultkeeps it, next to the newnotional.resultnow has anotionalcolumn of typeFloat64, so later code can use it like any other column.
what the checker knows about trades
Step 1 of 7
Want to go further?
Learn the full Astrolabe type grammar and the Polars operations it supports.
features
Formally defined and proven
The type grammar is a consistent system with a written specification. Its core theorems are proved in Lean, and its data-type rules are tested against Polars.
Broad Polars coverage
Data frames, lazy frames, expressions and selectors, through select, join,group_by, unpivot and more, each with the schema that Polars gives.
Checks at run time, too
For data that comes from outside, check_schema verifies a frame against its declared type at run time, andforce_schema casts it to that type.
Set up in one command
astrolabe init adds the plugin to your mypy configuration in one step. It then runs wherever mypy runs: your editor, pre-commit hooks and CI.
Honest and pragmatic
Not every schema is known before the code runs, and that’s fine. The checker marks such a frame or column as unknown, and every other check still applies.
Choose your strictness
One setting decides how strict the checker is with steps it cannot fully verify: lenient for an existing codebase, strict for new code, adjustable per operation.
how Astrolabe compares
Validation libraries check data at run time, only where the code calls a check, and only on the paths that run. Astrolabe analyzes every code path and every step, without running your code.
| Astrolabe | pandera | patito | dataframely | |
|---|---|---|---|---|
| When mypy runs | ||||
| Every column referenceA column that the frame does not have is an error wherever the code reads it: in select, pl.col, joins and group keys. | ✓ | – | – | – |
| Schema tracked through every transformEach operation updates the schema, so the code is checked at every step, not only where a frame enters a function. | ✓ | – | – | – |
| Data types in operationsA filter needs a Boolean, join keys must have the same type, and arithmetic must fit the column types. | ✓ | – | – | – |
| Function arguments checked by their columnsA call passes when the frame has the columns that the parameter declares, wherever the frame comes from. | ✓ | ◐checks the schema label, not the columns | – | ◐checks the schema label, not the columns |
| Functions that accept extra columnsA function names only the columns it reads. The caller’s other columns pass through to the result, still typed. | ✓ | – | – | – |
| When the code runs | ||||
| No required overheadType safety adds nothing to the pipeline at run time: no validation pass and no wrapper around Polars. | ✓ | – | – | – |
| Columns and data typesCheck a frame from outside against its declared type. | ✓check_schema | ✓ | ✓ | ✓ |
| Cast a frame to its schemaConvert each column to its declared data type. | ✓force_schema | ✓ | ✓ | ✓ |
| ValuesNulls, ranges, uniqueness and custom rules on the data. | – | ✓ | ✓ | ✓ |
Checked with mypy 2.4 against pandera 0.35, patito 0.8 and dataframely 3.1.
Install
Requires Python 3.12 or later.