Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

principle-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.

适用于任何有类型的语言。像 typescript-best-practices 这类 skill 把它落到具体语法。

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.

  • 让非法状态不可表示。 用 sum type 建模变体:TypeScript 的 discriminated union,Rust/Swift/Kotlin 带载荷的 enum,Scala sealed class,Haskell/OCaml ADT。别用一袋 optional 字段建模状态,让矛盾组合也能编译。微妙反模式:{ completed: boolean; completedAt?: Date } 允许 completed: true; completedAt: undefined,毫无意义。从单一来源推导布尔,如 completedAt !== null,或显式建模 { kind: 'open' } | { kind: 'done'; at: Date }。若 bug 逼你问「等等,这组合真会发生吗?」,类型就太松。

  • 类型是构造,不是限制。 从想要的值往上建类型,别用检查从更松的类型里剜。看似需要 refinement type 的不变量,通常差一次构造。非空列表是 head + rest,不是带长度检查的列表。合法时间范围是 start + duration,不是必须保持有序的两个时间戳。没有哪种表示享特权。把成对列表解释成偶长列表也可以,所以选无法构造非法值的形状,再在上面暴露调用方需要的接口。

  • 给语义原语 branding。 UserId 与 OrderId 底层是字符串,但不应互换。Rust newtype、Swift opaque、Kotlin value class、Haskell phantom、TypeScript branded intersection。创建时校验一次,下游信任类型。

  • 外部数据在解析前无类型。 RPC 载荷、JSON、IPC、CLI 参数、配置、环境变量、数据库行。每个边界有个 parse,把非结构化输入变成类型化模型。校验放哪见 boundary-discipline principle skill。

  • 别对类型系统撒谎。 绕过编译器的 cast、不安全强制、断言函数是潜伏的运行时崩溃。编译器证不了就证明它(校验、收窄、 refining 模型),或承认 cast 是风险。

  • 穷尽匹配是编译器的活。 对 sum type 匹配时,新变体未处理必须让编译失败。用语言惯用写法:TypeScript 的 never 绑定、Rust 无注解 match、Haskell -Wincomplete-patterns、Kotlin sealed class 穷尽匹配。

  • 从权威 schema 派生类型。 protobuf、OpenAPI、GraphQL schema、数据库 migration、设计系统 token 文件定义了形状时,从它派生,别手搓平行类型。见 encode-lessons-in-structure。

  • 只在出现偏函数的地方加强类型。 运行时断言、null 检查、「这绝不该发生」的 throw,标记类型太弱的地方。把检查推到类型里。然后停。类型系统的工作是追踪每个使用点必须处理的情况,不是尽可能精确描述数据。优先全函数。空列表的 sum 是 0,所以吃普通列表;空列表的 head 没答案,所以要求非空。

The tests:

自检:

  • “Can I write a comment explaining when this combination of fields is valid?” If yes, the type is too loose. Split it into a sum type.

  • “Do two of my function arguments share a primitive type but mean different things?” Brand them.

  • “Where did this any, this as, this assertNotNull come from?” Trace it to the boundary and validate there instead.

  • “If a new variant is added next month, will the compiler tell the next agent where to add a case?” If no, the match isn’t exhaustive.

  • “Is this type duplicating a shape another file owns?” Derive instead.

  • “Am I strengthening this type to keep an operation total, or just to be more precise?” If nothing would otherwise panic, keep the plain type.

  • 「我能写注释说明这组字段何时合法吗?」能,类型就太松。拆成 sum type。

  • 「两个函数参数共享原语类型但含义不同吗?」给它们 branding。

  • 「这个 any、as、assertNotNull 从哪来?」追到边界,在那里校验。

  • 「下月加新变体,编译器会告诉下一个 agent 在哪加 case 吗?」不会,匹配就不穷尽。

  • 「这类型在复制另一文件拥有的形状吗?」改成派生。

  • 「我加强类型是为了让操作保持全,还是只为更精确?」否则不会 panic,就留普通类型。