Lesson 6.6 — Flow-sensitive typing: occurrence typing, narrowing and smart casts¶
Techniques: occurrence typing — typing judgments that carry "then" and "else" propositions about variables, so a variable's type depends on the tests that guard its occurrence (Tobin-Hochstadt & Felleisen, Typed Scheme 2008 [THF08] and logical types 2010 [THF10]; Typed Racket [TR-Guide]; mypy and Pyright for Python); control-flow narrowing and smart casts — a dataflow analysis over the control-flow graph that refines union types at
typeof/===/instanceoftests, early returns and assignments (TypeScript [TS-Narrowing, TSC-Checker]) and Kotlin's smart casts restricted to stable variables [KOTLIN-Casts] · Pebble implements: none — Pebble has no union types, so a variable's type never changes along the flow; this lesson is theory, the drillnarrowing, and real tools · Drills:narrowing· Prerequisites: Lessons 6.1 and 6.5 (unions refine by subtyping); Lesson 5.7 (dataflow on the AST) · Time: 3 hours
Programs in dynamically typed languages test types all the time: if (typeof x === "string") return x.length;. A static type system that gives x one type for its whole scope — string | number — must reject x.length inside the test even though it is obviously safe there. Flow-sensitive typing lets the type of a variable change along the control flow: after a successful typeof x === "string" the type of x is string; after if (x === null) return; it is the declared type without null. Two traditions reached the same place from different directions: occurrence typing, a logic of propositions attached to typing judgments, designed to type existing Scheme programs; and narrowing, a dataflow analysis over the control-flow graph, designed to type existing JavaScript. The drill narrowing exercises the second; the proofs show why both are sound.
1. Problem and motivation¶
Occurrence typing¶
The problem. In an untyped language, the idiom (if (number? x) (add1 x) (string-length x)) is safe: each occurrence of x is guarded by a predicate. A conventional type system gives x : (U Number String) everywhere and rejects both branches. Tobin-Hochstadt and Felleisen designed occurrence typing for Typed Scheme (now Typed Racket) so that existing Scheme programs could be typed without restructuring [THF08]: predicates like number? have latent types that say what they prove about their argument, and the typing rule for if checks each branch in an environment refined by what the test proved. Their 2010 paper recast it as a logic: every expression's typing carries a proposition that holds when it evaluates to a true value and one that holds when it is false, combined through and, or and not [THF10]. mypy and Pyright use the same idea for Python's isinstance and is None tests [MYPY-Checker].
Control-flow narrowing and smart casts¶
The problem. JavaScript code tests types with typeof, ===, instanceof, truthiness and discriminant fields, and it uses statements — early return, throw, assignments — not only nested expressions. TypeScript therefore computes a variable's type at every reference by a backward walk over the function's control-flow graph, narrowing the declared union at each test and assignment it passes and widening back by union at join points [TS-Narrowing]. Kotlin's smart casts do the same for is checks and null checks, with a restriction TypeScript does not make: the variable must be stable — not a mutable property, and not a local var modified by a lambda — because otherwise the checked fact may be invalidated between the check and the use [KOTLIN-Casts]. Pebble would need this if it added union or nullable types; Chapter 14's dataflow framework is the general machinery.
2. Definitions and algorithms¶
Both techniques refine a union type over a finite set of primitive types, which is all the drill and the running example need.
Definition 6.6.1 (Union types, restriction and removal)
Let \(\mathcal{P}\) be a finite set of primitive types (the drill: number, string, boolean, null, undefined). A union type is a subset \(U \subseteq \mathcal{P}\), written \(p_1 \mid \cdots \mid p_k\); the empty union is \(\mathsf{never}\) (\(\bot\)), and \(U <: V\) iff \(U \subseteq V\). For a test \(g\) on a value, \(\mathrm{holds}(g, p)\) says whether \(g\) is true of every value of type \(p\). Restriction and removal are \(U \downarrow g = \{ p \in U \mid \mathrm{holds}(g, p) \}\) and \(U \setminus g = \{ p \in U \mid \neg\mathrm{holds}(g, p) \}\).
For the drill's tests, \(\mathrm{holds}\) is exact: typeof x === "number" holds for number only; typeof x === "object" holds for null (JavaScript's historical quirk) and would hold for objects; x === null for null; x == null for null and undefined.
Occurrence typing¶
Definition 6.6.2 (Propositions; typing with then/else propositions)
A proposition \(\psi\) is built from atoms \(x \in U\) ("the value of \(x\) has a type in \(U\)") with \(\land\), \(\lor\), \(\mathsf{tt}\), \(\mathsf{ff}\). The judgment \(\Gamma \vdash e : \tau \mathrel{;} \psi_{+} \mid \psi_{-}\) says: \(e\) has type \(\tau\); if it evaluates to a true value then \(\psi_{+}\) holds, and if to a false value then \(\psi_{-}\) holds. Refining a context by a proposition, \(\Gamma + \psi\), intersects: \(\Gamma + (x \in U) = \Gamma[x \mapsto \Gamma(x) \cap U]\), \(\Gamma + (\psi_1 \land \psi_2) = (\Gamma + \psi_1) + \psi_2\), \(\Gamma + \mathsf{ff}\) marks the context unreachable; for \(\psi_1 \lor \psi_2\) the refinement of each variable is the union of its refinements under \(\psi_1\) and under \(\psi_2\). The key rules [THF10, §3] are
and dually for ||: \(\psi_{1+} \lor (\psi_{1-} \land \psi_{2+}) \mid \psi_{1-} \land \psi_{2-}\), with \(e_2\) typed under \(\Gamma + \psi_{1-}\). A variable occurrence \(x\) is typed by T-Var in the refined context, so its type depends on the tests that dominate it.
Control-flow narrowing and smart casts¶
Algorithm 6.6.3 (Narrowing a union-typed variable along the control flow)
- Input: a function whose parameter \(x\) is declared with a union \(D\); its body as a statement list (probes,
ifwith guards,if (g) return;, assignmentsx = literal); guards built from the tests of Definition 6.6.1 with!,&&,||. - Output: the type of \(x\) at every probe (a subset of \(D\); \(\emptyset\) = unreachable,
never). - Precondition: the guards test only \(x\) and have no side effects; the body is loop-free (loops: §6).
- Postcondition: the state at each probe is exactly the set of primitive types \(p \in D\) such that some execution reaches the probe with \(x\) currently holding a value of type \(p\) (Theorem 6.6.7; after an assignment this differs from the initial type).
- Invariant:
Runis called with the state of the program point before its first statement;Narrow(g, S)returns the parts of \(S\) for which \(g\) can be true and can be false.
function Analyze(D, stmts):
Run(stmts, D); return the recorded probe states
function Run(stmts, S):
for each s in stmts:
case s of
probe p: record(p, S)
x = literal: S ← {type of literal} if S ≠ ∅ else ∅
if (g) return; (T, F) ← Narrow(g, S); S ← F
if (g) A else B:
(T, F) ← Narrow(g, S)
S ← Run(A, T) ∪ Run(B, F) # the join
return S
function Narrow(g, S): # (true part, false part), as short-circuit evaluation visits g
case g of
atomic test t: return (S ↓ t, S \ t)
!g1: (T, F) ← Narrow(g1, S); return (F, T)
g1 && g2: (T1, F1) ← Narrow(g1, S); (T2, F2) ← Narrow(g2, T1)
return (T2, F1 ∪ F2)
g1 || g2: (T1, F1) ← Narrow(g1, S); (T2, F2) ← Narrow(g2, F1)
return (T1 ∪ T2, F2)
This is the drill's oracle (tools/course/lib/narrowing.py). Narrow is T-Test, T-Not and T-And of Definition 6.6.2 computed on sets instead of propositions: \(\psi_{1-} \lor (\psi_{1+} \land \psi_{2-})\) becomes \(F_1 \cup F_2\) with \(F_2\) computed from \(T_1\).
Definition 6.6.4 (Stable variable; smart cast)
A variable is stable at a use if no write to it can happen between a dominating type test and the use: in Kotlin, a val, or a local var that is not written between the test and the use on any path and is not captured by a lambda that writes it; mutable properties (var members, open or custom-getter properties, properties of other modules) are never stable [KOTLIN-Casts]. A smart cast is the narrowing of Algorithm 6.6.3 applied only to stable variables.
Algorithm 6.6.5 (Smart-cast legality check)
- Input: a use \(u\) of variable \(v\) at which narrowing refines \(v\)'s type from \(D\) to \(N \subsetneq D\).
- Output: "cast allowed" or the reason it is not.
- Precondition: the dominating test \(c\) that refined the type is known (Algorithm 6.6.3 records it).
- Postcondition: allowed ⇒ the value read at \(u\) is the value tested at \(c\) (Theorem 6.6.8).
- Invariant: —
function SmartCastAllowed(v, c, u):
if v is a property:
if v is `var`, open, has a custom getter, or is declared in another module:
return "mutable property that could be mutated concurrently"
return allowed
if v is a local val: return allowed
# local var
if some lambda capturing v writes v: return "local variable mutated in a capturing closure"
if some path from c to u contains a write to v: return narrowing restarts at the write
return allowed
3. Worked examples¶
Occurrence typing¶
Occurrence typing on if (x is int and x > 0) then f(x) else g(x) with \(x : \{\mathsf{int}, \mathsf{str}, \mathsf{None}\}\) (Python's isinstance, as mypy does it): the test isinstance(x, int) gives \(\psi_{1+} = x \in \{\mathsf{int}\}\), \(\psi_{1-} = x \in \{\mathsf{str}, \mathsf{None}\}\); x > 0 is typed in \(\Gamma + \psi_{1+}\) (so \(x : \mathsf{int}\) there) and proves nothing about \(x\)'s type, so \(\psi_{2+} = \psi_{2-} = \mathsf{tt}\). T-And gives
| proposition | formula | refined type of \(x\) |
|---|---|---|
| then (\(\psi_{+}\)) | \(x \in \{\mathsf{int}\} \land \mathsf{tt}\) | int |
| else (\(\psi_{-}\)) | \(x \in \{\mathsf{str}, \mathsf{None}\} \lor (x \in \{\mathsf{int}\} \land \mathsf{tt})\) | int | str | None |
The else branch keeps int: a non-positive integer makes the test false. This is exactly mypy's and Pyright's answer in the box of §7 (line 9 there).
Control-flow narrowing and smart casts¶
The lesson's running TypeScript function (checked with tsc in §7; the unit test Narrowing.test_lesson_example runs the oracle on it):
function f(x: number | string | boolean | null | undefined) {
x; // p1
if (x === null) return;
x; // p2
if (typeof x === "number" || typeof x === "boolean") { x; /* p3 */ } else { x; /* p4 */ }
if (typeof x === "object") { x; /* p5 */ } else { x; /* p6 */ }
if (!(typeof x === "string") && x == null) { x; /* p7 */ } else { x = "s"; x; /* p8 */ }
x; // p9
}
Algorithm 6.6.3, one row per step (N, S, B, Nl, U abbreviate number, string, boolean, null, undefined):
| step | what | state(s) |
|---|---|---|
| 1 | start, probe p1 | {N, S, B, Nl, U} |
| 2 | guard x === null |
true {Nl}; false {N, S, B, U} |
| 3 | return on true; continue with false; probe p2 |
{N, S, B, U} |
| 4 | guard typeof x === "number" on |
true {N}; false {S, B, U} |
| 5 | guard typeof x === "boolean" on the false part {S, B, U} (\|\|) |
true {B}; false {S, U} |
| 6 | \|\|: true = {N} ∪ {B}; false = {S, U}; probes p3, p4 |
p3 {N, B}; p4 {S, U} |
| 7 | join | {N, S, B, U} |
| 8 | guard typeof x === "object" |
true {} (null was removed); false |
| 9 | probes p5, p6; join | p5 never; p6 {N, S, B, U}; after: {N, S, B, U} |
| 10 | guard typeof x === "string" |
true {S}; false {N, B, U} |
| 11 | ! swaps: !(…) true {N, B, U}; false {S} |
|
| 12 | guard x == null on the true part {N, B, U} (&&) |
true {U}; false {N, B} |
| 13 | &&: true = {U}; false = {S} ∪ {N, B} |
p7 {U}; else branch {N, S, B} |
| 14 | else: x = "s" makes it {S}; probe p8 |
p8 |
| 15 | join {U} ∪ {S}; probe p9 | {S, U} |
- Step 5 is where
||differs from a naive "narrow both operands from the same state": the second test runs only when the first was false. - Step 8 is the JavaScript quirk:
typeof nullis"object", but null was already removed at step 3, so p5 is unreachable (never). - Step 14: an assignment narrows to the assigned value's type within the declared type — TypeScript's assignment narrowing.
Try it
./course drill narrowing --seed 3 --difficulty hard --solution generates a similar function with nested ifs and assignments.
A Kotlin smart cast on the same idea: in if (x is String) return x.uppercase() the use of x is dominated by the test and x is a parameter (stable), so Algorithm 6.6.5 allows the cast; in if (h.value is String) return h.value.length with var value a property, it refuses, because another thread (or a called function) may assign h.value between the test and the read.
4. Invariants and correctness¶
Occurrence typing¶
Theorem 6.6.6 (Soundness of propositions)
If \(\Gamma \vdash e : \tau \mathrel{;} \psi_{+} \mid \psi_{-}\) by the rules of Definition 6.6.2, and \(e\) is evaluated in an environment whose values satisfy \(\Gamma\) (each \(x\) holds a value of a type in \(\Gamma(x)\)), then: if \(e\) evaluates to a true value, the environment satisfies \(\psi_{+}\); if to a false value, it satisfies \(\psi_{-}\).
Proof
By induction on the typing derivation. T-Test: \(\mathit{test}_g(x)\) is true exactly when the value of \(x\) has a type \(p\) with \(\mathrm{holds}(g, p)\) (the tests are exact), and that type is in \(\Gamma(x) = U\), hence in \(U{\downarrow}g\); symmetrically for false. T-Not: the value is true iff \(e\)'s is false, so the propositions swap. T-And: e1 && e2 is true iff both are true; \(e_1\) true gives \(\psi_{1+}\) (hypothesis), and then \(e_2\) is evaluated in an environment satisfying \(\Gamma + \psi_{1+}\), so its truth gives \(\psi_{2+}\) (hypothesis applied under the refined context): \(\psi_{1+} \land \psi_{2+}\). It is false iff \(e_1\) is false (\(\psi_{1-}\)) or \(e_1\) is true and \(e_2\) false (\(\psi_{1+} \land \psi_{2-}\)). || is dual. Expressions that prove nothing get \(\mathsf{tt} \mid \mathsf{tt}\), which always holds.
Control-flow narrowing and smart casts¶
Theorem 6.6.7 (Algorithm 6.6.3 is sound and exact for single-variable tests)
For every probe \(p\), the state recorded by Algorithm 6.6.3 is \(\{\, t' \in D \mid \text{some execution reaches } p \text{ with } x \text{ currently holding a value of type } t' \,\}\), where executions start with \(x\) holding a value of any type in \(D\) — the analysis never omits a possible type (soundness) and never includes an impossible one (exactness). (After an assignment the current type differs from the initial one: at p8 of §3 the state is {S}, although executions starting with N, S or B reach it.)
Proof
Fix \(t \in D\) and consider executions starting with a value of type \(t\). Because every guard tests only \(x\)'s type and the tests are exact, whether a guard is true is a function of the current type of \(x\) alone, and the statement sequence is loop-free; so the execution is determined by \(t\) (a single path). Claim, by induction on the statements executed: when Run is at a program point with state \(S\), then \(t' \in S\) iff the path for some initial type reaches that point with \(x\) of current type \(t'\). Probe: records \(S\). Assignment: every path reaching it continues with \(x\) of the literal's type, and it is reached iff \(S \ne \emptyset\). Guard: by induction on the guard's structure, Narrow returns exactly the current types for which the guard evaluates to true and to false: atomic tests by exactness; ! swaps; for g1 && g2, \(g_2\) is evaluated exactly when \(g_1\) is true, i.e. for types in \(T_1\), and the whole is true for \(T_2\) and false for \(F_1\) (first operand false) or \(F_2\) (second false) — matching Definition 6.6.2's propositions (Theorem 6.6.6). if (g) return: only the false part continues. if … else join: a type reaches the point after the if iff it reaches the end of one of the branches, so the union is exact. Applying the claim at each probe gives the theorem.
Theorem 6.6.8 (Smart casts are sound for stable variables)
If Algorithm 6.6.5 allows a smart cast of \(v\) at use \(u\), then in every execution the value of \(v\) read at \(u\) has the type established by the dominating test \(c\).
Proof
Since \(c\) dominates \(u\), every execution reaching \(u\) executed \(c\) with the outcome that led to \(u\)'s branch, so at \(c\) the value had the refined type. Stability means no write to \(v\) occurs between \(c\) and \(u\) in any execution: a val is never written after initialization; a local var not written on any \(c\)-to-\(u\) path and not captured by a writing lambda can be written only by statements on such paths (a lambda that captures it is the only other way to reach its storage, and none writes); a final, non-open property with the default getter returns its stored, unmodified value. So the value read at \(u\) is the value tested at \(c\). When the algorithm refuses (a mutable property, a captured-and-written local), a write between \(c\) and \(u\) is possible — from another thread, a callee, or the lambda — and the refined type could be false, which is why TypeScript's corresponding narrowing of mutable properties is unsound in the presence of intervening calls (a documented trade-off).
5. Complexity¶
| Technique | Time (worst) | Time (typical) | Space | Variables |
|---|---|---|---|---|
| Occurrence typing (Definition 6.6.2) | propositions can grow with the size of guards; normalized over one variable: \(O(n \cdot \lvert \mathcal{P} \rvert)\) | linear | \(O(v \cdot \lvert \mathcal{P} \rvert)\) | \(n\) AST nodes, \(v\) variables |
| Narrowing (Algorithm 6.6.3), loop-free | \(O(n \cdot \lvert \mathcal{P} \rvert)\) | linear | \(O(\lvert \mathcal{P} \rvert)\) per state | \(n\) statements and guard nodes |
| Narrowing with loops (TypeScript) | \(O(n \cdot h)\) passes, \(h \le \lvert \mathcal{P} \rvert\) | a few passes per loop | per flow node | lattice height \(h\) |
| Smart-cast legality (Algorithm 6.6.5) | \(O(n)\) per variable (capture and write scan) | cached per variable | \(O(n)\) | — |
Justification. Each guard node and each statement is processed once by Narrow/Run, and each set operation on subsets of a fixed \(\mathcal{P}\) is \(O(\lvert \mathcal{P} \rvert)\) (a bit mask: \(O(1)\)). With loops, states can only shrink along a loop's back edge toward the declared type's subsets, so a fixed point is reached after at most \(\lvert \mathcal{P} \rvert\) changes per point (the lattice of subsets has height \(\lvert \mathcal{P} \rvert\), Chapter 14).
Pathological family. TypeScript computes narrowing on demand, walking the flow graph backwards from each reference; a function with \(r\) references after a chain of \(k\) tests walks the chain for each reference, \(\Theta(r \cdot k)\) without caching, which is why its checker caches flow types per flow node. Propositional occurrence typing with arbitrary propositions (several variables, or of ands) can blow up as disjunctive normal forms: \(k\) nested || of && tests on different variables yield up to \(2^k\) disjuncts; Typed Racket normalizes and simplifies propositions to keep them small.
Scale. Narrowing is part of every expression reference in TypeScript, so its cost is paid per identifier; TypeScript's getFlowTypeOfReference [TSC-Checker] is one of the hottest functions of the checker.
6. Variants and refinements¶
Occurrence typing¶
- Latent predicates on user functions (Typed Racket's
(-> Any Boolean : Number), TypeScript'sx is Ttype predicates, mypy'sTypeGuard/TypeIs): a function's type records what its result proves, so user-defined tests narrow like built-ins. Trade-off: the checker trusts the annotation (TypeScript) or verifies it (Typed Racket). - Paths into data (
(car p)in [THF10], TypeScript's discriminated unionsif (s.kind === "circle")): propositions about fields refine the type of the containing object. - Refinement types (Liquid Haskell): propositions are arithmetic predicates checked by an SMT solver; occurrence typing's structure with a much richer logic.
Control-flow narrowing and smart casts¶
- Loops and fixed points (TypeScript): narrowing through loop back edges by iteration to a fixed point on the union lattice.
- Truthiness narrowing (
if (x)removesnull,undefined, and the falsy literal types0,"",false): needs literal types to be exact, otherwise it would removenumberfor0. - Definite assignment and nullability together (Kotlin, Swift's
if let, C#'s nullable reference types): the same flow analysis as Lesson 5.7, with "non-null" as the fact; Swift avoids stability issues by binding a new name (if let y = x).
7. In real compilers¶
Occurrence typing¶
mypy's find_isinstance_check [MYPY-Checker] maps a condition to a pair of type maps — the "if" and "else" propositions of Definition 6.6.2 restricted to atoms; Typed Racket's type checker computes the full propositions [THF10].
isinstance and is None in mypy 1.19.1 and Pyright 1.1.408
Reproduce (mypy 1.19.1 and Pyright 1.1.408 via uv):
mkdir -p py && cat > py/occurrence.py <<'EOF'
def describe(x: int | str | None) -> str:
if x is None:
reveal_type(x)
return "nothing"
reveal_type(x)
if isinstance(x, int) and x > 0:
reveal_type(x)
return "positive"
reveal_type(x)
return x if isinstance(x, str) else str(x)
EOF
uvx --from mypy==1.19.1 mypy py/occurrence.py
PYRIGHT_PYTHON_IGNORE_WARNINGS=1 uvx pyright@1.1.408 py/occurrence.py 2>&1 | sed "s|$PWD/||"
Output (complete):
py/occurrence.py:3: note: Revealed type is "None"
py/occurrence.py:5: note: Revealed type is "builtins.int | builtins.str"
py/occurrence.py:7: note: Revealed type is "builtins.int"
py/occurrence.py:9: note: Revealed type is "builtins.int | builtins.str"
Success: no issues found in 1 source file
py/occurrence.py
py/occurrence.py:3:21 - information: Type of "x" is "None"
py/occurrence.py:5:17 - information: Type of "x" is "int | str"
py/occurrence.py:7:21 - information: Type of "x" is "int"
py/occurrence.py:9:17 - information: Type of "x" is "str | int"
0 errors, 0 warnings, 4 informations
What to notice: line 3 is the "then" proposition of x is None, line 5 the "else" one continued after the early return. Line 7 is \(\psi_{+}\) of the and (§3), and line 9 is \(\psi_{-} = \psi_{1-} \lor (\psi_{1+} \land \psi_{2-})\): int stays because x > 0 proves nothing about the type. Both checkers agree on the sets; they print unions in different orders.
Control-flow narrowing and smart casts¶
TypeScript's getFlowTypeOfReference walks flow nodes backwards and narrowTypeByTypeof implements the typeof guard [TSC-Checker]; Kotlin's data-flow analysis decides smart casts.
The running example in tsc 5.9, and Kotlin 2.2's stability rule
Reproduce (tsc 5.9.3 via npx; kotlinc-jvm 2.2.20 from the kotlin-compiler-2.2.20.zip release on GitHub, on JRE 21):
mkdir -p ts kt && cat > ts/narrow.ts <<'EOF'
function f(x: number | string | boolean | null | undefined) {
const p1: never = x;
if (x === null) return;
const p2: never = x;
if (typeof x === "number" || typeof x === "boolean") {
const p3: never = x;
} else {
const p4: never = x;
}
if (typeof x === "object") {
const p5: never = x;
} else {
const p6: never = x;
}
if (!(typeof x === "string") && x == null) {
const p7: never = x;
} else {
x = "s";
const p8: never = x;
}
const p9: never = x;
}
EOF
npx -y -p typescript@5.9 tsc --noEmit --strict ts/narrow.ts
cat > kt/Smart.kt <<'EOF'
fun describe(x: Any?): String {
if (x is String) return x.uppercase() // smart cast: x is String here
if (x !is Int) return "not an int"
return (x + 1).toString() // smart cast: x is Int here
}
class Holder(var value: Any?)
fun viaProperty(h: Holder): Int {
if (h.value is String) return h.value.length // a mutable property is not stable
return 0
}
fun viaLocal(): Int {
var v: Any? = "abc"
val bump = { v = 42 } // v is captured and modified by a lambda
if (v is String) return v.length
bump()
return 0
}
fun main() { println(describe("pebble") + " " + describe(41)) }
EOF
kotlinc kt/Smart.kt -d kt/out 2>&1 | grep -v JAVA_TOOL
Output (complete):
ts/narrow.ts(2,11): error TS2322: Type 'string | number | boolean | null | undefined' is not assignable to type 'never'.
Type 'undefined' is not assignable to type 'never'.
ts/narrow.ts(4,11): error TS2322: Type 'string | number | boolean | undefined' is not assignable to type 'never'.
Type 'undefined' is not assignable to type 'never'.
ts/narrow.ts(6,15): error TS2322: Type 'number | boolean' is not assignable to type 'never'.
Type 'number' is not assignable to type 'never'.
ts/narrow.ts(8,15): error TS2322: Type 'string | undefined' is not assignable to type 'never'.
Type 'undefined' is not assignable to type 'never'.
ts/narrow.ts(13,15): error TS2322: Type 'string | number | boolean | undefined' is not assignable to type 'never'.
Type 'undefined' is not assignable to type 'never'.
ts/narrow.ts(16,15): error TS2322: Type 'undefined' is not assignable to type 'never'.
ts/narrow.ts(19,15): error TS2322: Type 'string' is not assignable to type 'never'.
ts/narrow.ts(21,11): error TS2322: Type 'string | undefined' is not assignable to type 'never'.
Type 'undefined' is not assignable to type 'never'.
kt/Smart.kt:10:35: error: smart cast to 'String' is impossible, because 'value' is a mutable property that could be mutated concurrently.
if (h.value is String) return h.value.length // a mutable property is not stable
^^^^^^^
kt/Smart.kt:17:29: error: smart cast to 'String' is impossible, because 'v' is a local variable that is mutated in a capturing closure.
if (v is String) return v.length
^
What to notice: assigning x to never makes tsc print the narrowed type at each probe. The eight messages are the §3 table's p1–p4, p6–p9 exactly, and p5 (line 11) produces no error because the type there is already never — the unreachable probe. Kotlin accepts describe (two smart casts on a parameter) and refuses exactly the two unstable cases of Algorithm 6.6.5, naming the reason TypeScript ignores.
8. Comparison¶
| Technique | Power / precision | Speed (asymptotic · practical) | Output / error quality | Implementation effort | Typical use |
|---|---|---|---|---|---|
| Occurrence typing | Refines variables (and paths into data) by arbitrary boolean combinations of predicates; sound (Theorem 6.6.6) | Linear with normalized propositions; DNF blow-up in the worst case | Types at each occurrence are explainable by the guarding tests | Medium: propositions in every typing judgment | Typed Racket, mypy/Pyright (isinstance, is None) |
| Control-flow narrowing and smart casts | Exact for single-variable tests on loop-free code (Theorem 6.6.7); follows statements (early returns, assignments); Kotlin adds stability for soundness (Theorem 6.6.8) | \(O(n \cdot \lvert \mathcal{P} \rvert)\); per-reference on demand in TypeScript | Errors show the narrowed union; Kotlin names why a cast is impossible | Medium–high: a flow graph and caching | TypeScript, Kotlin, Swift (if let), C# nullable references, Flow |
Choose occurrence typing when adding types to an expression-oriented untyped language (Scheme, Racket) whose idioms are nested ifs and predicates; choose flow-based narrowing when statements, early returns and assignments matter (JavaScript, Kotlin), and require stability (Kotlin) if your language has shared mutable state and you want soundness.
9. Assessment¶
| Technique | Quiz ids | Drill | Flashcard tag | Exercises |
|---|---|---|---|---|
| Occurrence typing | occurrence-and-else, mypy-else-branch |
narrowing (the &&/|| rules are Definition 6.6.2's) |
occurrence-typing |
— |
| Control-flow narrowing and smart casts | narrowing-trace, kotlin-stability |
narrowing |
narrowing |
— |
References¶
See the chapter references.