principle-type-system-discipline

Compare original and translation side by side

🇺🇸

Original

English

🇨🇳

Translation

Chinese

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:

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

类型检查器（type checker）就是证明助手。在编译期使用它消除不可能的状态、不匹配的原语和未处理的变体。类型允许你忽略的每一种情况，都会演变成编译器本可提前阻止的运行时故障。与其不断增加处理器，不如从定义上让错误和特殊情况不复存在。无法表示的状态、全函数（total functions）和接口重设计（下方模式）就是实现这一点的工具。

它适用于任何有类型的语言。

typescript-best-practices

等 skill 会用具体语法将它落地。

这些模式：

让非法状态无法表示。 将变体建模为 sum type：TypeScript 中使用 discriminated union，Rust/Swift/Kotlin 中使用带 payload 的 enum，Scala 中使用 sealed class，Haskell/OCaml 中使用 ADT。不要将状态建模为一堆可选字段，因为这样相互矛盾的组合仍可编译。一个微妙的反模式是：
```
{ completed: boolean; completedAt?: Date }
```
允许出现
```
completed: true; completedAt: undefined
```
，而这是毫无意义的。应从
```
completedAt !== null
```
这样的单一来源派生布尔值，或者将变体显式建模为
```
{ kind: 'open' } | { kind: 'done'; at: Date }
```
。如果一个 bug 让你不得不问“等等，这种组合真的可能发生吗？”，那么这个类型就过于宽松了。
类型是构造出来的，而不是限制出来的。 从你希望允许的值出发构建类型，而不是先用一个更宽松的类型表示，再通过检查剔除不允许的值。看似需要 refinement type 的不变量，通常只需换一种构造方式即可避免。非空列表应由一个 head 加一个 rest 构成，而不是一个需要检查长度的列表。有效时间范围应由一个 start 加一个 duration 构成，而不是两个必须保持先后顺序的 timestamp。不存在天然更权威的表示方式。如果将一对值的列表解释为偶数长度列表，那么它就应当如此；因此，应选择无法构造非法值的形状，并对外暴露调用者所需的接口。
为语义原语添加品牌类型。
```
UserId
```
和
```
OrderId
```
底层都是 string，但不应互相替代。可以使用 Rust 中的 newtype、Swift 中的 opaque type、Kotlin 中的 value class、Haskell 中的 phantom type，以及 TypeScript 中的 branded intersection。创建时验证一次，之后便可以信任类型。
外部数据在解析之前都是未类型化的。 RPC payload、JSON、IPC message、CLI 参数、配置文件、环境变量和数据库行都属于此类。在每个边界设置 parse function，将非结构化输入转换为类型化模型。有关验证位置的安排，请参阅 boundary-discipline principle skill。
不要对类型系统撒谎。 casts、unsafe coercions 以及绕过编译器的 assertion function 都是潜在的运行时崩溃。如果编译器无法证明某个事实，就自行证明它（validate、narrow 或 refine model），否则就接受 cast 带来的风险。
穷尽匹配应该交给编译器。 对 sum type 进行 match 时，如果新增了变体却没有处理，编译器必须报告编译失败。使用各语言提供的惯用机制：TypeScript 中采用
```
never
```
类型绑定，Rust 中采用未标注的
```
match
```
，Haskell 中采用
```
-Wincomplete-patterns
```
，Kotlin 中利用 sealed class 的 match exhaustiveness。
从权威 schema 派生类型。 当 protocol buffer、OpenAPI spec、GraphQL schema、database migration 或 design-system token file 定义了某种结构时，应从中派生类型，而不是手工维护一套平行类型。请参阅 encode-lessons-in-structure principle skill。
仅在出现部分定义（partiality）的位置加强类型。 运行时 assertion、null check，或抛出“this should never happen”异常的地方，都表明类型过于宽松。将该检查上移到类型中，然后停止继续收紧。类型系统的职责是跟踪每个使用点必须处理的情况，而不是尽可能精确地描述数据。优先使用 total function。空列表的
```
sum
```
为 0，因此它可以接受普通列表；空列表的
```
head
```
没有答案，因此它要求非空列表。

这些测试：

“我能否写一条注释来解释这组字段何时才有效？”如果可以，那么这个类型就过于宽松，应将其拆成 sum type。
“我的两个函数参数是否使用了相同的 primitive type，却表示不同的含义？”为它们添加品牌类型。
“这些
```
any
```
、
```
as
```
和
```
assertNotNull
```
最初从哪里来？”追溯到边界并在那里进行验证。
“如果下个月新增一个变体，编译器会告诉下一个 Agent 在哪里补上对应分支吗？”如果不会，说明匹配并不穷尽。
“这个类型是否重复定义了另一个文件所拥有的结构？”应改为派生类型。
“我加强这个类型是为了让操作保持 total，还是仅仅为了提高精确度？”如果原本不会发生 panic，就保留普通类型。