Contents
Appendix B

An Effect Checker

Effect Tracking lists five problems a checker for Annotated rows must solve, and concludes that solving them all means rebuilding a type checker. This appendix builds the part that needs no type inference. The checker here reads source text, resolves the calls it can, infers a row for every function, and reports each declared row the body exceeds. It is about 450 lines, and most of its pieces come from earlier chapters: a match over syntax-tree nodes, records for the data, a Result for the one operation that can fail, and a pure core with its Effects at the edge. The final listing runs the checker on its own source to confirm that last point.

The Restriction

The checker resolves a call by its name and by the written type of its receiver. A call it cannot resolve contributes an Effect named Unknown to the caller’s row. The checker treats no unresolved call as pure. With that rule the tool stays small, and every call it fails to resolve shows in a row. A row that reads Unknown says the checker could not resolve a call, and where. What the Checker Resolves, and What It Cannot See lists the constructs the rule does not cover.

Name resolution covers more calls than you might expect. Of the roughly 6,600 calls in this book’s chapter listings, nearly four in five resolve by name alone: a built-in, an imported name, or a function or class defined in the same file. The largest remaining group is a method called on a local variable with no annotation, and From a Call to a Name recovers part of that group.

The checker follows Koka’s policy. A function with no written row gets an inferred one. The checker compares a written row with the function’s body, and the function’s callers trust the declaration. performs() with no arguments declares that a function is pure.

Effect Names and the Table

An Effect is a class with no body, as Ask and Tell are in Appendix A. These eight cover the standard library:

# effect_names.py
class Console: ...
class FileSystem: ...
class Network: ...
class Clock: ...
class Random: ...
class Environment: ...
class Process: ...
class Unknown: ...

One question decides whether something deserves a name: does a test replace it? A test replaces the clock, the network, and the file system. No test replaces len(). A finer vocabulary makes the rows unreadable and the table in effect_table.py unmaintainable.

Appendix A lists three answers to the question of what untracked code performs. This checker takes the third, a separate declaration, because the first two, pure and Unknown, are wrong for print(). print() writes to the console, and calling it Unknown puts Unknown in nearly every row. The declaration cannot go on the function. A built-in has no __annotations__ and no __dict__ in which to store one, so print.__annotations__ = {} raises an AttributeError. The declarations therefore live in a table:

# effect_table.py
from fnmatch import fnmatchcase
from typing import Final
from effect_names import (Clock, Console, Environment,
                          FileSystem, Network, Process,
                          Random, Unknown)

type Row = frozenset[str]
type Table = dict[str, Row]

def names(*effects: type) -> Row:
    return frozenset(e.__name__ for e in effects)

PURE: Final[Row] = names()
UNKNOWN: Final[Row] = names(Unknown)
STDLIB: Final[Table] = {
    "builtins.print": names(Console),
    "builtins.input": names(Console),
    "builtins.open": names(FileSystem),
    "builtins.eval": UNKNOWN,
    "builtins.exec": UNKNOWN,
    "builtins.*": PURE,
    "pathlib.Path": PURE,
    "pathlib.Path.with_*": PURE,
    "pathlib.Path.*": names(FileSystem),
    "time.time": names(Clock),
    "time.sleep": names(Clock),
    "time.perf_counter": names(Clock),
    "datetime.datetime.now": names(Clock),
    "random.*": names(Random),
    "os.environ.*": names(Environment),
    "os.getenv": names(Environment),
    "os.path.join": PURE,
    "os.*": names(FileSystem),
    "socket.*": names(Network),
    "urllib.request.*": names(Network),
    "subprocess.*": names(Process),
    "ast.*": PURE,
    "fnmatch.*": PURE,
    "itertools.*": PURE,
    "functools.*": PURE,
    "math.*": PURE,
    "typing.*": PURE,
}

def lookup(name: str, table: Table) -> Row:
    for pattern, row in table.items():
        if fnmatchcase(name, pattern):
            return row
    return UNKNOWN

A key is an fnmatch pattern, the wildcard notation of a shell, in which * matches any run of characters, dots included. lookup() returns the row of the first pattern that matches. Because a dictionary keeps insertion order, a specific name goes above the glob that would otherwise match it. "os.path.join" is pure, and the "os.*" below it is FileSystem. Whole modules take one line each, which keeps the table short. A name that matches nothing is UNKNOWN. Because the table lists pure modules explicitly, leaving a module out can add an Unknown and cannot hide an Effect.

