Lesson 6.7 — Gradual typing: consistency, casts and blame¶
Techniques: gradual typing — the dynamic type
?, the consistency relation that replaces type equality, and compilation to a cast calculus (Siek & Taha 2006 [ST06]), with the static and dynamic gradual guarantee as the design criterion (Siek, Vitousek, Cimini & Boyland 2015 [SVCB15]); blame and the cost of soundness — casts carry blame labels that name the boundary at fault (Wadler & Findler 2009 [WF09]), and checked boundaries cost time, from a few times slower per call to orders of magnitude for whole partially typed programs (Takikawa et al. 2016 [TFGNVF16]) · Pebble implements: none — Pebble is fully static; the lab's ★ milestone L5 (labs/ch06-bidir,extras/) implements Algorithm 6.7.4 for Bic, and its provided evaluator runs casts and reports blame · Drills: none (the lab's corpus40-*.bic–45-*.bicplays that role) · Prerequisites: Lessons 6.1 (safety), 6.2 (static vs dynamic checking), 6.4 (the lab's language Bic) · Time: 3 hours
Lesson 6.2 put static and dynamic checking at the two ends of a line. Real code bases move along it: a Python or JavaScript program gains annotations one module at a time, and the typed part must keep working with the untyped part while that happens. Gradual typing makes this a type system: a program may leave any type out (writing the dynamic type ?, Any in Python, any in TypeScript), the checker accepts every use of ? that could succeed, and — in the sound variant — the compiler inserts a run-time cast at every place where a value crosses from less typed to more typed code. When a cast fails, its blame label says which boundary broke the promise. This lesson defines consistency and cast insertion, proves that fully static programs are never blamed and that removing annotations never breaks a program, and measures what sound boundaries cost.
1. Problem and motivation¶
Gradual typing¶
The problem. Replacing type equality by "anything goes when one side is unknown" is easy to say and easy to get wrong. If ? were a supertype of every type (Lesson 6.5's \(\top\)) and a subtype of every type, subsumption would make \(\mathsf{int} <: {?} <: \mathsf{bool}\) and, by transitivity, every type a subtype of every other: the static checker would accept everything. Siek and Taha's observation was that the relation needed is not a preorder: consistency \(\sim\) is reflexive and symmetric but not transitive, \(\mathsf{int} \sim {?}\) and \({?} \sim \mathsf{bool}\) but \(\mathsf{int} \not\sim \mathsf{bool}\) [ST06]. A checker that uses \(\sim\) where the static one uses \(=\) accepts fully static programs exactly as before and fully dynamic ones always; in between, every consistent-but-unequal use is a place where the program assumes something it has not proved — and where a sound implementation must check it at run time.
Blame and the cost of soundness¶
The problem. A failing check deep inside typed code is useless if it only says "expected int". With higher-order values the failure can happen long after the boundary was crossed: a function of type \(\mathsf{bool} \to \mathsf{int}\) passed where \({?} \to {?}\) is expected fails only when someone later calls it with 1. Wadler and Findler attach a blame label to every cast and prove that the typed side of a boundary is never the one blamed [WF09]. And the checks are not free: each crossing costs a test, each function crossing costs a wrapper, and Takikawa et al. found that in Typed Racket many partially typed configurations of real programs are dramatically slower than both the fully typed and the fully untyped versions [TFGNVF16]. This is why TypeScript and mypy check any statically only and insert no casts at all (§7).
2. Definitions and algorithms¶
The lab's language is Bic (Lesson 6.4), extended with ?: an unannotated lambda parameter has type ?, and annotations may mention ?.
Definition 6.7.1 (Gradual types; precision)
Gradual types are \(\tau ::= \mathsf{int} \mid \mathsf{bool} \mid \tau \to \tau \mid \{l_1 : \tau_1, \ldots, l_n : \tau_n\} \mid {?}\). A type without ? is static. Precision \(\tau \sqsubseteq \tau'\) ("\(\tau'\) is less precise than or equal to \(\tau\)") is the least relation with \(\tau \sqsubseteq {?}\) for every \(\tau\), \(\iota \sqsubseteq \iota\) for base types \(\iota\), and closed under the type constructors pointwise: \(\tau_1 \to \tau_2 \sqsubseteq \tau_1' \to \tau_2'\) iff \(\tau_1 \sqsubseteq \tau_1'\) and \(\tau_2 \sqsubseteq \tau_2'\) (note: covariant in the parameter — precision is about information, not substitutability), and records with the same labels pointwise. It lifts to programs: \(e \sqsubseteq e'\) if \(e'\) is \(e\) with some annotations replaced by less precise ones.
Definition 6.7.2 (Consistency; meet)
Consistency \(\tau \sim \sigma\) is the least relation with
It is reflexive and symmetric, not transitive. For consistent \(\tau \sim \sigma\), the meet \(\tau \sqcap \sigma\) keeps the information of both: \({?} \sqcap \sigma = \sigma\), \(\tau \sqcap {?} = \tau\), \(\iota \sqcap \iota = \iota\), and pointwise on functions and records. It is the greatest lower bound of \(\tau\) and \(\sigma\) in \(\sqsubseteq\): \(\tau \sqcap \sigma \sqsubseteq \tau\), \(\tau \sqcap \sigma \sqsubseteq \sigma\).
Definition 6.7.3 (Gradual typing rules, \(\Gamma \vdash_G e : \tau\))
Variables, constants and records as in Lesson 6.3; the other rules replace equality by consistency [ST06]:
A projection \(e.l\) from \(e : {?}\) has type \({?}\); from a record type it is Lesson 6.3's rule. let x: τ = e1 in e2 is G-Ann on \(e_1\).
Algorithm 6.7.4 (Cast insertion: compiling to the cast calculus)
- Input: a Bic program \(e\) and context \(\Gamma\).
- Output: a program \(e'\) of the cast calculus (Bic plus casts \(\langle \sigma \Rightarrow \tau \rangle^{\ell}\, e\)) and its type \(\tau\), or the first type error.
- Precondition: \(e\) contains no casts.
- Postcondition: \(\Gamma \vdash_G e : \tau\) iff the algorithm succeeds with \(\tau\); then \(\Gamma \vdash_C e' : \tau\) and erasing the casts of \(e'\) gives \(e\) (Theorem 6.7.6).
- Invariant: every cast \(\langle \sigma \Rightarrow \tau \rangle^{\ell}\) it inserts has \(\sigma \sim \tau\) and \(\sigma \ne \tau\), and \(\ell\) is the source position of the term it wraps.
function Insert(Γ, e): # returns (e', τ)
case e of
x, n, true, false: return (e, type from Γ or constant)
fn (x: τ1) => b: (b', τ2) ← Insert(Γ + x:τ1, b); return (fn (x: τ1) => b', τ1 → τ2)
fn x => b: (b', τ2) ← Insert(Γ + x:?, b); return (fn x => b', ? → τ2)
e1 e2:
(e1', φ) ← Insert(Γ, e1); (e2', σ) ← Insert(Γ, e2)
if φ = ?: return (Cast(e1', ?, σ → ?) e2', ?)
if φ = τ1 → τ2: require σ ~ τ1; return (e1' Cast(e2', σ, τ1), τ2)
error "applying a non-function"
(e : τ): (e', σ) ← Insert(Γ, e); require σ ~ τ; return (Cast(e', σ, τ), τ)
e1 + e2: each operand: (ei', σi) ← Insert(Γ, ei); require σi ~ int; ei' ← Cast(ei', σi, int)
return (e1' + e2', int)
if c then a else b:
(c', σ) ← Insert(Γ, c); require σ ~ bool; c' ← Cast(c', σ, bool)
(a', τa) ← Insert(Γ, a); (b', τb) ← Insert(Γ, b); require τa ~ τb
μ ← τa ⊓ τb; return (if c' then Cast(a', τa, μ) else Cast(b', τb, μ), μ)
function Cast(e', σ, τ):
if σ = τ: return e' # no cast between equal types
return ⟨σ ⇒ τ⟩^(position of e') e'
The lab's reference (solutions/labs/ch06-bidir/extras/Gradual.cpp) follows this pseudo-code case by case; == casts a ? side to the other side's type.
Blame and the cost of soundness¶
Definition 6.7.5 (Cast calculus values, cast evaluation and blame)
Values are \(v ::= n \mid b \mid \mathit{closure} \mid \{\overline{l = v}\} \mid v\!:\!\iota{\Rightarrow}{?}\) (a value injected into ?, remembering its type) \(\mid \mathit{wrap}(v, \sigma_1 \to \sigma_2 \Rightarrow \tau_1 \to \tau_2, \ell)\). A cast \(\langle \sigma \Rightarrow \tau \rangle^{\ell}\) applied to \(v\):
- \(\sigma = \tau\): \(v\).
- \(\tau = {?}\): inject \(v\) with its type \(\sigma\).
- \(\sigma = {?}\): \(v\) must be an injection \(w : \rho \Rightarrow {?}\); the result is \(\langle \rho \Rightarrow \tau \rangle^{\ell}\, w\).
- functions: \(\mathit{wrap}(v, \sigma \Rightarrow \tau, \ell)\). Applying a wrapper to \(a\) casts the argument backwards with the same label, calls, and casts the result forwards: \(\langle \sigma_2 \Rightarrow \tau_2 \rangle^{\ell}\, (v\ (\langle \tau_1 \Rightarrow \sigma_1 \rangle^{\ell}\, a))\).
- records with the same labels: field by field.
- otherwise (e.g. \(\mathsf{bool} \Rightarrow \mathsf{int}\) reached by rule 3): the program stops with blame \(\ell\).
Operations on a ? value that the checker let through (projection from ?, applying a ? that was cast to \(\sigma \to {?}\)) check the value's shape when they run and blame their own position on failure. [WF09] gives each label a polarity: a failure in rule 3 on a function's result is positive blame (the value broke its promise), a failure when casting a wrapper's argument is negative blame (the context supplied a bad argument); the lab keeps one label and prints its position.
3. Worked examples¶
Gradual typing¶
Take the one-line program (the lab's corpus 41-gradual-blame.bic, here at line 1)
Its unannotated parameter has type ? (G-LamU). In x + 1, G-Add needs \(? \sim \mathsf{int}\) — true — and Algorithm 6.7.4 casts x (column 17) to int; so f : ? -> int. In f true, G-App needs \(\mathsf{bool} \sim {?}\) — true — and the argument is cast to ?. The lab's printProgram prints the cast-inserted program as (output of the reference solution):
The static checker (Lesson 6.3) rejects the original at the unannotated fn (column 9); the gradual checker accepts it and the fault is found when it runs: true is injected (rule 2), then the cast at 1:17 finds an injected bool where int is wanted (rules 3 and 6): blame 1:17. Adding (x: int) moves the error to compile time at true — the gradual guarantee in action (§4).
The meet in G-If matters on functions. With a = (fn (x: int) => x : int -> ?) and b = (fn (y: ?) => 1 : ? -> int), \(\tau_a \sim \tau_b\) and \(\tau_a \sqcap \tau_b = \mathsf{int} \to \mathsf{int}\), so if true then a else b has type int -> int and both branches get a cast to it. Replacing both annotations by ? -> ? gives type ? -> ? — less precise, as it must be (Theorem 6.7.7). A rule that returned ? whenever the branches differ would type the original ? and the less precise version ? -> ?: removing annotations would have made the type more precise. The lab test L5_IfResultIsTheMeet checks exactly this.
Blame and the cost of soundness¶
Corpus 42-gradual-higher-order.bic:
The argument has type \(\mathsf{bool} \to \mathsf{int} \sim {?} \to {?}\), so it is cast with label 1:26 (the inner fn) and becomes a wrapper (rule 4) — nothing fails yet. Inside, g 1 casts 1 to ? (injection). Calling the wrapper casts that argument backwards, \({?} \Rightarrow \mathsf{bool}\) with label 1:26: the injected int is not a bool, blame 1:26. The failure happens inside the body of the first function, but the label names the boundary where the bool -> int function was given a less precise type. In [WF09]'s terms it is negative blame — the context, which called g with an int, broke the contract; the function itself is innocent, as the Blame Theorem promises for the more precisely typed side.
Try it
After implementing L5, build/labs/ch06-bidir's test ch06_bidir_tests --gtest_filter='*L5*' runs the six gradual corpus files and the guarantee checks; print a cast-inserted program with printProgram(*insertCasts(parse(src))) to see the casts above.
4. Invariants and correctness¶
Gradual typing¶
Theorem 6.7.6 (Cast insertion preserves types; casts are between consistent types)
If Algorithm 6.7.4 returns \((e', \tau)\) for \(\Gamma\) and \(e\), then (a) \(\Gamma \vdash_G e : \tau\); (b) \(\Gamma \vdash_C e' : \tau\), where \(\vdash_C\) is the static rules of Lesson 6.3 (with equality) plus \(\dfrac{\Gamma \vdash_C e : \sigma \quad \sigma \sim \tau}{\Gamma \vdash_C \langle \sigma \Rightarrow \tau\rangle^{\ell} e : \tau}\) and G-AppDyn; (c) erasing the casts of \(e'\) gives \(e\). Conversely, if \(\Gamma \vdash_G e : \tau\) the algorithm succeeds with \(\tau\).
Proof
By induction on \(e\), one case per line of Insert; the induction hypothesis gives (a)–(c) for the subterms. Variables and constants: no cast, the rules coincide. Lambdas: the body's result extends the context exactly as G-Lam/G-LamU. Application with \(\varphi = \tau_1 \to \tau_2\): the algorithm requires \(\sigma \sim \tau_1\) — the premise of G-App, giving (a) — and wraps \(e_2'\) in Cast\((e_2', \sigma, \tau_1)\), which has type \(\tau_1\) by the cast rule when \(\sigma \ne \tau_1\) and is \(e_2'\) itself, of type \(\sigma = \tau_1\), otherwise; so the application is typed by the static rule with equal parameter and argument types, giving (b). With \(\varphi = {?}\): G-AppDyn, and the function is cast to \(\sigma \to {?}\) (\(? \sim \sigma \to {?}\) holds), so the static rule applies to the cast function. Annotation, +: the premises \(\sigma \sim \tau\), \(\sigma_i \sim \mathsf{int}\) are exactly what is required, and each cast is to the type the static rule needs. if: the condition is cast to bool; \(\tau_a \sim \tau_b\) is G-If's premise; \(\tau_a \sqcap \tau_b\) exists and is consistent with each branch type (\(\tau \sqcap \sigma \sqsubseteq \tau\), and a type is consistent with any type it is more precise than, by induction on \(\sqsubseteq\)), so the branch casts are well-typed and both branches have type \(\mu\). (c): Cast only adds cast nodes. The converse: every require is a premise of the corresponding G-rule, so if the derivation exists no require fails, and the returned type is the rule's conclusion. The invariant holds because Cast omits equal types and is only called after the corresponding consistency check.
Theorem 6.7.7 (The gradual guarantee [SVCB15])
Let \(e \sqsubseteq e'\) (\(e'\) is \(e\) with some annotations made less precise). Static: if \(\vdash_G e : \tau\) then \(\vdash_G e' : \tau'\) with \(\tau \sqsubseteq \tau'\). Dynamic: if the cast-inserted \(e\) evaluates to a value \(v\), then the cast-inserted \(e'\) evaluates to a value \(v'\) with \(v \sqsubseteq v'\) (equal at base types); if \(e'\) ends in blame, so does \(e\) — removing annotations can only remove failures, never add them.
Proof (static part in full; dynamic part: sketch, full proof: [SVCB15])
Two lemmas, each by induction on the types. (L1) Consistency is monotone in precision: if \(\sigma \sim \tau\), \(\sigma \sqsubseteq \sigma'\) and \(\tau \sqsubseteq \tau'\), then \(\sigma' \sim \tau'\) — if either primed type is ? it holds; otherwise neither unprimed type is ?, both have the primed type's constructor, and the pointwise cases follow by induction. (L2) The meet is monotone: if \(\tau_2 \sim \tau_3\), \(\tau_2 \sqsubseteq \tau_2'\), \(\tau_3 \sqsubseteq \tau_3'\), then \(\tau_2 \sqcap \tau_3 \sqsubseteq \tau_2' \sqcap \tau_3'\) (\(\tau_2' \sim \tau_3'\) by L1) — if \(\tau_2' = {?}\) the right side is \(\tau_3'\) and \(\tau_2 \sqcap \tau_3 \sqsubseteq \tau_3 \sqsubseteq \tau_3'\); symmetrically; otherwise pointwise by induction.
Static part, by induction on the derivation of \(\Gamma \vdash_G e : \tau\), generalized to contexts: if \(\Gamma \sqsubseteq \Gamma'\) pointwise, then \(\Gamma' \vdash_G e' : \tau'\) with \(\tau \sqsubseteq \tau'\). Variables: from \(\Gamma \sqsubseteq \Gamma'\). G-Lam: the annotation \(\tau_1 \sqsubseteq \tau_1'\) extends the contexts consistently, the body by induction, and \(\to\) is monotone in \(\sqsubseteq\). G-App: \(e_1'\) has a type less precise than \(\tau_1 \to \tau_2\), so either ? (then G-AppDyn gives ?, less precise than \(\tau_2\)) or \(\tau_1' \to \tau_2'\) with \(\tau_1 \sqsubseteq \tau_1'\), \(\tau_2 \sqsubseteq \tau_2'\); the argument's \(\sigma \sqsubseteq \sigma'\), and \(\sigma' \sim \tau_1'\) by L1; the result \(\tau_2 \sqsubseteq \tau_2'\). G-AppDyn: \(e_1'\) still has type ?. G-Ann: \(\sigma \sim \tau\) becomes \(\sigma' \sim \tau'\) by L1. G-Add: L1 with \(\mathsf{int} \sqsubseteq \mathsf{int}\). G-If: L1 for the condition and the branches, L2 for the result. Projection: from a record type the field's precision follows pointwise; from ? the result is ?.
Dynamic part (sketch). Relate the two cast-inserted programs by a precision relation on terms and values in which each cast of \(e'\) is less precise than the corresponding cast (or absence of cast) of \(e\), and show a simulation: every step of \(e\) is matched by zero or more steps of \(e'\) that preserve the relation, where the extra steps of \(e'\) are its additional casts to and from ?. The key case is a cast \(\langle \sigma \Rightarrow \tau \rangle\) in \(e\) that succeeds: the corresponding cast in \(e'\) goes between less precise types, and a cast that succeeds cannot fail at less precise types, since each failure of rule 6 requires two incompatible static constructors, which a less precise type (with ? in their place) no longer has. The lab tests the consequence on its corpus and on 200 random programs: L5_GradualGuaranteeOnTheCorpus, L5_GradualGuaranteeOnRandomPrograms (every annotation replaced by ?, same value).
Blame and the cost of soundness¶
Theorem 6.7.8 (Static programs need no casts and are never blamed)
If \(e\) contains no ? (every lambda parameter is annotated with a static type), then Algorithm 6.7.4 inserts no cast into \(e\), \(\vdash_G e : \tau\) iff \(e\) is well-typed by the static rules of Lesson 6.3 at \(\tau\), and running the result never produces blame. More generally, every blame label names the position of a cast whose source or target type contains ?, or of an operation on a ?-typed value (Definition 6.7.5).
Proof
For static types, \(\sigma \sim \tau\) iff \(\sigma = \tau\): by induction on the rules of Definition 6.7.2, the two ? axioms never apply, and the remaining rules are the ones of equality. Similarly \(\sigma \sqcap \sigma = \sigma\). By induction on \(e\), every type computed by Insert is static (constructors of static types; the ? → of G-LamU never arises), so every require σ ~ τ is an equality test — the static rules — and every Cast(e', σ, τ) is called with \(\sigma = \tau\) and inserts nothing. A program without casts and without ?-typed values never reaches rules 2–6 of Definition 6.7.5, and blame is produced only there (or by a dynamic operation on a ? value, of which there are none). For the general statement: every inserted cast has \(\sigma \sim \tau\) and \(\sigma \ne \tau\) (the invariant), and by the first sentence two consistent unequal types cannot both be static, so one of them contains ?; the only other source of blame is a dynamic operation on a ?-typed value, which blames its own position. [WF09] proves the sharper, polarity-aware Blame Theorem: a cast from a more precise to a less precise type can only receive negative blame, and one in the other direction only positive, so "well-typed programs can't be blamed".
5. Complexity¶
| Technique | Time (worst) | Time (typical) | Space | Variables |
|---|---|---|---|---|
| Consistency / meet test | \(O(\lvert\tau\rvert + \lvert\sigma\rvert)\) | small types: \(O(1)\) | \(O(\lvert\tau\rvert)\) for the meet | \(\lvert\tau\rvert\) type size |
| Cast insertion (Algorithm 6.7.4) | \(O(n \cdot t)\) | linear | \(O(n)\) extra cast nodes | \(n\) AST nodes, \(t\) largest type |
| First-order cast at run time | \(O(1)\) (tag test) | \(O(1)\) | \(O(1)\) | — |
| Record / structural cast at run time | \(O(\text{size of the value})\) | per crossing | a copy | — |
| Function cast at run time | \(O(1)\) to wrap; every later call pays two casts | per call | one wrapper per crossing | — |
Justification. Cast insertion is one pass that computes, at each node, at most a constant number of consistency tests and meets on the types of its children; each is a simultaneous traversal of the two types. At run time, rule 3 inspects one tag, rule 5 visits every field (and recursively), rule 4 allocates one wrapper and defers the rest to calls.
Pathological family. Wrappers do not collapse in Definition 6.7.5: a function that crosses a ? -> ? boundary \(k\) times (passed back and forth between typed and untyped code in a loop) is wrapped \(k\) times, and every call then performs \(2k\) casts and uses \(\Theta(k)\) space — a space leak that turns a tail-recursive loop into one with growing memory. Representations that compose casts eagerly keep one cast per value; the lab's evaluator does not.
Scale. Per boundary call, a checked boundary in the §7 measurement makes a trivial Python function 4.4–5.6× slower (two runs of the box's script; the ratio varies with the machine). For whole programs [TFGNVF16] measured every typed/untyped configuration of Typed Racket benchmarks and found configurations orders of magnitude slower than the untyped program — which is why the cost is a design parameter, not an implementation detail (§8).
6. Variants and refinements¶
Gradual typing¶
- Optional typing / erasure (TypeScript
any, mypyAny, Python annotations): consistency in the checker, no casts at run time; unsound (a typedintparameter may hold a string, §7) but free. - Gradual types everywhere:
?inside generic types (List<?>-like), gradual objects and subtyping (consistent subtyping combines Definition 6.7.2 with Lesson 6.5), gradual effects and ownership. - Type inference with
?: unification must treat?specially; Chapter 7's Hindley–Milner meets the same question when a program mixes inferred and dynamic types.
Blame and the cost of soundness¶
- Polarity and contracts [WF09]: two labels per cast (positive, negative) — the lab's single label cannot tell the function from its caller in corpus 42.
- Boundary checks only (the box's decorator): check first-order values where they enter typed code and trust the rest; cheap, but higher-order values escape unchecked.
- Space-efficient casts: compose adjacent casts into one normal form so a value carries at most one pending cast; fixes the pathological family of §5.
7. In real compilers¶
Gradual typing¶
mypy folds consistency into subtyping: _is_subtype returns true when the right side is Any, and SubtypeVisitor.visit_any when the left side is [MYPY-Subtypes]; nothing is inserted into the program, so it is gradual typing without casts. TypeScript's any behaves the same way [TSC-Checker].
Any in mypy 1.19.1 is consistent with int, and nothing is checked at run time (Python 3.11)
Reproduce (mypy 1.19.1 via uv; CPython 3.11):
mkdir -p py && cat > py/gradual.py <<'EOF'
from typing import Any
def inc(x: int) -> int:
return x + 1
def load() -> Any: # e.g. parsed JSON: statically unknown
return "41"
v = load()
print(inc(v)) # Any is consistent with int: no static error, no run-time cast
EOF
uvx --from mypy==1.19.1 mypy --strict py/gradual.py
python3 py/gradual.py 2>&1 | sed "s|$PWD/||" | tail -4
Output (complete):
Success: no issues found in 1 source file
File "py/gradual.py", line 4, in inc
return x + 1
~~^~~
TypeError: can only concatenate str (not "int") to str
What to notice: even --strict accepts inc(v): \(\mathsf{Any} \sim \mathsf{int}\) (Definition 6.7.2). A sound gradual system would insert \(\langle {?} \Rightarrow \mathsf{int}\rangle\) at the call and blame line 10; Python runs the call, and the failure surfaces inside the typed function, on a line whose types are correct, with an error about string concatenation.
Blame and the cost of soundness¶
A sound implementation checks at boundaries. The beartype decorator checks a function's arguments against its annotations on every call — a first-order cast \(\langle {?} \Rightarrow \mathsf{int} \rangle\) whose label is the parameter name.
A checked boundary in Python: beartype 0.22.9's blame message and its cost
Reproduce (beartype 0.22.9 via uv; CPython 3.11):
mkdir -p py && cat > py/blame.py <<'EOF'
import timeit
from typing import Any
from beartype import beartype
@beartype
def inc(x: int) -> int: # a checked boundary: a cast from Any to int on entry
return x + 1
def inc_unchecked(x: int) -> int:
return x + 1
def load() -> Any:
return "41"
n = 1_000_000
t0 = timeit.timeit(lambda: inc_unchecked(41), number=n)
t1 = timeit.timeit(lambda: inc(41), number=n)
print("checked call at least 1.5x slower:", t1 > 1.5 * t0)
try:
inc(load())
except Exception as e:
print(type(e).__name__ + ":", str(e).splitlines()[0])
EOF
uv run --quiet --no-project --with beartype==0.22.9 python3 py/blame.py
Output (complete):
checked call at least 1.5x slower: True
BeartypeCallHintParamViolation: Function __main__.inc() parameter x='41' violates type hint <class 'int'>, as str '41' not instance of int.
What to notice: the failure is now reported at the boundary and blames it — function, parameter, value and expected type — instead of deep inside. Printing the ratio t1 / t0 instead gave 4.4 and 5.6 in two runs on the course container: for a function this small, the check costs several times the call. Only first-order checks are done; a Callable[[int], int] argument would be checked for being callable, not wrapped (§6).
8. Comparison¶
| Technique | Power / precision | Speed (asymptotic · practical) | Output / error quality | Implementation effort | Typical use |
|---|---|---|---|---|---|
| Gradual typing | Accepts every fully static and every fully dynamic program; static programs are typed exactly as before (Theorem 6.7.8); removing annotations never breaks a program (Theorem 6.7.7) | Checking linear; the run-time cost depends on whether casts are inserted | Static errors only where types are known to clash; the rest deferred to run time | Low for the checker (consistency for equality), high for sound run-time casts | TypeScript, mypy/Pyright, Typed Racket, C# dynamic, Dart before 2.0 |
| Blame and the cost of soundness | Sound: typed code never sees an ill-typed value, and failures name the boundary (Theorem 6.7.8, [WF09]) | \(O(1)\) first-order checks, wrappers for functions; whole-program slowdowns up to orders of magnitude [TFGNVF16] | Blame names the boundary and, with polarity, which side broke it | High: wrappers, representation of injected values, space-efficient casts | Typed Racket (contracts), beartype-style boundary checks; erased in TypeScript and mypy |
Choose erasure (TypeScript, mypy) when adoption and zero run-time cost matter more than a guarantee; choose sound casts with blame when typed code must be able to trust its types (a typed library used from untyped code) and the boundaries are coarse enough that their cost is paid rarely.
9. Assessment¶
| Technique | Quiz ids | Drill | Flashcard tag | Exercises |
|---|---|---|---|---|
| Gradual typing | consistency-not-transitive, gradual-cast-insertion |
— | gradual |
Lab L5 (★) |
| Blame and the cost of soundness | blame-label, mypy-any-no-cast |
— | blame |
Lab L5 (★) |
References¶
See the chapter references.