Type-driven development
Contract
| Field |
Bound contract |
| Trigger |
The work is modeling a domain, encoding a state machine, hardening an API boundary, making invalid states unrepresentable, or parsing instead of validating. |
| Authority |
Reversible local: writes only domain types, public signatures, and affected callers and tests; rollback is version control or undo. No remote mutation. |
| Side effect |
Rewrites domain types, public signatures, and affected callers and tests to the new algebraic model. |
| Done |
Invalid states are unconstructible, matches are exhaustive, boundaries parse, and no scattered post-hoc validation remains. |
Inputs
Required: the domain problem, data model, or API surface to encode.
Optional: existing types or callers to refactor.
Refusals
- Will not add runtime guards to fix a type-design failure: fix the type design.
- Will not add a wildcard arm to silence a non-exhaustive match: add the missing variant.
- Will not proceed with type holes or incomplete bodies.
- Will not use this approach when the language lacks ADTs, sealed hierarchies, or equivalent sum-type support: skip and report.
Procedure
- Plan. State the domain in one paragraph. List all valid states, all invalid states, and every operation with its preconditions and postconditions. If any operation is partial, mark it as such. Done when: the domain is stated with valid states, invalid states, and operations listed.
- Design types first. For each invalid state, write a type that the compiler prevents. Use ADTs, phantom types, branded types, newtype wrappers, sealed hierarchies, or opaque types, whichever the language supports. Do not write implementation bodies until all types compile. Done when: all types compile and every invalid state is unrepresentable.
- Parse at boundaries. For every untrusted input (external data, deserialization, FFI, user input), write a
parse constructor that returns the new type. Do not return bool and defer validity to callers. Done when: every untrusted input boundary has a parse function returning the new type.
- Exhaustive matching. Encode state machine transitions as exhaustive
match/switch/visit on the sum type. Compiler warnings on incomplete arms are failures. Done when: every state-machine transition is an exhaustive match with no wildcard arms.
- Verify. Run the language's strict type checker and exhaustiveness check. Fix the type design, not the implementation, when the checker reports an illegal state is representable. Done when: the type checker and exhaustiveness check pass.
- Build. Run the full target build. Implement the bodies guided by the types. Done when: the target build passes.
Failure and recovery
| Failure class |
Behavior |
| Unsupported language |
If the language lacks ADTs, sealed hierarchies, or equivalent sum-type support, skip this approach and report. |
| Type checker failure |
Block. Fix the type design until the invalid state is unrepresentable. Do not add runtime guards. |
| Non-exhaustive match |
Compile-time failure. Add the missing variant to the type, not a wildcard arm. |
| Invalid state remains representable |
Block. The type design is insufficient; iterate until the compiler enforces the invariant. |
| Type holes remain |
Block. Complete all incomplete bodies or remove the holes before proceeding. |
| Build fails |
Block. Resolve implementation errors until the target build passes. |
Output
A domain type system where every algebraic constructor is present, every boundary has a parse function returning the new type, every state-machine variant is matched exhaustively, and no runtime validation scattered outside the parse layer remains.
1---2name: type-driven3description: Use when modeling a domain, encoding a state machine, hardening APIs, making invalid states unrepresentable, or parsing instead of validating. Not for TypeScript: use typescript-best-practices.4---56# Type-driven development78## Contract910| Field | Bound contract |11|---|---|12| Trigger | The work is modeling a domain, encoding a state machine, hardening an API boundary, making invalid states unrepresentable, or parsing instead of validating. |13| Authority | Reversible local: writes only domain types, public signatures, and affected callers and tests; rollback is version control or undo. No remote mutation. |14| Side effect | Rewrites domain types, public signatures, and affected callers and tests to the new algebraic model. |15| Done | Invalid states are unconstructible, matches are exhaustive, boundaries parse, and no scattered post-hoc validation remains. |1617## Inputs1819Required: the domain problem, data model, or API surface to encode.20Optional: existing types or callers to refactor.2122## Refusals2324- Will not add runtime guards to fix a type-design failure: fix the type design.25- Will not add a wildcard arm to silence a non-exhaustive match: add the missing variant.26- Will not proceed with type holes or incomplete bodies.27- Will not use this approach when the language lacks ADTs, sealed hierarchies, or equivalent sum-type support: skip and report.2829## Procedure30311. **Plan.** State the domain in one paragraph. List all valid states, all invalid states, and every operation with its preconditions and postconditions. If any operation is partial, mark it as such. **Done when:** the domain is stated with valid states, invalid states, and operations listed.322. **Design types first.** For each invalid state, write a type that the compiler prevents. Use ADTs, phantom types, branded types, newtype wrappers, sealed hierarchies, or opaque types, whichever the language supports. Do not write implementation bodies until all types compile. **Done when:** all types compile and every invalid state is unrepresentable.333. **Parse at boundaries.** For every untrusted input (external data, deserialization, FFI, user input), write a `parse` constructor that returns the new type. Do not return `bool` and defer validity to callers. **Done when:** every untrusted input boundary has a parse function returning the new type.344. **Exhaustive matching.** Encode state machine transitions as exhaustive `match`/`switch`/`visit` on the sum type. Compiler warnings on incomplete arms are failures. **Done when:** every state-machine transition is an exhaustive match with no wildcard arms.355. **Verify.** Run the language's strict type checker and exhaustiveness check. Fix the type design, not the implementation, when the checker reports an illegal state is representable. **Done when:** the type checker and exhaustiveness check pass.366. **Build.** Run the full target build. Implement the bodies guided by the types. **Done when:** the target build passes.3738## Failure and recovery3940| Failure class | Behavior |41|---|---|42| Unsupported language | If the language lacks ADTs, sealed hierarchies, or equivalent sum-type support, skip this approach and report. |43| Type checker failure | Block. Fix the type design until the invalid state is unrepresentable. Do not add runtime guards. |44| Non-exhaustive match | Compile-time failure. Add the missing variant to the type, not a wildcard arm. |45| Invalid state remains representable | Block. The type design is insufficient; iterate until the compiler enforces the invariant. |46| Type holes remain | Block. Complete all incomplete bodies or remove the holes before proceeding. |47| Build fails | Block. Resolve implementation errors until the target build passes. |4849## Output5051A domain type system where every algebraic constructor is present, every boundary has a parse function returning the new type, every state-machine variant is matched exhaustively, and no runtime validation scattered outside the parse layer remains.
OutlineDriven