The key is the name as a programmer imports it, because a function’s own attributes report its name unreliably. os.remove.__module__ is nt on Windows and posix elsewhere, open.__module__ is _io, and random.random reports None for its module and Random.random for its qualified name. The checker reads source, and in source the name is os.remove.

Because names() builds a row from classes, a misspelled Effect in the table is an error the type checker reports. A Row is a frozenset[str] because the checker does not import the code it reads. In source text, performs(Ask) is the name Ask.

# test_effect_table.py
import pytest
from effect_table import STDLIB, UNKNOWN, lookup, names

@pytest.mark.parametrize(
    "name, expected",
    [
        ("builtins.print", {"Console"}),
        ("builtins.len", set()),
        ("pathlib.Path.read_text", {"FileSystem"}),
        ("pathlib.Path.with_suffix", set()),
        ("time.time", {"Clock"}),
        ("os.path.join", set()),
        ("os.remove", {"FileSystem"}),
        ("requests.get", {"Unknown"}),
    ],
)
def test_first_matching_pattern_wins(
    name: str, expected: set[str]
) -> None:
    assert lookup(name, STDLIB) == expected

def test_unlisted_name_is_unknown_not_pure() -> None:
    assert lookup("anything.at_all", {}) == UNKNOWN

def test_names_reads_class_names() -> None:
    class Ask: ...
    assert names(Ask) == {"Ask"}

From a Call to a Name

Every call in a syntax tree has a func expression, and this listing turns that expression into a dotted name the table can match:

# call_names.py
import ast
import builtins
from typing import Final
from record import record

UNRESOLVED: Final[str] = "?"
LITERALS: Final[dict[type[ast.expr], str]] = {
    ast.List: "builtins.list",
    ast.ListComp: "builtins.list",
    ast.Dict: "builtins.dict",
    ast.DictComp: "builtins.dict",
    ast.Set: "builtins.set",
    ast.SetComp: "builtins.set",
    ast.Tuple: "builtins.tuple",
    ast.JoinedStr: "builtins.str",
}

def top_of(name: str) -> str:
    return name.split(".")[0]

def imports_of(tree: ast.Module) -> dict[str, str]:
    found: dict[str, str] = {}
    for node in ast.walk(tree):
        match node:
            case ast.Import(names=aliases):
                for a in aliases:
                    top = top_of(a.name)
                    full = a.name if a.asname else top
                    found[a.asname or top] = full
            case ast.ImportFrom(
                module=str(module), names=aliases
            ):
                for a in aliases:
                    full = f"{module}.{a.name}"
                    found[a.asname or a.name] = full
    return found

def dotted(node: ast.expr) -> list[str]:
    match node:
        case ast.Name(id=name):
            return [name]
        case ast.Attribute(value=value, attr=attr):
            head = dotted(value)
            return [*head, attr] if head else []
        case _:
            return []

@record
class Scope:
    module: str
    names: dict[str, str]
    defined: frozenset[str]
    types: dict[str, str]

    def name(self, name: str) -> str:
        if name in self.types:
            return UNRESOLVED
        if name in self.names:
            return self.names[name]
        if name in self.defined:
            return f"{self.module}.{name}"
        if hasattr(builtins, name):
            return f"builtins.{name}"
        return UNRESOLVED

    def annotation(self, node: ast.expr) -> str:
        match node:
            case ast.Subscript(value=value, slice=inner):
                outer = self.annotation(value)
                if outer == "typing.Final":
                    return self.annotation(inner)
                return outer
        match dotted(node):
            case [head, *rest]:
                return ".".join([self.name(head), *rest])
            case _:
                return UNRESOLVED

    def type_of(self, node: ast.expr) -> str:
        match node:
            case ast.Constant(value=str()):
                return "builtins.str"
            case ast.Name(id=name) if name in self.types:
                return self.types[name]
            case ast.Name(id=name):
                return self.name(name)
            case ast.Call(func=func):
                return self.callee(func)
            case _:
                return LITERALS.get(type(node), UNRESOLVED)

    def callee(self, func: ast.expr) -> str:
        match func:
            case ast.Name(id=name):
                return self.name(name)
            case ast.Attribute(value=value, attr=attr):
                if top_of(ast.unparse(func)) in self.names:
                    return self.annotation(func)
                receiver = self.type_of(value)
                if receiver == UNRESOLVED:
                    return UNRESOLVED
                return f"{receiver}.{attr}"
            case _:
                return UNRESOLVED

imports_of() and dotted() are class patterns over ast nodes. Composite and Interpreter notes that the standard library walks these trees with ast.NodeVisitor, in the style of Visitor. The node types are a closed set, so match does the same work with no class to subclass. dotted() is the smallest example. It is recursive, as the tree is. os.path.join is an Attribute whose value is an Attribute whose value is a Name.

A Scope holds the names the checker has collected at one point in a file. names maps a local name to its full one, so rm becomes os.remove. defined holds the functions and classes the module defines. types maps a variable to the name of its type. name() searches from the innermost scope outward, as Python does: variables, then the module’s imports and definitions, then builtins. A name found in types is a variable, and calling a variable calls whatever value it holds at runtime. The source does not name that value, so name() answers UNRESOLVED.

callee() handles the two shapes a resolvable call takes. A bare name goes to name(). An attribute is either a path through an import, such as time.sleep, or a method on a receiver. type_of() finds the receiver’s type where the source makes it evident: a string constant, one of the literals in LITERALS, a variable whose type the scope records, or a call, which takes its callee’s name as its type. p = Path(name) therefore gives p the type pathlib.Path, and p.read_text() becomes pathlib.Path.read_text, which a pattern in the table matches.

annotation() reads a written type. It drops the subscript from list[str] and looks through Final[...] to the type inside.

# test_call_names.py
import ast
import pytest
from call_names import UNRESOLVED, Scope, imports_of

def test_imports_map_local_names_to_full_names() -> None:
    tree = ast.parse(
        "import os\n"
        "import os.path as p\n"
        "from os import remove as rm\n"
    )
    assert imports_of(tree) == {
        "os": "os",
        "p": "os.path",
        "rm": "os.remove",
    }

def callee(call: str, types: dict[str, str]) -> str:
    names = {"rm": "os.remove", "time": "time"}
    scope = Scope("m", names, frozenset({"local"}), types)
    node = ast.parse(call, mode="eval").body
    assert isinstance(node, ast.Call)
    return scope.callee(node.func)

@pytest.mark.parametrize(
    "call, expected",
    [
        ("rm(x)", "os.remove"),
        ("time.sleep(1)", "time.sleep"),
        ("local()", "m.local"),
        ("print(x)", "builtins.print"),
        ("', '.join(xs)", "builtins.str.join"),
        ("[].append(1)", "builtins.list.append"),
        ("dict.fromkeys(xs)", "builtins.dict.fromkeys"),
        ("p.read_text()", "pathlib.Path.read_text"),
        ("action(x)", UNRESOLVED),
        ("q.anything()", UNRESOLVED),
        ("f()()", UNRESOLVED),
    ],
)
def test_callee(call: str, expected: str) -> None:
    types = {"p": "pathlib.Path", "action": UNRESOLVED}
    assert callee(call, types) == expected

The last three cases are the limits. action(x) calls a parameter, q.anything() has a receiver of no known type, and f()() calls the result of a call. Each comes back UNRESOLVED.

Facts About a Function

The checker needs three facts about a function: the row it declares, the Effects it hides, and the names it calls.

Hiding needs a marker, and ask() in Appendix A shows why. ask() declares Ask and calls input(), which performs Console. Both descriptions are accurate, and The Check shows the checker reporting each. A second piece of metadata names the Effects that stop at this function:

# effect_marks.py
from record import record

@record
class Hides:
    effects: frozenset[type]

def hides(*effects: type) -> Hides:
    return Hides(frozenset(effects))

Annotated[str, performs(Ask), hides(Console)] states that ask() is the boundary where Console becomes Ask. The checker removes Console from the body’s row and checks nothing about the claim, as the type checker trusts a cast(). hides() is the third line of Appendix A’s rule, “the Effects f handles,” in the weakest form you can write without handlers. The annotation also puts two pieces of metadata in one Annotated, the arrangement PEP 593 exists to allow. row() from Appendix A skips the Hides object it does not recognize.

# function_facts.py
import ast
from typing import TypeIs
from call_names import UNRESOLVED, Scope, imports_of
from effect_table import PURE, Row
from record import record
from result import Err, Ok, Result

type Def = ast.FunctionDef | ast.AsyncFunctionDef

@record
class Facts:
    name: str
    declared: Row | None
    hidden: Row
    calls: tuple[str, ...]

def marked(func: Def, marker: str) -> Row | None:
    match func.returns:
        case ast.Subscript(
            value=ast.Name(id="Annotated"),
            slice=ast.Tuple(elts=[_, *extras]),
        ):
            for extra in extras:
                match extra:
                    case ast.Call(
                        func=ast.Name(id=found), args=args
                    ) if found == marker:
                        return frozenset(
                            a.id
                            for a in args
                            if isinstance(a, ast.Name)
                        )
    return None

