Static Type Checking

The previous lesson modeled a single step of the side reading the annotation: inferring a call site’s return type. The measurement showed that the generic notation could declare both violations with no false alarm — but there was no program making the declaration, only an inference rule.

This lesson builds that program. A layer that reads the source or the annotations, compares calls against the signature, and declares mismatches without running them is called static type checking. The number asked has three parts: of the first lesson’s four violations, how many does this layer find, how many does it miss, and why does it miss the ones it misses?

The Checker Is Modeled in This Lesson

A warning up front: the checker used in this lesson is written within the lesson. No ready-made tool is run, and no tool’s name appears. What is measured is not a specific program’s behavior, it is the approach’s own limit — and that limit follows from the information in the checker’s hand. The modeled checker uses exactly that information: it reads the annotations, looks at the call’s arguments, and lists the mismatches.

The measurement uses two checker forms. The first takes the calls’ arguments directly; because the arguments are constants written into the source, this gives the same information as reading the source. The second does the job more explicitly: it turns the source text into an abstract syntax tree, walks the call nodes in the tree, and compares the constant arguments against the signature. The second never runs the code at all; this is the measurable counterpart of the word “static.”

The Information in the Checker’s Hand

The checker sees three things: the annotations in the signature, the call sites, and the constant values written into the calls. There is exactly one thing it does not see, and the whole lesson is the consequences of that one thing: it does not see the value’s meaning.

The annotation age: int says “an integer comes here.” -5 is an integer. The checker performs the test isinstance(-5, int), gets the answer true, and passes it. In the same way, the annotation name: str does not exclude an empty string, because an empty string is a string. This is not a shortcoming, it is exactly what is written in the signature: the signature declares the type, not the domain.

The measurement’s assumptions:

• TL18 — The oracle is the setup itself: which of the five calls carries a type violation and which carries a domain violation was decided in the first lesson and is not changed here.
• TL19 — The checker is modeled within the lesson; no external tool is run. The model’s rule is singular: if the type of the value bound does not match the type in the annotation, declare it.
• TL20 — The domain rule is also modeled within the lesson and looks at only two conditions: is the name empty, is the age negative. These two conditions are the setup’s definition of a domain violation.
• TL21 — In the scope measurement, the checked code sits as a text constant; it is checked both by being turned into an abstract syntax tree and by being run. The two layers are applied to the same text.
• TL22 — “Executed call site” is the number of calls really reached during a run, and it is counted with a tracked wrapper. The run is done in a single mode.
• TL23 — The abstract-syntax-tree check only tests constant arguments; an argument given as a variable is not checked in this model and is not counted.
• TL24 — In the domain-type measurement, the Age class derives from integer and tests its rule at construction time; the class’s instance behaves like an integer everywhere.
• TL25 — “Declared on the raw call” is how many of the five calls, as written in the source, get declared; what is counted is the call, not the parameter.
• TL26 — “Erroring during construction” is the number of calls that raise an exception when the value is constructed through Age.
• TL27 — No environment-dependent data is written; line numbers are the checked text constant’s own lines.

Measurement

"""Static type checking: what a modeled checker finds, what it cannot see."""
import ast


def describe_person(name: str, age: int) -> str:
    return f"{name}:{age}"


CALLS = (
    ("name", 30),          # valid
    ("name", "thirty"),    # type violation: age is a string
    (7, 30),               # type violation: name is a number
    ("name", -5),          # type valid, domain violation: age negative
    ("", 30),              # type valid, domain violation: name empty
)


def checker(function_, calls):
    """Modeled checker reading annotations and checking calls.

    Only sees TYPE mismatch; cannot see the value's meaning.
    """
    signature = [(a, t) for a, t in function_.__annotations__.items() if a != "return"]
    found = []
    for i, arg in enumerate(calls):
        for (name, type_), value in zip(signature, arg):
            if not isinstance(value, type_):
                found.append((i, name))
    return found


def domain_rule(name, age):
    """Meaning conditions the type cannot see."""
    errors = []
    if isinstance(name, str) and not name:
        errors.append("name empty")
    if isinstance(age, int) and age < 0:
        errors.append("age negative")
    return errors


found = checker(describe_person, CALLS)
type_violations = [i for i, a in enumerate(CALLS)
              if not isinstance(a[0], str) or not isinstance(a[1], int)]
domain_violations = [i for i, a in enumerate(CALLS) if domain_rule(*a)]

print(f"{'call':>6s} {'type violation':>15s} {'domain violation':>17s} "
      f"{'checker found':>15s} {'runtime':>10s}")
for i, arg in enumerate(CALLS):
    print(f"{i:6d} {str(i in type_violations):>15s} {str(i in domain_violations):>17s} "
          f"{str(any(b[0] == i for b in found)):>15s} {'no error':>10s}")
print(f"calls {len(CALLS)}, type violation {len(type_violations)}, domain violation "
      f"{len(domain_violations)}, checker found {len({b[0] for b in found})}")
print(f"parameters the checker flagged: {found}")

SOURCE = '''
def dispatch(mode):
    if mode == "short":
        return describe_person("name", 30)
    if mode == "long":
        return describe_person("name", "thirty")
    return describe_person(7, 30)
'''


def static_check(source, function_):
    """Modeled checker reading source text and checking calls.

    Does not run the code; only walks the syntax tree.
    """
    signature = [(a, t) for a, t in function_.__annotations__.items() if a != "return"]
    sites, found = [], []
    for node in ast.walk(ast.parse(source)):
        if isinstance(node, ast.Call) and getattr(node.func, "id", "") == "describe_person":
            sites.append(node.lineno)
            for arg, (name, type_) in zip(node.args, signature):
                if isinstance(arg, ast.Constant) and not isinstance(arg.value, type_):
                    found.append((node.lineno, name))
    return sites, found


PASSED = []


def tracked(name, age):
    PASSED.append((name, age))
    return describe_person(name, age)


env = {"describe_person": tracked}
exec(SOURCE, env)
errors = 0
try:
    env["dispatch"]("short")
except Exception:
    errors += 1

sites, static = static_check(SOURCE, describe_person)
print()
print(f"call sites in source {len(sites)}, executed {len(PASSED)}, "
      f"runtime errors {errors}")
print(f"call sites the checker saw {len(sites)}, violations found "
      f"{len({y for y, _ in static})}, sites found {static}")

SOURCE2 = '''
def forward(value):
    return describe_person("name", value)
'''
sites2, static2 = static_check(SOURCE2, describe_person)
print(f"call written with a variable: site seen {len(sites2)}, "
      f"arguments tested 0, declared {len(static2)}")


class Age(int):
    """A value object carrying the domain rule into the type: construction tests it."""

    def __new__(cls, value):
        if value < 0:
            raise ValueError("age negative")
        return super().__new__(cls, value)


def describe_person_domain(name: str, age: Age) -> str:
    return f"{name}:{age}"


raw = len({b[0] for b in checker(describe_person_domain, CALLS)})
constructed, construction_errors = [], 0
for name, age in CALLS:
    try:
        constructed.append((name, Age(age)))
    except (ValueError, TypeError):
        construction_errors += 1
after_construction = len({b[0] for b in checker(describe_person_domain, constructed)})
print()
print(f"domain-typed signature: declared on raw calls {raw}, erroring during construction "
      f"{construction_errors}, declared on {len(constructed)} constructed calls {after_construction}")
print(f"is Age(30) an integer: {isinstance(Age(30), int)}; "
      f"empty name is still invisible: {checker(describe_person_domain, [('', Age(30))])}")

  call  type violation  domain violation   checker found    runtime
     0           False             False           False   no error
     1            True             False            True   no error
     2            True             False            True   no error
     3           False              True           False   no error
     4           False              True           False   no error
calls 5, type violation 2, domain violation 2, checker found 2
parameters the checker flagged: [(1, 'age'), (2, 'name')]

call sites in source 3, executed 1, runtime errors 0
call sites the checker saw 3, violations found 2, sites found [(7, 'name'), (6, 'age')]
call written with a variable: site seen 1, arguments tested 0, declared 0

domain-typed signature: declared on raw calls 5, erroring during construction 2, declared on 3 constructed calls 1
is Age(30) an integer: True; empty name is still invisible: []

Two Found, Two Not Found

The upper table gives the lesson’s binding number. 2 of five calls carry a type violation, 2 carry a domain violation. The number of calls the checker finds is 2, and the calls it finds are exactly the ones carrying a type violation: age in the first call, name in the second. On the two calls carrying a domain violation, the column says false.

Who caught it: in this measurement, the checker caught two violations, and no layer caught the other two. The runtime column is clean on all five lines.

The reason for the ones not found can be read in a single line. In the third call, the age is -5, and -5 is an integer; isinstance(-5, int) returns true. In the fourth call, the name is an empty string, and an empty string is a string; isinstance("", str) returns true. The checker did not run wrong — it answered the question it was asked correctly. The question not asked was “is this value valid,” and that question is not written in the signature.

The list of parameters the checker points to also gives the shape of this information limit. The declaration carries not only the call number but also which parameter did not match: age in the first call, name in the second. The declaration can be this specific because a type name is written right next to that parameter in the signature. Because nothing is written across from the domain rule, no such declaration can be produced either.

The Scope Is the Written Code, Not the Executed Code

