ADR-0004 deferred exhaustiveness and disjointness markers (sealed, abstract) "until a second model needs them". This is a report that a second model needs them.
The use case
A model of a software-development methodology: the artifacts a team's process produces, and how they relate. One entity is a Commitment — a decision an agent must not re-make — which is exactly one of two kinds:
- Invariant — a property of the artifact, mechanically checkable. For example "dependencies point inward only", enforced by an import-graph test plus a linter allowlist.
- Practice — a behavioural or process rule that no test can check. For example "never edit a test to make it pass", or "rebase, never merge". Enforceable by a hook or a review step, or not at all.
subtypeOf (thank you, #8/#21) expresses the hierarchy, and having the parent's invariants cover both children is exactly right. Two things it cannot say:
- Exhaustive. Invariant and Practice are the complete enumeration. Nothing stops a bare
Commitment that is neither.
- Abstract. A
Commitment should never be instantiated directly; every one is an Invariant or a Practice.
Why it bites this model specifically
The whole point of the split is that each kind gets a different enforcement path: an Invariant must have a mechanical enforcement, a Practice may not be able to have one. An unclassified Commitment is precisely the thing that escapes both rules, so the classification being provably complete is load-bearing rather than decorative.
Without a marker, the model's own prose has to carry the claim, which is the situation ADR-0004 describes for the is-a link before subtypeOf existed: "the is-a claim lived only in definition prose, so the hierarchy was invisible to the renderer... and the linter could not check the enumeration."
What would help
Whatever shape you prefer, the checks we would want are:
- an
abstract: true parent errors (or warns) if anything references it as a concrete instance;
- a
sealed: true parent renders its children as a closed enumeration, so a reader and an agent both know the list is complete.
Rendering suggestion: the Markdown hierarchy section already lists a parent's subtypes; a closed list could simply say so.
Related: #6 (flag invariants not covered by a test) is the same shape of check one level down, and the two compose well for this model.
🤖 Filed by Claude Code on behalf of a modelith user, from a real modelling session that hit this gap.
ADR-0004 deferred exhaustiveness and disjointness markers (
sealed,abstract) "until a second model needs them". This is a report that a second model needs them.The use case
A model of a software-development methodology: the artifacts a team's process produces, and how they relate. One entity is a Commitment — a decision an agent must not re-make — which is exactly one of two kinds:
subtypeOf(thank you, #8/#21) expresses the hierarchy, and having the parent's invariants cover both children is exactly right. Two things it cannot say:Commitmentthat is neither.Commitmentshould never be instantiated directly; every one is an Invariant or a Practice.Why it bites this model specifically
The whole point of the split is that each kind gets a different enforcement path: an Invariant must have a mechanical enforcement, a Practice may not be able to have one. An unclassified
Commitmentis precisely the thing that escapes both rules, so the classification being provably complete is load-bearing rather than decorative.Without a marker, the model's own prose has to carry the claim, which is the situation ADR-0004 describes for the is-a link before
subtypeOfexisted: "the is-a claim lived only in definition prose, so the hierarchy was invisible to the renderer... and the linter could not check the enumeration."What would help
Whatever shape you prefer, the checks we would want are:
abstract: trueparent errors (or warns) if anything references it as a concrete instance;sealed: trueparent renders its children as a closed enumeration, so a reader and an agent both know the list is complete.Rendering suggestion: the Markdown hierarchy section already lists a parent's subtypes; a closed list could simply say so.
Related: #6 (flag invariants not covered by a test) is the same shape of check one level down, and the two compose well for this model.
🤖 Filed by Claude Code on behalf of a modelith user, from a real modelling session that hit this gap.