01 — Why Static Types

A type system is a lightweight formal method that proves a class of runtime errors cannot occur — without running the program. The guarantees it provides depend on how expressive the type language is.

The cost of untyped code

In cp-03/cp-04, MiniLang is fully dynamic: every value carries its type at runtime (std::variant<nil, double, bool, string, FnValue>). A type error like "hello" + 42 raises a RuntimeError when the + operator tries to add a string and a number. This is correct, but:

  • The error appears at runtime, not compile time.
  • It may appear on a rarely-executed code path — you might not see it until production.
  • Error messages say "expected number" without knowing the programmer's intent.

What the type checker provides

The type checker runs after parsing and before execution. It annotates every expression with a type (Num, Bool, Str, Nil, Fn<...>) and reports mismatches statically:

let x: Num = "hello";  // error at line 1: expected Num, got Str

This moves the failure from runtime to compile time.

MiniLang's type language

Type ::= Num | Bool | Str | Nil | Any
       | Fn(Type, ...) -> Type
  • Num, Bool, Str, Nil — the four base types from the value set.
  • Any — the gradual escape hatch (step 06). A value of type Any can be used anywhere without a static error; correctness is checked at runtime.
  • Fn(T1, T2, ...) -> R — a function type.

Soundness vs completeness

A type system is sound if every accepted program is safe at runtime. A type system is complete if it accepts every safe program.

No practical type system is both sound and complete (undecidability). The trade-off is:

  • Reject false positives (be unsound) → miss bugs.
  • Reject true negatives (be incomplete) → reject correct programs.

MiniLang's checker is sound for the base types: a program that passes type-checking with no Any types will not produce a type error at runtime. The Any type trades soundness for usability on the parts of the program that can't be typed statically.

Checked vs unchecked features

In cp-05, the following are statically checked:

  • Arithmetic (+, -, *, /) requires Num operands.
  • Comparison (<, <=, etc.) requires Num or Str operands.
  • Logical (and, or) requires Bool operands.
  • Negation ! requires Bool; unary - requires Num.
  • Function call arity is checked against the declared parameter count.
  • Function return type must match the declared return type (if annotated).
  • let/var type annotations must match the initialiser.

The following are not statically checked in cp-05:

  • Array element types (no array type in the type language).
  • Object field access (no class types yet).

These are left for extensions.