def assigned(
    body: list[ast.stmt], scope: Scope
) -> dict[str, str]:
    types: dict[str, str] = {}
    written: dict[str, str] = {}
    values: dict[ast.AST, str] = {}
    nodes = (n for stmt in body for n in ast.walk(stmt))
    for node in nodes:
        match node:
            case ast.AnnAssign(
                target=ast.Name(id=name), annotation=note
            ):
                written[name] = scope.annotation(note)
            case ast.Assign(targets=[target], value=value):
                values[target] = scope.type_of(value)
            case (
                ast.Name(id=name, ctx=ast.Store())
                | ast.MatchAs(name=str(name))
                | ast.MatchStar(name=str(name))
                | ast.ExceptHandler(name=str(name))
            ):
                found = values.get(node, UNRESOLVED)
                if types.setdefault(name, found) != found:
                    types[name] = UNRESOLVED
    return types | written

def parameters(
    func: Def, scope: Scope, owner: str
) -> dict[str, str]:
    args = func.args
    every = args.posonlyargs + args.args + args.kwonlyargs
    types = {
        arg.arg: scope.annotation(arg.annotation)
        if arg.annotation
        else UNRESOLVED
        for arg in every
    }
    if owner and args.args:
        types[args.args[0].arg] = owner
    return types

def calls_in(
    body: list[ast.stmt], scope: Scope
) -> tuple[str, ...]:
    return tuple(
        scope.callee(node.func)
        for stmt in body
        for node in ast.walk(stmt)
        if isinstance(node, ast.Call)
    )

def function_facts(
    func: Def, base: Scope, owner: str
) -> Facts:
    types = (
        base.types
        | parameters(func, base, owner)
        | assigned(func.body, base)
    )
    scope = Scope(
        base.module, base.names, base.defined, types
    )
    return Facts(
        f"{owner or base.module}.{func.name}",
        marked(func, "performs"),
        marked(func, "hides") or PURE,
        calls_in(func.body, scope),
    )

def is_function(node: ast.stmt) -> TypeIs[Def]:
    kinds = ast.FunctionDef | ast.AsyncFunctionDef
    return isinstance(node, kinds)

def is_def(
    node: ast.stmt,
) -> TypeIs[Def | ast.ClassDef]:
    if isinstance(node, ast.ClassDef):
        return True
    return is_function(node)

def module_scope(module: str, tree: ast.Module) -> Scope:
    defined = frozenset(
        node.name for node in tree.body if is_def(node)
    )
    bare = Scope(module, imports_of(tree), defined, {})
    aliases = {
        node.name.id: bare.annotation(node.value)
        for node in tree.body
        if isinstance(node, ast.TypeAlias)
    }
    named = Scope(module, bare.names | aliases, defined, {})
    top = [
        node
        for node in tree.body
        if not is_def(node)
        and not isinstance(node, ast.TypeAlias)
    ]
    types = assigned(top, named)
    return Scope(module, named.names, defined, types)

def class_facts(
    node: ast.ClassDef, base: Scope
) -> list[Facts]:
    owner = f"{base.module}.{node.name}"
    methods = [
        function_facts(m, base, owner)
        for m in node.body
        if is_function(m)
    ]
    init = f"{owner}.__init__"
    built = tuple(m.name for m in methods if m.name == init)
    return [*methods, Facts(owner, None, PURE, built)]

def facts_of(module: str, tree: ast.Module) -> list[Facts]:
    base = module_scope(module, tree)
    found: list[Facts] = []
    for node in tree.body:
        if is_function(node):
            found.append(function_facts(node, base, ""))
        elif isinstance(node, ast.ClassDef):
            found += class_facts(node, base)
    top = [node for node in tree.body if not is_def(node)]
    name = f"{module}.<module>"
    calls = calls_in(top, base)
    return [*found, Facts(name, None, PURE, calls)]

def read_module(
    module: str, source: str
) -> Result[list[Facts], str]:
    try:
        tree = ast.parse(source)
    except SyntaxError as e:
        return Err(f"{module}: line {e.lineno}: {e.msg}")
    return Ok(facts_of(module, tree))

