Type-Level Encoding of Invariants¶

Types can encode not just "what kind of data" but "what properties it has" - using the type system to make violations compile-time errors rather than runtime bugs.

Tension Addressed¶

Safety vs. Flexibility; Expressiveness vs. Simplicity

Recognizable As¶

"Newtype" patterns (wrapping primitives to distinguish semantically different values); state machine states as types; units of measure; non-empty collections as distinct types; capability types

Canonical Sources¶

Wadler, "Theorems for Free!" (1989); Kennedy, "Types for Units-of-Measure" (1997); Kiselyov, "Strongly Typed Heterogeneous Collections" (2004)

Transfers To¶

Schema design (encoding constraints in structure), API design (builder pattern with required steps), any domain where compile-time enforcement is preferable to runtime checking

This represents the advanced application of "making illegal states unrepresentable." Instead of validating at runtime that an email is valid, the type system ensures you can only have an "Email" type if validation succeeded. The pattern enables "parse, don't validate" - validating once at boundaries and relying on types thereafter.