The second measurement shows what the checker gives in return, and the number is striking.

In the checked text, there are 3 call sites for describe_person; two are violations. When the program is run in a single mode, only 1 of these three is actually reached, because the other two sit inside conditions that are not satisfied. The runtime error count is 0 — both because the reached call is clean, and because, as measured in the previous lesson, the annotation does not stop the call anyway.

The checker walking the abstract syntax tree, by contrast, sees all 3 of the three call sites and declares 2 violations — along with the line numbers, and which parameter did not match. It never ran the code: ast.parse turned the text into a tree, ast.walk walked the tree, no body was executed.

The difference between the two is not a percentage, it is a difference of kind. Run time can only examine the site it reaches; reaching it depends on conditions, input, and the mode of that particular run. The checker’s scope, by contrast, is the text itself: every call site written even once is checked, even if it is never run. The ratio in the measurement is 3/3 against 1/3.

The ratio’s meaning changes with the run. Had the same program been run in three separate modes, all three call sites would have been reached, and the second and third calls still would have raised no error — because the annotation does not stop the call. So the number 1/3 is not a measure of the checking, it is a measure of the scope: it says which piece of code was looked at, not whether what was looked at was found correct.

This does not make up for the two violations the checker cannot find, but it trades off against them. The checker knows less, and it knows that less in more places; run time knows more — it sees the real value in hand — and it knows it in fewer places.

The Model’s Own Limit

One line sits below this table, and honesty requires counting it separately. In a call whose argument is not a constant but a variable, the checker sees the call site — 1 — but the argument it tests is 0 and the violation it declares is 0.

This is not the same kind of limit as the previous section’s. Not finding the domain violation was a knowledge limit: because the rule is written nowhere, no checker can read it. Not being able to test the variable call, by contrast, is a model limit: which value the variable carries could be inferred by tracing the assignments made to it. The checker modeled in this lesson does not do that tracing, and the limit is written explicitly here.

The distinction matters, because the remedy for the two is different. A model limit closes with a better checker. A knowledge limit does not close — without writing the rule down somewhere, no checker can find it. The next section tries what that “somewhere” could be.

Moving the Domain Rule into the Type

The third measurement tries a natural question: if the checker has no domain information in hand, what happens if we put that information into the signature? The measurement builds an Age class deriving from integer; the class tests its rule at construction time, and its instance behaves like an integer everywhere — the last line shows this with isinstance.

Once the signature is age: Age, the checker really changes. 5 of the five calls, as written in the source, get declared: no constant number is an Age instance, not even the clean call. So putting domain information into the signature forces every call site to construct the value.

Once the values are constructed, the table settles into place. 2 of the five calls error during construction — negative age and non-integer age, both fall in the Age constructor. Of the remaining 3 calls, 1 is declared by the checker: the call whose name is a number.

But the last line shows the gap that remains: an empty name is still invisible, because no such type was built for name. Three of four violations are now caught, and the catchers are separate layers — 1 by the checker, 2 by construction.

The result that follows from this is this lesson’s result, and the next lesson’s starting point. Moving the domain rule into the type makes the violation visible, but the place it becomes visible is not the checker, it is run time: the call Age(-5) raises an exception, and that exception comes out while the program runs. The rule moved not into the writing, but into a constructor’s body.

Summary

• Static type checking is a layer that reads code without running it and compares calls against the signature; in this lesson, the checker is modeled within the lesson and no external tool is used.
• The checker finds 2 type violations in five calls and cannot see 2 domain violations. The reason is missing information: -5 is an integer, an empty string is a string, and the signature does not write a domain rule.
• The check’s scope is the written code: the checker walking the abstract syntax tree sees all 3 of three call sites and declares 2 violations, while the run only reaches 1 call site and raises 0 errors.
• The checker knows less, in more places; run time knows more, in fewer places; the two do not substitute for each other.
• The two limits are of different kinds: not being able to test a variable call is a model limit and closes with a better checker; not being able to see a domain rule is a knowledge limit and does not close until the rule is written somewhere.
• Once the domain rule is moved into the type, 5 of the raw calls get declared, 2 error during construction, and 1 of the three constructed calls is caught by the checker — the rule has moved from the writing into a constructor’s body, meaning into run time.

Next Step

The third measurement moved the rule into run time, but did it for a single domain, with a hand-written class. Writing a separate class for every domain does not scale; as the number of rules grows, constructors repeat each other, and where the rules live gets scattered. It is also possible to gather the rules in one place, as the data’s schema, and apply that schema at call time. The next lesson models this layer within the lesson and asks the course’s final number: how many violations does run time, the checker, and the domain rule catch separately — and how many layers does it take to see all four violations?