marked() is one nested pattern. It matches a return annotation of the form Annotated[T, ...], binds everything after T to extras, and returns the argument names of the first call to marker. The guard, if found == marker, compares a captured name with a parameter, which a pattern alone cannot do. For a function with no such annotation, marked() returns None, which means “inferred.” An empty row means “pure,” so None and the empty row must differ. Row | None is an ordinary optional, with no assertion anywhere to unwrap it.

parameters() and assigned() fill a scope’s types: an annotated parameter, the first parameter of a method (the class), an annotated assignment, and a plain assignment whose right side has an evident type. assigned() also records every other name a body binds: a loop variable, a with or except target, a walrus target, a name inside a tuple target, and a name a pattern captures. Each alternative of the or-pattern binds name, as an or-pattern requires. Such a name gets UNRESOLVED, and so does a name that two assignments give different types. An annotation overrides UNRESOLVED in both cases. ast.walk() visits an assignment before its target, so values holds the type of the right side by the time the target’s Name arrives.

module_scope() does the same for a module’s top level. It reads each type statement separately, so a parameter annotated Table resolves to builtins.dict, and it keeps those statements out of assigned(), which would otherwise record an alias’s name as a variable. Because is_function() and is_def() return TypeIs, a comprehension filtered by one yields nodes whose narrowed type has a name.

calls_in() collects the third fact. ast.walk() yields a statement and every node beneath it, and callee() names each ast.Call among them. The walk descends into a nested function or a lambda, so the calls inside one count toward the function that contains it.

facts_of() records every top-level function, every method under module.Class.method, and each class under its own name. The class’s entry holds a call to its __init__() when the class defines one, so Log() performs what Log.__init__() performs. The module’s top-level statements become a function named module.<module>. It is the program’s edge and declares no row, so the checker has nothing to compare, and its inferred row says what running the file performs.

read_module() is the one operation here that can fail. It returns a Result, so a parse failure becomes a value the caller must inspect.

# test_function_facts.py
from textwrap import indent
from typing import Final
import pytest
from call_names import UNRESOLVED
from function_facts import Facts, read_module
from result import Err, Ok

SOURCE: Final[str] = '''
from pathlib import Path
from typing import Annotated, Final

type Names = list[str]
LIMIT: Final[dict[str, int]] = {}

class Log:
    def __init__(self) -> None:
        print("open")

    def write(self, text: str) -> None:
        self.flush()

    def flush(self) -> None: ...

def save(
    p: Path, names: Names
) -> Annotated[None, performs(FileSystem), hides(Console)]:
    log = Log()
    log.write(", ".join(names))
    names.sort()
    LIMIT.get("x")
    p.write_text("")
'''

def facts() -> dict[str, Facts]:
    match read_module("m", SOURCE):
        case Ok(found):
            return {f.name: f for f in found}
        case Err(problem):
            raise AssertionError(problem)

def test_every_def_and_the_module_get_facts() -> None:
    assert sorted(facts()) == [
        "m.<module>",
        "m.Log",
        "m.Log.__init__",
        "m.Log.flush",
        "m.Log.write",
        "m.save",
    ]

def test_a_class_calls_its_init() -> None:
    assert facts()["m.Log"].calls == ("m.Log.__init__",)

def test_self_resolves_to_the_class() -> None:
    assert facts()["m.Log.write"].calls == ("m.Log.flush",)

def test_receivers_resolve_five_ways() -> None:
    assert facts()["m.save"].calls == (
        "m.Log",
        "m.Log.write",
        "builtins.str.join",
        "builtins.list.sort",
        "builtins.dict.get",
        "pathlib.Path.write_text",
    )

def test_both_markers_are_read() -> None:
    save = facts()["m.save"]
    assert save.declared == {"FileSystem"}
    assert save.hidden == {"Console"}

@pytest.mark.parametrize(
    "binding",
    [
        "for str in xs: pass",
        "with open(xs) as str: pass",
        "if str := xs.pop(): pass",
        "str, n = xs",
        "match xs:\n  case [str]: pass",
        "match xs:\n  case [*str]: pass",
        "try: pass\nexcept OSError as str: pass",
        "str = 'text'\nstr = list(xs)",
    ],
)
def test_a_binding_shadows_the_builtin(
    binding: str,
) -> None:
    body = indent(f"{binding}\nstr.upper()", "    ")
    match read_module("m", f"def f(xs):\n{body}\n"):
        case Ok(found):
            assert found[0].calls[-1] == UNRESOLVED
        case Err(problem):
            raise AssertionError(problem)

def test_a_syntax_error_comes_back_as_a_value() -> None:
    result = read_module("bad", "def f(:\n")
    assert isinstance(result, Err)
    assert result.error.startswith("bad: line 1")

