7. Make the checker stricter

Some results have no proof. The checker knows the name of a column but not its data type, or it cannot know the columns of a frame at all. One setting decides which of these results are errors.

A result without a proof

map_elements runs a Python function on each value. The checker cannot read the function, so it cannot know the data type of the result:

pipeline.pymypy: no errors

1class Trades(Columns):

2 symbol: pl.String

3 price: pl.Float64

4 quantity: pl.Int64

5

6

7trades: TypedDataFrame[Trades]

8rounded = trades.with_columns(pl.col("price").map_elements(round))

Resultroundeddeclared

symbolStringpriceUncheckedquantityInt64

Revealed type

TypedDataFrame[TypedDict({'symbol': String, 'price': Unchecked, 'quantity': Int64}, closed=True), None]

The column price keeps its name, with the data type Unchecked. Every other check still applies: the other columns keep their data types, and a later step that reads price passes.

Make it an error

The setting allow_unproven sets a level. A stricter level reports more of these results. At the level stated, the same line is an error:

pyproject.toml

[tool.astrolabe]
allow_unproven = "stated"

pipeline.pymypy: 1 error

1class Trades(Columns):

2 symbol: pl.String

3 price: pl.Float64

4 quantity: pl.Int64

5

6

7trades: TypedDataFrame[Trades]

8rounded = trades.with_columns(pl.col("price").map_elements(round))

↑error: Column "price" of "map_elements" is Unchecked: a Python function decides the type, and no return_dtype= names it [implicitly-unchecked]

↑note: set allow_unproven = "omitted" in [tool.astrolabe] to allow this, or set [tool.astrolabe.allow_unproven_overrides] map_elements = "omitted"

The note names two ways to let the line pass: a less strict level, or an override for one operation.

Give the checker the proof

Here, the better fix is to state the data type. return_dtype= names it, and the column is typed again:

pipeline.pymypy: no errors

1class Trades(Columns):

2 symbol: pl.String

3 price: pl.Float64

4 quantity: pl.Int64

5

6

7trades: TypedDataFrame[Trades]

8rounded = trades.with_columns(pl.col("price").map_elements(round, return_dtype=pl.Int64))

Resultroundeddeclared

symbolStringpriceInt64quantityInt64

Revealed type

TypedDataFrame[TypedDict({'symbol': String, 'price': Int64, 'quantity': Int64}, closed=True), None]

The default level is omitted. A new project can start at a stricter level, and an existing codebase can start at the default. See Configuration for each level, and Adopting in an existing codebase.

This is the end of the tutorial. The Guides explain each topic in more detail.