FREE LESSON · Languages & compilers · 2 OF 4
Static vs Dynamic Typing Explained
Types make impossible states harder to express — Static constraints and runtime meaning
A type system classifies values and permitted operations.
Static checking rejects some programs before execution; dynamic checking attaches decisions to runtime values. Rich types can encode variants, ownership, nullability, effects, or units. No practical type system proves every desirable property, and unsafe escape hatches or external data reintroduce obligations.
Types are a proof language with a deliberately limited theorem set.
A tagged union makes variants explicit
Instead of a nullable result with side-channel error codes, define Success(value) or Failure(reason). Pattern matching then requires each variant to be handled, and the payload appropriate to one variant is unavailable in the other. The representation moves a runtime convention into a checkable structure.
A good type captures a real invariant and makes violations inconvenient or impossible.