test_receivers_resolve_five_ways() shows the receiver rules together. In save(), log gets its type from a constructor call, the string by being a constant, names through a type alias, LIMIT through Final[...], and p by its annotation. test_a_binding_shadows_the_builtin() binds the name str in eight ways. Each time, str.upper() comes back UNRESOLVED instead of resolving to builtins.str.upper.

Rows to a Fixed Point

Appendix A’s rule is recursive. A function’s row needs its callees’ rows, which need theirs. Two functions that call each other make the recursion circular. The standard answer is to start every row empty and apply the rule until nothing changes. Rows that the rule leaves unchanged are a fixed point of the rule:

# infer_rows.py
from effect_table import Row, Table, lookup
from function_facts import Facts

type Rows = dict[str, Row]

def call_row(call: str, rows: Rows, table: Table) -> Row:
    if call in rows:
        return rows[call]
    return lookup(call, table)

def body_row(facts: Facts, rows: Rows, table: Table) -> Row:
    found = (call_row(c, rows, table) for c in facts.calls)
    return frozenset().union(*found)

def step(
    known: dict[str, Facts], rows: Rows, table: Table
) -> Rows:
    return {
        name: facts.declared
        if facts.declared is not None
        else body_row(facts, rows, table)
        for name, facts in known.items()
    }

def infer(known: dict[str, Facts], table: Table) -> Rows:
    rows: Rows = dict.fromkeys(known, frozenset())
    while (new := step(known, rows, table)) != rows:
        rows = new
    return rows

call_row() looks for a call among the functions the checker has read, then in the table. An unresolved call has the name "?", which matches no pattern, so lookup() answers UNKNOWN. step() is a pure function from one set of rows to the next. A declared row passes through unchanged, which is how callers come to trust it. An undeclared row becomes the union of what its calls perform. infer() is the loop. The walrus operator lets the while condition compute the next rows and compare them in one expression. Each step can add members to a row and cannot remove one, and the vocabulary is finite, so the loop ends.

# test_infer_rows.py
from effect_table import PURE, STDLIB
from function_facts import Facts
from infer_rows import infer

def known(*facts: Facts) -> dict[str, Facts]:
    return {f.name: f for f in facts}

def test_rows_propagate_up_the_call_chain() -> None:
    rows = infer(
        known(
            Facts("m.a", None, PURE, ("m.b",)),
            Facts("m.b", None, PURE, ("m.c",)),
            Facts("m.c", None, PURE, ("builtins.print",)),
        ),
        STDLIB,
    )
    assert rows["m.a"] == {"Console"}

def test_mutual_recursion_reaches_a_fixed_point() -> None:
    calls = ("m.even", "time.time")
    rows = infer(
        known(
            Facts("m.even", None, PURE, ("m.odd",)),
            Facts("m.odd", None, PURE, calls),
        ),
        STDLIB,
    )
    assert rows["m.even"] == rows["m.odd"] == {"Clock"}

def test_a_declared_row_is_trusted_by_callers() -> None:
    declared = frozenset({"Ask"})
    calls = ("builtins.input",)
    rows = infer(
        known(
            Facts("m.ask", declared, PURE, calls),
            Facts("m.greet", None, PURE, ("m.ask",)),
        ),
        STDLIB,
    )
    assert rows["m.greet"] == {"Ask"}

Nothing in infer_rows.py reads source text, so each test builds its Facts by hand instead of writing and parsing a program.

The Check

A finding is an Effect that a function’s body performs, that the function does not hide, and that its declared row omits:

# row_check.py
from effect_table import STDLIB, Table
from function_facts import Facts, read_module
from infer_rows import Rows, body_row, infer
from record import record
from result import Err, Ok

@record
class Finding:
    where: str
    problem: str

@record
class Report:
    rows: Rows
    findings: list[Finding]

def undeclared(
    facts: Facts, rows: Rows, table: Table
) -> list[Finding]:
    if facts.declared is None:
        return []
    body = body_row(facts, rows, table) - facts.hidden
    return [
        Finding(facts.name, f"undeclared {effect}")
        for effect in sorted(body - facts.declared)
    ]

def check(
    sources: dict[str, str], table: Table = STDLIB
) -> Report:
    known: dict[str, Facts] = {}
    findings: list[Finding] = []
    for module, source in sources.items():
        match read_module(module, source):
            case Ok(found):
                known |= {f.name: f for f in found}
            case Err(problem):
                findings.append(Finding(module, problem))
    rows = infer(known, table)
    for facts in known.values():
        findings += undeclared(facts, rows, table)
    return Report(rows, findings)

