principle-type-system-discipline

SKILL.md

Type System Discipline

The type checker is a proof assistant. Use it to eliminate impossible states, mismatched primitives, and unhandled variants at compile time. A case the types let you ignore becomes a runtime failure the compiler could have stopped. Prefer defining errors and special cases out of existence over proliferating handlers. Unrepresentable states, total functions, and interface redesign (the patterns below) are the tools.

Applies to any typed language. Skills like typescript-best-practices ground it in specific syntax.

The patterns:

Make illegal states unrepresentable. Model variants as sum types: discriminated unions in TypeScript, enums with payloads in Rust/Swift/Kotlin, sealed classes in Scala, ADTs in Haskell/OCaml. Don't model state as a bag of optional fields where contradictory combinations compile. A subtle anti-pattern: { completed: boolean; completedAt?: Date } admits completed: true; completedAt: undefined, which is meaningless. Derive the boolean from a single source like completedAt !== null, or model the variants explicitly as { kind: 'open' } | { kind: 'done'; at: Date }. If a bug forces the question "wait, can this combination actually happen?", the type is too loose.

Types are constructions, not restrictions. Build the type up from the values you want instead of carving them out of a looser type with checks. The invariant that seems to need a refinement type is usually a construction away. A non-empty list is a head plus a rest, not a list with a length check. A valid time range is a start plus a duration, not two timestamps you must keep ordered. No representation is privileged. A list of pairs is an even-length list if you interpret it that way, so choose the shape that cannot build the illegal value and expose the interface callers need on top.

Brand semantic primitives. UserId and OrderId are strings underneath but should not be interchangeable. Newtypes in Rust, opaque types in Swift, value classes in Kotlin, phantom types in Haskell, branded intersections in TypeScript. Validate once at creation, trust the type downstream.

External data is untyped until parsed. RPC payloads, JSON, IPC messages, CLI args, config files, environment variables, database rows. Have a parse function at every boundary that turns unstructured input into the typed model. See the boundary-discipline principle skill for where to put validation.

Don't lie to the type system. Casts, unsafe coercions, and assertion functions that bypass the compiler are latent runtime crashes. If the compiler can't prove a fact, prove it (validate, narrow, refine the model) or accept that the cast is a hazard.

Exhaustive matching is the compiler's job. When you match on a sum type, the compiler must fail compilation if a new variant is added without handling. Use the idiom your language provides: never-typed binding in TypeScript, unannotated match in Rust, -Wincomplete-patterns in Haskell, sealed-class match exhaustiveness in Kotlin.

Derive types from authoritative schemas. When a protocol buffer, OpenAPI spec, GraphQL schema, database migration, or design-system token file defines a shape, derive from it instead of hand-rolling a parallel type. See the encode-lessons-in-structure principle skill.

Strengthen a type only where partiality appears. A runtime assertion, null check, or "this should never happen" throw marks the place a type is too weak. Push that check up into the type. Then stop. The type system's job is to track the cases each use site must handle, not to describe the data as precisely as possible. Prefer total functions. sum of an empty list is 0, so it takes the plain list. head of an empty list has no answer, so it demands the non-empty one.

The tests: