From 64f4e6772eb0e9cf93e6fc1a4202592669661fb5 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 5 Jul 2026 07:58:07 +0000 Subject: [PATCH] docs(P-010): restructure Own.Types around the five-pillar taxonomy MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reorganize the type-disciplines proposal under semantic primitives, algebraic domain modeling, state/lifetime discipline, tooling, and future — adding discriminated unions/exhaustive matching/Option/Result (previously undocumented anywhere in the repo), strongly typed IDs, ValueTask/single-use constraints, and an elaborated tooling section (source generators, code fixes, generated docs, OwnIR facts). Existing typestate/ownership items are cross-referenced to P-004/005/006/007 instead of duplicated, and a diagnostic-prefix open question (`TYP0xx` vs `[type: …]` tag) is recorded against the DI/EFF/OBL precedent. Co-Authored-By: Claude Sonnet 5 Claude-Session: https://claude.ai/code/session_019ChcHzqtYRaVGiHmL2dCQ8 --- docs/proposals/P-010-type-disciplines.md | 256 ++++++++++++++++++++--- 1 file changed, 231 insertions(+), 25 deletions(-) diff --git a/docs/proposals/P-010-type-disciplines.md b/docs/proposals/P-010-type-disciplines.md index 9e880aeb..63e8cbde 100644 --- a/docs/proposals/P-010-type-disciplines.md +++ b/docs/proposals/P-010-type-disciplines.md @@ -2,13 +2,18 @@ - **Status:** draft (horizon) - **Depends on:** `spec/OwnCore.md` (the ownership/affine core and its fact - vocabulary), `spec/Lifetimes.md`; relates to P-006 (capability/lifetime — where - branded `resource`/capability types are held), P-008 (effects — the `use !Db` - half of a signature), and P-005 (IDisposable typestate — the first concrete - protocol). See `docs/ROADMAP.md` for where this sits in the strategy. + vocabulary), `spec/Lifetimes.md`; relates to P-005 (`IDisposable` typestate — + the first concrete protocol), P-006 (DI lifetimes — a region contract, not a + protocol), P-007 (ArrayPool/Span borrow-view — the pooled-buffer instance), + P-008 (effects — the `use !Db` half of a signature), and P-017 (multi-stack + frontends — where `Own.Types` facts travel beyond C#). See `docs/ROADMAP.md` + for where this sits in the strategy. ## Motivation +> **Own.Types is not trying to make C# pretty. Own.Types makes domain lies +> mechanically harder to write.** + The guiding heuristic: types aren't only about the *shape* of data (`string`/`int`/`User`). They can encode validity, access rights, state, dimension, order of operations, effects, protocol, ownership, even proofs. If a @@ -24,25 +29,66 @@ not `DeclarationId`, even though both are `string`) and **what STATE it is in** make everything `string` / `int` / `Guid` / `Dictionary` — is not flexibility. It is homeless JSON pretending to be architecture. -`Own.Types` adds those two dimensions as an **external static-contract layer** -over existing C#: an analyzer / source generator / `.own` spec that checks the +`Own.Types` adds those dimensions as an **external static-contract layer** over +existing C#: an analyzer / source generator / `.own` spec that checks the discipline, without rewriting the code into a new language. This is the move that turns Own.NET from "a borrow checker for C#" into "an external static contract layer for C#/.NET that adds ownership, typestate, effects, capabilities, and domain types" — while the DSL stays a spec/model/contract language and pointedly refuses to become a second C# people write business logic in. +## Map of the five pillars + +```text +Own.Types +├─ Semantic primitives — what a value MEANS +│ ├─ newtype / branded types +│ ├─ constrained (refinement) types +│ ├─ units / quantities +│ └─ strongly typed IDs +│ +├─ Algebraic domain modeling — what a value CAN BE +│ ├─ discriminated unions +│ ├─ exhaustive matching +│ ├─ Option +│ └─ Result / error unions +│ +├─ State/lifetime discipline — what STATE a value is in +│ ├─ typestate +│ ├─ owned/borrowed/must-dispose +│ ├─ event subscription lifetime +│ ├─ pooled buffer lifecycle +│ └─ ValueTask/single-use constraints +│ +├─ Tooling — how the discipline is enforced +│ ├─ source generators +│ ├─ Roslyn analyzers +│ ├─ code fixes +│ ├─ generated docs +│ └─ OwnIR facts +│ +└─ Future — horizon, not committed + ├─ .own DSL + ├─ F# generator/backend + ├─ interop analyzers + └─ multi-language frontends +``` + +The first four pillars share one restraint: brands, refinements, units, unions, +and protocols all lower to plain structs/records plus smart constructors — the +*discipline* is enforced by analyzer, not by a second type checker that could +drift from the affine core (the project's standing meta-irony). + ## Scope -The four most-applied disciplines, in priority order. Each has a `.own` -declaration and a checked C# imitation; none requires a runtime. +### 1. Semantic primitives — what a value means 1. **Branded / opaque types.** Distinguish `ProductId`, `DeclarationId`, `Email` though all are `string` underneath, so `GetProduct(declarationId)` is a diagnostic, not a 2 a.m. incident. DSL: `brand ProductId : string;`. C#: `[OwnBrand("ProductId")]` on a `readonly record struct` plus a smart constructor; the analyzer enforces that the wrapped value only enters through - it. (Mechanically these are phantom types — see the catalog.) + it. (Mechanically these are phantom types — see the deferred catalog.) 2. **Refinement types** — "int, but valid": `refinement Port : int where value >= 1 && value <= 65535;`, @@ -58,8 +104,55 @@ declaration and a checked C# imitation; none requires a runtime. tax rates, and physical quantities — the domains where a silent unit mix-up is a financial bug, not a rounding one. -4. **Typestate / protocols.** Encode object state in the type so methods can only - be called in a valid order: +4. **Strongly typed IDs.** Not a new mechanism — the single most-applied + *instance* of branded types, called out because it is the pattern developers + reach for first: `brand OrderId : Guid; brand CustomerId : Guid;` so + `GetOrder(customerId)` is caught even though both brands share the same + underlying `Guid`. The analyzer's job here is narrower than general branding: + catch **argument-order transposition** at call sites where two branded IDs of + the same underlying type are adjacent parameters — the concrete bug this + pillar exists to kill. + +### 2. Algebraic domain modeling — what a value can be + +5. **Discriminated unions.** A closed set of shapes a value can take: + `union Shape { Circle(radius: float); Rect(w: float, h: float); }`. Lowers to + a sealed hierarchy (or a source-generated closed struct union) that cannot be + extended from outside the declaration — the analyzer, not `sealed` alone, + enforces closedness across partial classes and other-assembly subclassing + attempts. + +6. **Exhaustive matching.** C#'s `switch` over a non-`enum` type has no + exhaustiveness check at all, and even enum switches only get an ignorable + `CS8509` warning. Own.Types promotes this to a hard diagnostic tied to the + `union` declaration: every `switch`/pattern match over a branded union must + cover every case or an explicit `default`/discard, and a new case added to + the union must break every non-exhaustive match site at compile time, not at + 3 a.m. in production. + +7. **`Option`.** Replaces the gap nullable reference types leave open (nothing + stops a `string?` from silently meaning "not yet loaded" *and* "deliberately + absent" *and* "error", all at once). `Option` is a two-state union + (`Some`/`None`); the analyzer flags unmatched `.Value` access the same way it + flags a non-exhaustive union match — this pillar is a specialization of #6, + not a separate mechanism. + +8. **`Result` / error unions.** `Result` as the alternative to + exceptions-as-control-flow for expected failure. Two enforcement angles: (a) + the exhaustiveness rule from #6 — a `Result` must be matched on both `Ok` and + `Error`, not just unwrapped; (b) an "unobserved result" diagnostic, structurally + the same shape as an unawaited `Task` — a `Result` that is constructed and + never matched or propagated is silently swallowed failure. + +Pillar 2's four items are one mechanism wearing three hats: a closed-shape +declaration plus an exhaustiveness check. `Option` and `Result` are simply the +one- and two-error-case unions developers reach for constantly enough to name +directly, rather than making every call site spell out a bespoke `union`. + +### 3. State/lifetime discipline — what state a value is in + +9. **Typestate / protocols.** Encode object state in the type so methods can + only be called in a valid order: ```text protocol Report { @@ -78,12 +171,83 @@ declaration and a checked C# imitation; none requires a runtime. Typestate is also the generalization that subsumes **session types** (typed message-ordering protocols) as the special case where the object is a channel. -The combined picture — domain types, refinements, resources, protocol state, and -effects in one signature set: +10. **Owned / borrowed / must-dispose.** Already built as a standalone + diagnostic in [P-005](P-005-idisposable-ownership.md) — Own.NET already + treats `IDisposable` as typestate C# lacks. This pillar's job is *not* to + duplicate P-005's checker; it is to surface the same ownership verdict as a + **type-level marker** in the signature a developer reads (`Owned`, + `Borrowed`, `[OwnMustDispose]`) so the discipline is visible at the call + site, not only in an analyzer squiggle. + +11. **Event subscription lifetime.** Already covered as a resource-lifetime + profile in P-004 (WPF) and P-006 (DI lifetime, where a subscription is one + captive-dependency shape). Own.Types' angle: a typed subscription handle + that is itself a two-state protocol (`Active -> Disposed`, unsubscribe + consumes self), so double-unsubscribe and use-after-unsubscribe fall out of + the same typestate mechanism as #9, instead of a bespoke `SUB0xx` rule. + +12. **Pooled buffer lifecycle.** Already covered in + [P-007](P-007-arraypool-span.md) (ArrayPool/Span borrow-view). Own.Types' + angle: model a rented buffer as `Buffer` — a two-state + protocol exactly like #9 — so "view survives `Return`" is reported through + the general typestate/use-after-move path rather than a parallel + pool-specific engine. + +13. **`ValueTask`/single-use constraints.** A well-known .NET footgun: + `ValueTask` must be awaited (or converted) exactly once, and never both + stored and awaited. Structurally this is a **single-transition protocol** + (`Pending -> Awaited`; awaiting twice, or awaiting after `.AsTask()`, is + use-after-move) — the same affine "consume once" mechanism as #9, applied to + a BCL type Own.NET does not own and cannot annotate at the source, so the + marker has to live at the call site (`[OwnSingleUse]` on the + producing member, or an analyzer-only rule with no DSL declaration). + +Pillars 10–13 are **not** new checkers to build — they are existing or +near-existing lifetime facts (P-004/005/006/007) reframed as instances of the +two general Own.Types mechanisms (ownership marker, typestate protocol). The +payoff of doing this pillar at all is *unification*: one mental model +(protocol state, consume-on-transition) instead of four bespoke rule families. + +### 4. Tooling — how the discipline is enforced + +14. **Source generators.** Emit the boilerplate a brand/refinement/union + declaration implies — smart constructors, equality, `ToString`, exhaustive + `Match`/`Switch` helper methods — so the discipline costs one declaration, + not hand-written ceremony per type. + +15. **Roslyn analyzers.** The enforcement side for every pillar above: brand- + boundary violations (#1), predicate bypass (#2), unit mismatch (#3), + non-exhaustive match (#6), unobserved `Result` (#8), invalid protocol + transition / use-after-transition (#9, #11–#13). + +16. **Code fixes.** A matching quick-fix per analyzer: insert the missing + `switch` arm stub for a non-exhaustive match, wrap a raw literal in its + brand's smart constructor, insert the missing `Dispose`/transition call. + Diagnostics without a code fix push the discipline back onto the developer + manually re-deriving the fix; that is the gap this item exists to close. + +17. **Generated docs.** Render the `.own` declarations (brand / refinement / + union / protocol) into human-readable reference pages, the same way + `spec/Diagnostics.md` is the single source of truth for `OWN` codes today — + one declaration, read by the compiler *and* the wiki, so the contract and + its documentation cannot drift apart. + +18. **OwnIR facts.** The seam every pillar above lowers through: new OwnIR fact + kinds (`brand`, `refinement`, `union`, `protocol-state`) alongside the + existing resource/ownership facts in `spec/OwnIR.md`, so any frontend — + today's Roslyn C# extractor, tomorrow's OwnTS/OwnJava/OwnKotlin (P-017) — + emits and consumes the same domain-type vocabulary without re-deriving it + per language. + +The combined picture — domain types, refinements, unions, resources, protocol +state, and effects in one signature set: ```text brand ProductId : string; +brand OrderId : Guid; brand CustomerId : Guid; refinement NonEmptyString : string where !String.IsNullOrWhiteSpace(value); +unit usd; +union PaymentResult { Approved(txId: string); Declined(reason: string); } resource Db; resource ArrayPool; protocol Report { @@ -95,9 +259,33 @@ protocol Report { fn CalculateTotal(order: Order) -> Money pure; fn LoadOrder(id: ProductId) -> Order use Db; +fn Charge(customer: CustomerId, amount: usd) -> PaymentResult use Db; fn RenderReport(report: Report) -> File use !ArrayPool, !Log; ``` +## Future (horizon, not committed) + +Distinct from the deferred catalog below: these are things Own.Types plausibly +grows *into*, not type-theory tempo it is refusing. + +- **`.own` DSL.** Today's brand/refinement/union/protocol snippets are sketch + syntax inside this proposal, not a ratified grammar. Graduating this pillar + means these constructs get a real entry in `spec/Grammar.md`, with the same + test-pinned discipline as every other DSL construct. +- **F# generator/backend.** F#'s discriminated unions, units of measure, and + records are a structural match for pillars 1–2 — a codegen backend that lowers + `.own` declarations to *idiomatic F#* (real DUs, real `[]`) instead of + a C# analyzer shim, for teams that can host an F# core project inside a C# + solution and want the compiler itself enforcing the discipline. +- **Interop analyzers.** Once an F# backend exists, the boundary itself needs + checking: a value crossing from a real F# DU into the C#-side shim + representation must stay branded and exhaustive across the language edge, not + just within one language. +- **Multi-language frontends.** Ties directly to + [P-017](P-017-multi-stack-frontends.md) — Own.Types facts (#1–#13) become one + more fact family the OwnTS/OwnJVM frontends emit over the same OwnIR seam + (#18) the ownership facts already use. + ## Non-goals Refuse the boil-the-ocean version. The first move is explicitly **not** dependent @@ -105,9 +293,12 @@ types, GADTs, or higher-kinded types — that way lies a tower of type-level arithmetic (башня type-level арифметики) where you wanted to write a function and end up proving 2 + 2 = 4. The DSL must not become a new general-purpose language; it stays a spec/model/contract layer. No new runtime, no rewriting the codebase — -brands and refinements lower to plain structs and smart constructors, and the -discipline is enforced by analyzer, not by a parallel type checker that drifts -from the core (the project's standing meta-irony). `[OwnIgnore("reason")]` remains +brands, refinements, and unions lower to plain structs/records and smart +constructors, and the discipline is enforced by analyzer, not by a parallel type +checker that drifts from the core (the project's standing meta-irony). +Algebraic domain modeling (pillar 2) gets the same restraint: exhaustive matching +is enforcement of *existing* C# `switch`/pattern-match syntax, not a new +pattern-matching language grafted on top of it. `[OwnIgnore("reason")]` remains the escape hatch. ## Deferred catalog @@ -122,14 +313,16 @@ Surveyed and explicitly **not** first — recorded so the ideas aren't lost: `Add: Expr -> Expr -> Expr`). Only if a typed AST / DSL / query-builder need appears — relevant to the Snipper / Reactor / AST-transform ideas, not before. -- **Phantom types** — already in scope, as the underlying mechanism behind brands. +- **Phantom types** — already in scope, as the underlying mechanism behind + brands (pillar 1, including strongly typed IDs). - **Higher-kinded types** (abstract over `F<_>`: Functor / Monad). Do not touch: assembling a spaceship out of `IEnumerable`, `Task`, and pain. - **Row types** ("an object with at least these fields"), **existential types** ("there is some hidden `T`" — plugin/handler systems, heterogeneous - collections), **intersection `A & B`** / **union `A | B`** types, and - **gradual typing** (strict + dynamic mixed; the risk is `any` spreading until - the type system is a decorative quality sticker). + collections), **intersection `A & B`** / **union `A | B`** types (the + type-theory *union*, distinct from pillar 2's closed-shape `union` + declaration), and **gradual typing** (strict + dynamic mixed; the risk is + `any` spreading until the type system is a decorative quality sticker). - **Modal types** (`Html`, `Sql`, `sanitize: Html -> Html`) and **indexed types** (`Buffer`, `Password`, pipeline @@ -137,14 +330,16 @@ Surveyed and explicitly **not** first — recorded so the ideas aren't lost: with branded + typestate, so they may fall out for free once those two land. Priority, most-applied → academic tail: **branded/opaque · units of measure · -typestate · refinement · effect types (P-008) · session types · phantom**, then -**dependent / GADT / HKT** as the cognitively expensive end. +typestate · refinement · discriminated unions/exhaustive matching · effect types +(P-008) · session types · phantom**, then **dependent / GADT / HKT** as the +cognitively expensive end. ## Open questions 1. **Surface:** analyzer-only (annotate C# in place) vs `.own` spec + source - generator vs both. Brands and refinements want a generator (smart - constructors); typestate wants the analyzer + the affine core. + generator vs both. Brands, refinements, and unions want a generator (smart + constructors, exhaustive-match helpers); typestate wants the analyzer + the + affine core. 2. **Where do brands live** relative to P-006 capabilities — is a capability just a branded, non-`Copy` resource token, or its own kind? 3. **Refinement strength:** syntactic predicate enforced at the constructor @@ -152,6 +347,17 @@ typestate · refinement · effect types (P-008) · session types · phantom**, t verification backend, P-002). v0 should be the former. 4. **Typestate ↔ ownership seam:** confirm transitions express consume-self through the *existing* affine facts, so `commit` then `rollback` is reported as - use-after-move by the one core — no second mechanism. + use-after-move by the one core — no second mechanism. Pillar 3's items 10–13 + are the concrete test of this seam: each must reduce to it, not spawn a + parallel one. 5. Do **modal/indexed** types ever need their own surface, or are they always reducible to brand + typestate in practice? +6. **Diagnostic prefix.** `DI`, `EFF`, and `OBL` are established per-pillar + families (see `ownlang/diagnostics.py`). Does Own.Types reserve `TYP0xx` the + same way, or fold into core `OWN` codes with a `[type: …]` kind tag mirroring + the existing `[resource: …]` tag? Reserving `TYP` now avoids repeating the + `WPFxxx`-catalog-vs-emitted-code confusion recorded in + `docs/notes/consolidation-and-positioning.md`. +7. Do discriminated-union exhaustiveness (#6) and `Option`/`Result` unwrap-safety + (#7, #8) stay one analyzer rule family or split into separate rules sharing + only the source-generator scaffolding?