check() takes source text in a dictionary and a table, and returns a Report. It reads no file and prints nothing, so a test passes it a string and checks the returned value, with no files to create or output to capture. The match on read_module()’s result turns a parse failure into a finding, beside the findings about rows.

Here is the checker on Appendix A’s greeting program, with one function added:

# greeting_check.py
from typing import Final
from row_check import check

GREETING: Final[str] = '''
from typing import Annotated
from effect_rows import performs

class Ask: ...
class Tell: ...

def ask(prompt: str) -> Annotated[str, performs(Ask)]:
    return input(prompt)

def tell(message: str) -> Annotated[None, performs(Tell)]:
    print(message)

def greet() -> Annotated[None, performs(Ask, Tell)]:
    name: str = ask("What is your name? ")
    tell(f"Hello, {name}!")

def shout(message: str) -> None:
    tell(message.upper())

def quiet() -> Annotated[None, performs()]:
    shout("hi")
'''
report = check({"greeting": GREETING})
for name, row in report.rows.items():
    if row:
        print(name, sorted(row))
#: greeting.ask ['Ask']
#: greeting.tell ['Tell']
#: greeting.greet ['Ask', 'Tell']
#: greeting.shout ['Tell']
for finding in report.findings:
    print(finding.where, finding.problem)
#: greeting.ask undeclared Console
#: greeting.tell undeclared Console
#: greeting.quiet undeclared Tell

The demo prints each nonempty row, then each finding. Appendix A’s row(shout) read [], because shout() declares nothing. The checker infers ['Tell'] from the call to tell(). quiet() declares itself pure and calls shout(), and the checker reports quiet(), two calls away from the tell() whose declaration supplies the Tell. Carrying Tell up two calls is propagation, which Appendix A’s tracked_greeting.py cannot do.

Facts About a Function predicts the first two findings. ask() and tell() perform Console and say Ask and Tell. Adding hides(Console) to each clears both findings, as this test file shows:

# test_row_check.py
from typing import Final
from row_check import Finding, check

HEAD: Final[str] = "from typing import Annotated\n"

def findings(source: str) -> list[Finding]:
    return check({"m": HEAD + source}).findings

def test_an_undeclared_effect_is_a_finding() -> None:
    source = (
        "def f() -> Annotated[None, performs()]:\n"
        "    print('hi')\n"
    )
    assert findings(source) == [
        Finding("m.f", "undeclared Console")
    ]

def test_a_declared_effect_is_not() -> None:
    source = (
        "def f() -> Annotated[None, performs(Console)]:\n"
        "    print('hi')\n"
    )
    assert findings(source) == []

def test_hides_removes_an_effect_from_the_body() -> None:
    source = (
        "def f() -> Annotated[\n"
        "    None, performs(Tell), hides(Console)\n"
        "]:\n"
        "    print('hi')\n"
    )
    assert findings(source) == []

def test_an_unannotated_function_is_inferred() -> None:
    report = check({"m": "def f():\n    print('hi')\n"})
    assert report.findings == []
    assert report.rows["m.f"] == {"Console"}

def test_an_unresolved_call_is_unknown() -> None:
    source = (
        "def f(action) -> Annotated[None, performs()]:\n"
        "    action()\n"
    )
    assert findings(source) == [
        Finding("m.f", "undeclared Unknown")
    ]

def test_a_broken_module_is_a_finding() -> None:
    report = check({"bad": "def f(:\n"})
    assert [f.where for f in report.findings] == ["bad"]

Effects for Code You Don’t Own

The table covers the standard library with patterns. A third-party library needs the other form, a stub: source text in this appendix’s own notation, passed to check() under the library’s module name.

# third_party_stub.py
from typing import Final
from row_check import check

APP: Final[str] = '''
import requests
from typing import Annotated
from effect_names import Network
from effect_rows import performs

def fetch(url: str) -> Annotated[str, performs(Network)]:
    return requests.get(url).text
'''
STUB: Final[str] = '''
from typing import Annotated
from effect_names import Network
from effect_rows import performs

def get(
    url: str,
) -> Annotated[object, performs(Network)]: ...
'''

def problems(sources: dict[str, str]) -> list[str]:
    return [f.problem for f in check(sources).findings]

print(problems({"app": APP}))
#: ['undeclared Unknown']
print(problems({"app": APP, "requests": STUB}))
#: []

