Reference 09 Composing refinements

9. Composing refinements (and, or)

A refinement can be built from other named refinements instead of restating their predicates:

shape Open         = SupportTicket where status != "closed"
shape Overdue      = SupportTicket where due < today
shape HighPriority = SupportTicket where priority == "high"

shape UrgentOverdueTicket = Overdue and HighPriority and Open
shape NeedsAttention      = Overdue or Escalated

A and B / A or B desugar to conjunction/disjunction of the operands' own predicates — not new mechanism, and/or in a new position (between named refinements instead of inside one where). and composes within a base: an instance has exactly one base shape, so two distinct bases are disjoint by construction and Overdue and SuccessfulCharge is provably empty — reported as dead machinery (checks.md A2), never silently accepted. or may compose unrelated base shapes — a cross-base union, shape Content = Post or Photo — the same set union of instances, with nothing new to define beyond what the property rule below already says about it. and binds tighter than or; not binds tighter than both (A and B or C ≡ (A and B) or C).

Composition carries refinement properties (## Refinements): A and B has the union of its operands' properties — a same-name collision between two distinct declarations is a compile error, while the same declaration inherited through a shared base is fine. A or B exposes only properties both operands inherit from a shared declaration, since a member may belong to either side alone. A composite may declare its own body (Reconciled, ## Refinements, §8), and a refinement of a refinement inherits its base's properties down the chain.

Across bases the property rule is unchanged, and it decides everything. Unrelated shapes inherit nothing from one declaration, so a cross-base union exposes id and exactly one more thing: the inverses inferred through fields typed with the union (## Relationships, the polymorphic association — Comment.target: one Content puts comments on both operands and on Content from one declaration, so Content where count(comments) >= 2 is a refinement over the union). Post.author and Photo.author are two declarations that happen to agree, and are not shared: a rule over Content reading this.author is a compile error. What such a rule may do without more: read id and the shared inverses, create facts whose fields are typed with the union, count, test existence, delete. Everything else is reached by narrowing per operand (## Predicate expressions): if target is Post then target.author else target.author — identical branches resolving to two declarations, which reads absurdly and is meant to, since the language refuses to guess that agreeing declarations mean one thing; where operands should share a declaration the missing construct is the cross-shape mixin (OQ35). Same-name, same-type sharing by coincidence was rejected: Car.weight in kilograms and Bicycle.weight in grams would compile and mean nothing, and a field added to one operand could create a match at a distance (## 1. Principles). The consequences, each checked: a cross-base union's body admits derived properties only — over the shared inverses or narrowed per operand — while frozen has no base to name, captured has no entry moment but creation (the spelling is initially on each operand), and undeletable gates on a refinement of each operand instead; a union with a transient operand is refused until the mixin lands — the rule fires per act, but every read is a branch per operand and nothing durable may reference the act; a rule's condition composing unrelated shapes inline must name the union first; entry into a bare static union is creation of an operand instance, so when leaving Content is the bare-shape unfireable error offering when deleted; and for one-writer disjointness a union overlaps each of its operands while distinct bases never overlap. The generated surface views a union through its own type — the shared members, the operand's name, a narrowing accessor per operand — and each operand's view widens to it.

The intended style: small, deliberately atomic refinements named to read like traits (Open, Overdue, HighPriority — no type suffix), with composites built as pure intersections/unions of trait names rather than restated predicates. Not solved: true cross-shape structural mixins, where a trait like Overdue is reusable across unrelated shapes (e.g. both SupportTicket.due and Invoice.due) — see Open/unresolved.