Lesson 6.2 — Classifying type systems: static and dynamic, strong and weak, sound and unsound¶

Techniques: static checking vs dynamic (tag) checking, and the undecidability that forces static checkers to be conservative (Rice 1953; dynamic typing as one static type, [PFPL, Ch. 22]); strong vs weak typing as trapped vs untrapped errors and implicit reinterpretation (Cardelli [Car96, §1]); sound vs intentionally unsound type systems (TypeScript [TS-Compat], Java's covariant arrays [JLS21-10]) · Pebble implements: static, strong and sound checking; its only run-time checks are the traps of pebble-spec §11.3 · Drills: progress-preservation (what unsoundness means formally) · Prerequisites: Lesson 6.1 · Time: 3 hours

"Is Python strongly typed?" "Is TypeScript sound?" "Is C statically typed?" These questions have precise answers once you separate three independent axes that everyday usage mixes up: when errors are checked (before or during execution), what happens when an operation is applied to the wrong kind of value (a trap or silent garbage), and whether the checker's promise is kept (sound) or deliberately bent for convenience (unsound). This lesson defines the three axes on top of Lesson 6.1's semantics, proves why no static checker can be exact, and runs the same mistake through C, JavaScript, Python, mypy, TypeScript and Java to place each on the map.

1. Problem and motivation¶

Static vs dynamic checking¶

The problem. An operation such as + is meaningful only for some operands. Either the implementation checks, before the program runs, that no execution can apply it to the wrong operands (static checking), or it attaches a tag to every value and checks the tags each time the operation runs (dynamic checking). Lisp (McCarthy 1960) and Smalltalk made dynamic checking the norm for flexible languages; ALGOL 68, Pascal and ML made static checking the norm for safe, fast ones. Rice's theorem (1953) explains why static checking is always conservative: deciding exactly which programs will misuse an operation is undecidable, so a static checker must reject some programs that would never fail. Harper's view [PFPL, Ch. 22] dissolves the dichotomy: a dynamically typed language is a statically typed one with a single type of tagged values. Pebble is statically checked: typeCheck rejects true + 1 before any code exists.

Strong vs weak typing¶

The problem. What happens when a program does apply an operation to the wrong kind of value? Cardelli [Car96, §1] distinguishes trapped errors, which stop execution at once (an exception, a trap), from untrapped errors, which go unnoticed and let the computation continue on meaningless data (reading an int as a pointer, running off the end of an array). A language without untrapped errors is safe; "strongly typed" is informal usage for safe-and-checked, and "weakly typed" for languages that either permit untrapped errors (C) or silently convert between unrelated types (JavaScript's "5" - 1). Pebble is strong in both senses: nothing is undefined behavior (pebble-spec §11.2), and there are no implicit conversions except the literal rule of §5.

Sound vs unsound type systems¶

The problem. A static type system is sound if its promise holds: well-typed programs do not reach the errors the system claims to exclude (Corollary 6.1.17 for Lesson 6.1's language). Some widely used systems are unsound on purpose. TypeScript's designers list the unsound features they accepted for convenience and compatibility with JavaScript idioms [TS-Compat]; Java made arrays covariant in 1995, before it had generics, and pays for soundness with a run-time store check [JLS21-10]. Knowing exactly where a system is unsound tells you which run-time errors your checker cannot rule out, and which optimizations are therefore illegal.

2. Definitions and algorithms¶

Static vs dynamic checking¶

Definition 6.2.1 (Static and dynamic checks)

A static check is a decidable predicate on program texts evaluated before execution; a program failing it is rejected. A dynamic check is a test on run-time values performed as part of evaluating an operation; failing it is a trapped error. A language is statically checked (for a class of errors) if every program that could exhibit such an error is rejected statically, and dynamically checked if every such error is caught by a dynamic check when it would happen.

Theorem 6.2.2 (Exact static checking is undecidable)

Let \(L\) be Lesson 6.1's untyped language extended with general recursion (so that it is Turing-complete). There is no algorithm that decides, for every closed term \(e\) of \(L\), whether some evaluation \(e \longrightarrow^{*} e'\) reaches a stuck \(e'\).

Proof

By reduction from the halting problem. Suppose \(D\) decides "\(e\) can get stuck". Given any closed term \(p\) in which no stuck state is reachable (for example, any term well typed in a safe recursive extension of Lesson 6.1's system, written without errors), build \(q = \mathsf{let}\ z = p\ \mathsf{in}\ (\mathsf{true} + 1)\). Evaluation of \(q\) first evaluates \(p\); if \(p\) never reaches a value, \(q\) never reaches the stuck term \(\mathsf{true} + 1\) (and \(p\) itself never gets stuck); if \(p\) reaches a value, E-LetV produces \(\mathsf{true} + 1\), which is stuck. So \(q\) can get stuck iff \(p\) halts, and \(D(q)\) would decide halting for this class of terms, which contains every Turing machine encoded without errors. Contradiction; hence no such \(D\) exists. (This is an instance of Rice's theorem: "can get stuck" is a non-trivial semantic property.)

Consequently a static type system is a conservative approximation: sound systems reject some programs that would never get stuck, such as if true then 1 else (true + 1), which Figure 6.1.1 rejects although its else branch never runs.

Definition 6.2.3 (Tagged values; dynamic typing as one static type)

A dynamically typed version of Lesson 6.1's language has one static type \(\mathsf{dyn}\) (every closed term has it) and tagged run-time values \(\langle \mathit{tag}, v \rangle\) with \(\mathit{tag} \in \{\mathsf{int}, \mathsf{bool}, \mathsf{fun}\}\). Every elimination form checks the tag of its operand before using it; a tag mismatch raises the trapped error \(\mathsf{error}\) [PFPL, §22.1].

Algorithm 6.2.4 (Evaluation with dynamic tag checks)

Input: a closed term \(e\) of the untyped language.
Output: a tagged value, \(\mathsf{error}\) (a trapped type error), or divergence.
Precondition: values carry their tags; λ-values are closures.
Postcondition: never produces an untrapped error: every operation's operands have the tag it requires, or \(\mathsf{error}\) is returned (Proposition 6.2.9).
Invariant: every value in the environment and every value returned by Eval is tagged.

function Eval(ρ, e):                  # ρ maps variables to tagged values
    case e of
        x:            return ρ(x)
        n:            return ⟨int, n⟩
        true/false:   return ⟨bool, e⟩
        λx. e1:       return ⟨fun, closure(ρ, x, e1)⟩
        e1 e2:        f ← Eval(ρ, e1);  a ← Eval(ρ, e2)
                      if f.tag ≠ fun: return error
                      (ρ', x, body) ← f.value;  return Eval(ρ'[x ↦ a], body)
        e1 + e2:      a ← Eval(ρ, e1);  b ← Eval(ρ, e2)
                      if a.tag ≠ int or b.tag ≠ int: return error
                      return ⟨int, a.value + b.value⟩
        e1 < e2:      as for +, returning ⟨bool, a.value < b.value⟩
        if c then t else f:
                      v ← Eval(ρ, c);  if v.tag ≠ bool: return error
                      return Eval(ρ, t) if v.value = true else Eval(ρ, f)
        let x = e1 in e2:  return Eval(ρ[x ↦ Eval(ρ, e1)], e2)

error propagates out of every enclosing call.

Strong vs weak typing¶

Definition 6.2.5 (Trapped and untrapped errors; safety; strong and weak)

Following [Car96, §1]: an execution error is an operation applied outside its domain. It is trapped if execution stops immediately in a defined way (an exception, a trap, \(\mathsf{error}\)), and untrapped if execution continues with an arbitrary result (undefined behavior). A language is safe if no execution error is untrapped. We call a language strongly typed if it is safe and performs no implicit conversions between unrelated types, and weakly typed if it has untrapped errors (C: out-of-bounds writes, type punning through pointers) or silently converts values of one type into another to make an operation defined (JavaScript: "5" - 1 is 4, "5" + 1 is "51").

The two failure modes of weak typing are different: untrapped errors make a program's meaning undefined; silent conversions make it defined but surprising. Both defeat the purpose of the type distinction, which is to detect a mix-up.

Definition 6.2.6 (Coercion table of an operator)

For an operator \(\oplus\), its coercion table \(C_\oplus\) maps each pair of operand tags to either an operation on converted operands or \(\mathsf{error}\). A language is strict for \(\oplus\) if \(C_\oplus\) is \(\mathsf{error}\) on every pair of distinct tags. For JavaScript's +: \((\mathsf{number}, \mathsf{number}) \mapsto\) addition; any pair with a \(\mathsf{string}\) \(\mapsto\) convert both to strings and concatenate; \((\mathsf{boolean}, \mathsf{number}) \mapsto\) convert the boolean to \(0/1\) and add. Python's + is strict between numbers and strings; C's + accepts every pair of arithmetic types after the usual arithmetic conversions (Lesson 6.3) and pointer + integer.

Sound vs unsound type systems¶

Definition 6.2.7 (Soundness with respect to a set of errors)

Let \(W\) be a set of "wrong" outcomes (stuck states, or particular trapped errors such as TypeError). A static type system is sound for \(W\) if no well-typed program can produce an outcome in \(W\), and unsound for \(W\) if some well-typed program does. A system is intentionally unsound when its specification documents such programs and accepts them.

Algorithm 6.2.8 (The covariant-array store check)

Input: an array reference \(a\) whose static element type is \(S\), an index \(i\), a value \(v\) with static type \(S\).
Output: the store \(a[i] \gets v\), or the trapped error ArrayStoreException.
Precondition: every array object records its run-time element type \(R\), fixed at allocation; covariance allows \(R <: S\) (Lesson 6.5).
Postcondition: after a successful store, every element of the array is an instance of \(R\) (Proposition 6.2.11).
Invariant: each element of an array with run-time element type \(R\) is an instance of \(R\).

function ArrayStore(a, i, v):
    if i < 0 or i ≥ a.length: throw ArrayIndexOutOfBoundsException
    if v ≠ null and not (dynamicClass(v) <: a.runtimeElementType):
        throw ArrayStoreException             # JLS §10.5
    a.elements[i] ← v

3. Worked examples¶

The same mistake — a function that increments its argument, called with the string "41" on a path that runs only sometimes — placed on all three axes:

System	When is the mistake found?	What happens at run time?	Axis position
Pebble (`pebblec`)	statically: E0401 at the argument	never runs	static, strong, sound
Python 3.11	when the call executes	`TypeError` (trapped)	dynamic, strong
mypy 1.19.1 on the same Python	statically: `[arg-type]`	Python still runs it if you ignore mypy	static (optional), sound up to `Any` (Lesson 6.7)
JavaScript (node 22)	never	`"41" + 1` is `"411"`: a silent conversion	dynamic, weak
TypeScript 5.9 (`strict`)	statically, for this program	—	static, intentionally unsound elsewhere (§4)
C (clang 23)	a warning at best	pointer arithmetic on the string: garbage, possibly undefined behavior	static but weak

Static vs dynamic checking¶

Algorithm 6.2.4 on let inc = λx. x + 1 in if b then inc "41" else inc 41 with \(b = \mathsf{false}\): evaluation takes the else branch, inc 41 checks ⟨int, 41⟩ against int, and the result is ⟨int, 42⟩; the ill-typed call is never executed and no error is ever raised. With \(b = \mathsf{true}\) the + inside inc meets the tag \(\mathsf{str}\) and returns \(\mathsf{error}\) — inside inc, far from the mistaken call. A static checker (Figure 6.1.1 with a string type) rejects the program in both cases, at the argument.

Strong vs weak typing¶

JavaScript's coercion table for + and - on the five inputs of the box below:

expression	tags	rule of \(C_\oplus\)	result
`"5" + 1`	string, number	a string operand: concatenate	`"51"`
`"5" - 1`	string, number	`-` converts both to numbers	`4`
`"5" * "2"`	string, string	`*` converts both to numbers	`10`
`[] + {}`	object, object	both converted to primitive strings, concatenated	`"[object Object]"`
`true + 1`	boolean, number	`true` → `1`, add	`2`

Python's + has error for (str, int): the same "5" + 1 raises TypeError, a trapped error; "5" * 2 is defined (repetition), so strictness is per operator, not per language.

Sound vs unsound type systems¶

Covariant arrays, step by step (TypeScript and Java run the same program in the box):

step	statement	static types	run-time contents of the array
1	`dogs = [new Dog()]`	`dogs : Dog[]`	`[Dog]`
2	`animals = dogs`	`animals : Animal[]`, accepted because `Dog[] <: Animal[]`	the same array object
3	`animals.push(new Animal())` / `animals[0] = new Animal()`	an `Animal` into an `Animal[]`: well typed	TS: `[Dog, Animal]`; Java: `ArrayStoreException` (Algorithm 6.2.8)
4	`dogs[1].bark()`	`dogs[1] : Dog`: well typed	TS: `TypeError: dogs[1].bark is not a function`

In TypeScript step 4 is an error the type system promised to exclude (a method call on a value without that method): unsound. In Java step 3 traps, so the invariant "every element of a Dog[] is a Dog" is never broken and step 4 cannot go wrong: sound, at the price of a check on every array store.

4. Invariants and correctness¶

Static vs dynamic checking¶

Proposition 6.2.9 (Dynamic checking is safe)

Algorithm 6.2.4 never applies an operation to operands outside its domain: every run either diverges, returns a tagged value, or returns \(\mathsf{error}\).

Proof

By induction on the evaluation (on the depth of the recursion of Eval for terminating runs). The only operations with restricted domains are application (needs a closure), + and < (need integers) and if (needs a boolean). Each branch of Algorithm 6.2.4 that performs one of them first compares the operand's tag with the required one and returns \(\mathsf{error}\) on mismatch. Tags are correct by the invariant: every value is created with the tag of its form (n with int, λ with fun, …) and never modified, and variables hold only values produced by Eval. So every performed operation receives operands of its domain, and every mismatch is trapped.

Proposition 6.2.9 is safety without any static type system — Python and Scheme are safe. What static typing adds is Theorem 6.1.13's progress: no \(\mathsf{error}\) at all, found before running.

Strong vs weak typing¶

Proposition 6.2.10 (Implicit conversions hide type errors from dynamic checks)

If \(C_\oplus\) maps a pair of distinct tags \((t_1, t_2)\) to an operation instead of \(\mathsf{error}\), then a program that applies \(\oplus\) to a value of tag \(t_1\) where the programmer intended \(t_2\) produces no trapped error at that operation.

Proof

Immediate from Definition 6.2.6: the evaluation of \(\oplus\) consults \(C_\oplus(t_1, t_2)\), which by assumption is an operation, so evaluation continues with its result instead of raising \(\mathsf{error}\). The mix-up surfaces only later, if at all, when some strict operation meets the converted value — or never, as in "41" + 1 = "411".

Sound vs unsound type systems¶

Proposition 6.2.11 (Covariant mutable arrays: unsound without the store check, sound with it)

Assume subtyping \(\mathit{Dog} <: \mathit{Animal}\), covariant arrays (\(S <: T \Rightarrow S[\,] <: T[\,]\)), array reads typed by the static element type, and a method bark present on Dog only. (1) Without a store check, some well-typed program calls bark on an object without it. (2) With Algorithm 6.2.8 on every store, every array with run-time element type \(R\) contains only instances of \(R\) (or null), so a read through a static type \(S[\,]\) with \(R <: S\) yields an instance of \(S\).

Proof

(1) The program of §3 is well typed under the stated rules: step 2 by covariance, step 3 because Animal <: Animal, step 4 because dogs : Dog[] reads a Dog. Without a check, step 3 stores an Animal into an array whose other alias claims Dog elements, and step 4 calls bark on it. (2) By induction on the sequence of stores to an array \(a\) with run-time element type \(R\): initially \(a\) holds nulls or the initializer's elements, all instances of \(R\) (allocation checks them). A store passes Algorithm 6.2.8 only if the value is null or its dynamic class is a subtype of \(R\), which preserves the invariant; a failing store changes nothing. A read through a static type \(S[\,]\) is legal only if the array's static type is \(S[\,]\), and by the soundness of the static assignment rules (every array reference of static type \(S[\,]\) points to an array with run-time element type \(R <: S\) — Featherweight Java proves the analogous property for objects [IPW01]) the element is an instance of \(R <: S\).

What breaks the argument. Part (2) relies on arrays recording \(R\) at run time. Java generics are erased (Lesson 6.9), so a List<Dog> cannot check stores — which is why Java made generic types invariant (Lesson 6.5) instead of covariant.

5. Complexity¶

Technique	Time (worst)	Time (typical)	Space	Variables
Static checking	\(O(n)\) once, at compile time (Lesson 6.1 §5)	linear	\(O(n)\)	\(n\) program size
Dynamic tag checks	\(\Theta(k)\): one tag comparison per executed operation	1–2 instructions per operation; removed by JIT speculation	one tag per value	\(k\) operations executed
Covariant-array store check	\(\Theta(s \cdot h)\)	\(O(1)\) per store with class-hierarchy caching	none extra	\(s\) stores executed, \(h\) hierarchy depth
Implicit conversions (weak typing)	cost of the conversion per operation	a function call (`ToNumber`, `ToString`)	temporaries	—

Justification. Static checking visits each node once (Theorem 6.1.11). Algorithm 6.2.4 adds one comparison to each primitive operation it executes, so its overhead is proportional to the number \(k\) of executed operations, not to program size: a loop body run \(10^9\) times pays \(10^9\) checks. The store check walks the value's class hierarchy in the worst case (\(h\) superclasses) but HotSpot answers it with a cached "subtype check" in constant time for most stores.

Pathological family. The program \(\mathsf{loop}_k\) that adds two variables \(k\) times pays \(k\) tag checks under dynamic typing and none under static typing, so the static/dynamic cost ratio grows without bound in \(k\). Conversely, the static checker's cost is paid even for code that never runs.

Scale. JIT compilers (V8, HotSpot, PyPy) recover most of the dynamic cost by speculating on the tags they observe and compiling a check-free fast path guarded by one tag test, deoptimizing if the guess fails; the remaining costs of checking at boundaries between typed and untyped code are the subject of Lesson 6.7 (up to two orders of magnitude slowdowns in Typed Racket [TFGNVF16]).

Static vs dynamic checking¶

Optional (pluggable) typing (mypy, TypeScript, Python's annotations): a static checker that the language implementation ignores; programs run with dynamic checks only. Trade-off: gradual adoption, but the static guarantee is advisory (the §3 table).
Soft typing (Cartwright and Fagan 1991): insert dynamic checks only where static inference cannot prove an operation safe; a precursor of gradual typing (Lesson 6.7).
Hybrid type checking [PFPL, Ch. 23]: a static system with one dynamic type and casts; the principled form of "mostly static".

Strong vs weak typing¶

Checked conversions only (Rust, Swift, Pebble): every conversion is written (as), so the coercion table of every operator is strict (Lesson 6.3).
Sanitizers (Clang's -fsanitize=undefined,address): turn many of C's untrapped errors into trapped ones at run time, at 2× or more slowdown; C becomes "strong while you test".
Strict mode flags ("use strict" in JavaScript does not change +; TypeScript's strict rejects mixed operands statically): weak run-time semantics fenced by static rules.

Sound vs unsound type systems¶

Soundness restored by run-time checks (Java arrays, Dart 2's covariant generics with checked writes): keep the convenient rule and pay for a check.
Soundness restored by stricter rules (C# and Kotlin arrays/generics with declared variance, TypeScript's strictFunctionTypes, Lesson 6.5): reject the convenient programs.
Unsoundness by escape hatch only (Rust unsafe, Haskell unsafeCoerce, Lesson 6.1's box): the checked fragment is sound; soundness of the whole program is the programmer's obligation.

7. In real compilers¶

Static vs dynamic checking¶

CPython's binary_op implementation dispatches on the operands' types at every + and raises TypeError when no implementation accepts them: Algorithm 6.2.4 with Python's coercion rules. mypy [MYPY-Checker] is a separate, optional static checker over the same program.

The same mistake, checked late and early: Python 3.11 and mypy 1.19.1

Reproduce (Python 3.11.15, mypy 1.19.1 via uv):

mkdir -p py && cat > py/late.py <<'EOF'
def inc(x: int) -> int:
    return x + 1

def main(flag: bool) -> None:
    print(inc(41))
    if flag:
        print(inc("41"))   # a type error on a path that may never run

main(False)
main(True)
EOF
python3 py/late.py 2>&1 | sed "s|$PWD/||"; echo "exit status: ${PIPESTATUS[0]}"
uvx --from mypy==1.19.1 mypy py/late.py; echo "exit status: $?"

Output (complete):

42
42
Traceback (most recent call last):
  File "py/late.py", line 10, in <module>
    main(True)
  File "py/late.py", line 7, in main
    print(inc("41"))   # a type error on a path that may never run
          ^^^^^^^^^
  File "py/late.py", line 2, in inc
    return x + 1
           ~~^~~
TypeError: can only concatenate str (not "int") to str
exit status: 1
py/late.py:7: error: Argument 1 to "inc" has incompatible type "str"; expected "int"  [arg-type]
Found 1 error in 1 file (checked 1 source file)
exit status: 1

What to notice: main(False) runs cleanly — a dynamic checker only sees executed operations (§3). When the bad call finally runs, the trapped error (Proposition 6.2.9) is raised inside inc, at x + 1, not at the mistaken call. mypy reports the same mistake statically, at the argument, without running anything; Python itself ignores the annotations.

Strong vs weak typing¶

V8 implements JavaScript's + with the ToPrimitive/ToString/ToNumber conversions of the ECMAScript specification (the coercion table of Definition 6.2.6); Clang's -Wconversion family [CLANG-SemaChecking] warns about some of C's silent conversions but cannot make them illegal.

Weak and strong: node 22, Python 3.11 and clang 23 on mixed operands

Reproduce (node v22.22.2, Python 3.11.15, clang 23.1.2):

mkdir -p js py && cat > js/weak.js <<'EOF'
console.log("5" + 1, "5" - 1, "5" * "2", [] + {}, true + 1);
EOF
node js/weak.js
cat > py/strong.py <<'EOF'
print("5" * 2)
print("5" + 1)
EOF
python3 py/strong.py 2>&1 | sed -n '1p;$p'
cat > weak.c <<'EOF'
#include <stdio.h>
int main(void) {
  const char *s = "5";
  int n = 3.9;           /* silently truncated */
  unsigned u = -1;       /* silently wraps */
  printf("%s %d %u %d\n", s + 1, n, u, -1 < 1u);
  return 0;
}
EOF
clang-23 -std=c17 -Wall weak.c -o weak && ./weak

Output (complete):

51 4 10 [object Object] 2
55
TypeError: can only concatenate str (not "int") to str
weak.c:4:11: warning: implicit conversion from 'double' to 'int' changes value from 3.9 to 3 [-Wliteral-conversion]
    4 |   int n = 3.9;           /* silently truncated */
      |       ~   ^~~
1 warning generated.
 3 4294967295 0

What to notice: the first line is the coercion table of §3, column by column. Python printed 55 for "5" * 2 (repetition is defined), then "5" + 1 trapped: Python is strict for + on strings and numbers. C accepted everything: s + 1 is pointer arithmetic on the string (it prints the empty string after "5"), 3.9 became 3, -1 became 4294967295, and -1 < 1u is false because -1 is converted to unsigned (the usual arithmetic conversions of Lesson 6.3); only the literal truncation got a default warning.

Sound vs unsound type systems¶

TypeScript's isTypeRelatedTo [TSC-Checker] relates Dog[] to Animal[] covariantly by design; javac's Types.isSubtype [JAVAC-Types] does the same for arrays, and the JVM's aastore instruction performs Algorithm 6.2.8.

Covariant arrays: TypeScript 5.9 goes wrong, Java 21 traps

Reproduce (tsc 5.9.3 via npx, node v22.22.2, javac/java 21.0.10):

mkdir -p ts java && cat > ts/unsound.ts <<'EOF'
class Animal { name = "animal"; }
class Dog extends Animal { bark() { return "woof"; } }
const dogs: Dog[] = [new Dog()];
const animals: Animal[] = dogs;       // arrays are covariant: accepted
animals.push(new Animal());           // accepted: an Animal into an Animal[]
console.log(dogs[1].bark());          // well typed: dogs[1] is a Dog
EOF
npx -y -p typescript@5.9 tsc --strict --target es2020 --outDir ts/out ts/unsound.ts; echo "tsc exit status: $?"
node ts/out/unsound.js 2>&1 | head -5 | sed "s|$PWD/||"
cat > java/Covariant.java <<'EOF'
public class Covariant {
    static class Animal {}
    static class Dog extends Animal {}
    public static void main(String[] args) {
        Dog[] dogs = { new Dog() };
        Animal[] animals = dogs;          // Java arrays are covariant: accepted
        animals[0] = new Animal();        // checked at run time
        System.out.println("unreachable");
    }
}
EOF
javac -d java java/Covariant.java && java -cp java Covariant

Output (complete; the container prints a Picked up JAVA_TOOL_OPTIONS banner before Java's output, removed here):

tsc exit status: 0
ts/out/unsound.js:13
console.log(dogs[1].bark()); // well typed: dogs[1] is a Dog
                    ^

TypeError: dogs[1].bark is not a function
Exception in thread "main" java.lang.ArrayStoreException: Covariant$Animal
    at Covariant.main(Covariant.java:7)

What to notice: tsc accepts the program with --strict (exit status 0), and the compiled JavaScript then fails at step 4 of §3 with exactly the error the type system claims to prevent: unsound (Proposition 6.2.11(1)). Java accepts the same shape but its store check (Algorithm 6.2.8) traps at step 3, Covariant.java:7, so no Dog[] ever holds an Animal: sound, with a trapped error in place of a stuck state.

8. Comparison¶

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
Static checking	Rejects every program that could go wrong, and some that could not (Theorem 6.2.2)	\(O(n)\) at compile time · no run-time cost	Errors before running, at the offending subterm, on every path	Rules + checker (Lessons 6.3–6.4)	C, Java, Rust, Swift, Haskell, Pebble
Dynamic checking	Exact: only executed errors are reported (Proposition 6.2.9)	\(\Theta(k)\) tag checks at run time · JITs remove most	Errors only on executed paths, at the failing operation (often far from the mistake)	Tags on values, checks in every primitive	Python, JavaScript, Lisp, Ruby
Strong typing	No untrapped errors and no silent cross-type conversions	Checks at run time or compile time as above	Mix-ups become errors	Low once conversions are explicit	Python, Rust, Pebble
Weak typing	Untrapped errors or implicit conversions accepted (Proposition 6.2.10)	Conversions cost per operation; UB costs nothing until it bites	Mix-ups produce wrong values silently	Lowest for the language implementer	C (untrapped), JavaScript (conversions)
Sound type systems	The promise holds for all well-typed programs (Definition 6.2.7)	Sometimes needs run-time checks (Algorithm 6.2.8)	No surprises at run time for the excluded errors	Higher: every convenient rule must be justified	Java (modulo casts/arrays checks), Rust safe code, Haskell, Pebble
Intentionally unsound systems	Accepts documented programs that fail (TS arrays, method bivariance)	No checks needed	Occasional run-time type errors despite a clean compile	Lower; more JavaScript idioms type-check	TypeScript, Dart 1, Eiffel (catcalls)

Choose static and strong when the language compiles to native code and optimizations rely on types (Pebble, Rust); choose dynamic for exploratory scripting where the cost of annotations dominates. Choose soundness unless compatibility with an untyped ecosystem forces otherwise — and then document every hole, as TypeScript does, so that optimizers and programmers know which errors remain possible.

9. Assessment¶

Technique	Quiz ids	Drill	Flashcard tag	Exercises
Static vs dynamic checking	`static-dynamic-rice`, `dynamic-check-location`	— (the classification is conceptual; `progress-preservation` drills the formal side of "going wrong")	`static-dynamic`	—
Strong vs weak typing	`js-coercions`, `trapped-untrapped`	— (see the coercion tables of §3)	`strong-weak`	—
Sound vs unsound systems	`covariant-array-soundness`, `ts-unsound-features`	`progress-preservation`	`soundness`	—

A drill does not fit the first two techniques: their content is a classification of languages and run-time behaviors rather than a computation over a generated instance; the quiz questions ask you to place concrete programs on the axes.

References¶

See the chapter references.

Lesson 6.2 — Classifying type systems: static and dynamic, strong and weak, sound and unsound¶

1. Problem and motivation¶

Static vs dynamic checking¶

Strong vs weak typing¶

Sound vs unsound type systems¶

2. Definitions and algorithms¶

Static vs dynamic checking¶

Strong vs weak typing¶

Sound vs unsound type systems¶

3. Worked examples¶

Static vs dynamic checking¶

Strong vs weak typing¶

Sound vs unsound type systems¶

4. Invariants and correctness¶

Static vs dynamic checking¶

Strong vs weak typing¶

Sound vs unsound type systems¶

5. Complexity¶

6. Variants and refinements¶

Static vs dynamic checking¶

Strong vs weak typing¶

Sound vs unsound type systems¶

7. In real compilers¶

Static vs dynamic checking¶

Strong vs weak typing¶

Sound vs unsound type systems¶

8. Comparison¶

9. Assessment¶

References¶