Without the stub, requests.get matches nothing in the table and reads Unknown, so fetch() draws a finding. With it, requests.get is a declared function like any other. The checker’s existing rule covers requests.get. Callers trust a declared row. The stub’s body is ..., which calls nothing, so its body row is empty and stays within its declaration. Type checkers solve the same problem the same way, with stub files that declare the types of code they cannot read.

The Checker Checks Itself

Every function in the checker so far is pure. This listing is the edge, the one place the checker reads a file or writes to the console. Each of its functions declares the row it performs:

# check_files.py
from pathlib import Path
from typing import Annotated, Final
from effect_names import Console, FileSystem
from effect_rows import performs
from row_check import Report, check

def read(
    path: Path,
) -> Annotated[str, performs(FileSystem)]:
    return path.read_text(encoding="utf-8")

def load(
    paths: list[Path],
) -> Annotated[dict[str, str], performs(FileSystem)]:
    return {path.stem: read(path) for path in paths}

def show(
    report: Report,
) -> Annotated[None, performs(Console)]:
    for name in report.rows:
        if row := report.rows[name]:
            print(name, sorted(row))
    for finding in report.findings:
        print("!", finding.where, finding.problem)

FILES: Final[list[str]] = [
    "effect_table.py",
    "call_names.py",
    "function_facts.py",
    "infer_rows.py",
    "row_check.py",
    "check_files.py",
    "../utils/result.py",
]
show(check(load([Path(name) for name in FILES])))
#: check_files.read ['FileSystem']
#: check_files.load ['FileSystem']
#: check_files.show ['Console']
#: check_files.<module> ['Console', 'FileSystem']
#: result.Ok.bind ['Unknown']

The demo runs the checker on six of its own source files and on utils/result.py, and prints every nonempty row. Because the output names no function from effect_table.py, call_names.py, function_facts.py, infer_rows.py, or row_check.py, the checker confirms that its core is pure. FileSystem and Console appear in three functions at the edge and in the module that calls them. Effect Management calls that arrangement pushing the Effects to the edges, and here a tool verifies it.

The one Unknown is Ok.bind(), which calls the function it receives. That call is the callback problem of Effect Tracking, appearing in a class from this book.

Reaching that output took four changes to the checker’s own code. imports_of() called a.name.split(".") on a loop variable, which has no written type, so top_of() now takes the name as an annotated parameter. body_row() called PURE.union(), a method on an imported constant, and now calls frozenset().union(). type_of() called self.types.get(), a method on a record’s field, and now tests name in self.types in a pattern’s guard. load() called path.read_text() inside a comprehension, and now calls read(path). Each change is small, and two of them improved the code. All four are what the tool requires. You write for it as you write for a type checker, with types where the tool needs them.

What the Checker Resolves, and What It Cannot See

Here, in one place, is what the checker resolves:

Every limit below produces Unknown, so each one appears in a row instead of going unreported:

A name bound in one of those ways is a variable of no known type, even when it matches the name of a built-in. Both functions here perform FileSystem:

# binding_check.py
from typing import Final
from row_check import check

SOURCE: Final[str] = '''
from pathlib import Path

def clear(paths: list[Path]) -> None:
    for dir in paths:
        dir.rmdir()

def load() -> str:
    path = "settings.toml"
    path = Path(path)
    return path.read_text()
'''
report = check({"m": SOURCE})
for name, row in report.rows.items():
    if row:
        print(name, sorted(row))
#: m.clear ['Unknown']
#: m.load ['Unknown']

The checker cannot see that FileSystem, so each row reads Unknown. If assigned() recorded no binding for the loop variable, dir.rmdir() would resolve to builtins.dir.rmdir. If it kept the first assignment’s type, path.read_text() would resolve to builtins.str.read_text. The builtins.* pattern calls both pure, so both rows would be empty.

The limits in this second list produce no Unknown. The checker reports nothing about them, and a production tool must remove each one:

Some of the second list is bookkeeping, such as resolving Annotated through the imports and reading the decorator that marks a staticmethod. Cleverness removes none of the rest, in either list. Most are pieces of type inference. An operator runs a method that its operands’ types select, and a method on a call’s result needs the type the call returns. A callback needs the Effect variable of Effect Tracking. Appendix A’s argument holds. Past this point you are writing a type checker. Much of tracking needs no type inference, though. Name resolution, a table of the standard library, and a fixed point give every function in a program a row. Here they also verify the architecture of the program that computes the rows.