O-002, Granularity Inversion
error[O-002]: precision cannot be manufactured, only surrendered.
What fired
A membrane transform pointed upward along the granularity lattice. The spec's example (§7): a rule of the form -> others: exact where the holding itself is only known at coarse(city). The membrane was asked to emit more precision than it possesses.
Why the grammar forbids it
Axiom IV: precision only flows downhill. Every value carries a granularity coordinate on the lattice
exact ⊒ coarse(g) ⊒ category ⊒ existence
and the type system admits transforms only downward. Coarsening is a cast; refinement is a type error. There is no syntax for an upward cast (per spec §4.7, the grammar simply has no word for it), so O-002 exists to catch the one place where inversion can still be expressed: a membrane rule whose declared output grain exceeds the grain of the value flowing through it.
The ethics are the point. Privacy leaks are usually precision leaks: you shared your city and something downstream reconstructed your street. A system that can sharpen your data after you released it has taken something you never gave. In Osmol that sharpening is not a violation to detect, it is a sentence that cannot be typed: downstream of any membrane, information can only get blurrier.
How to fix it
You have exactly two honest options: surrender the precision, or stop promising it.
twin ana {
hold location(ana) = grid(52.52, 13.40) -- known only at coarse(city)
-- (it arrived through a membrane at that grain)
membrane {
location(*) -> others: exact -- error[O-002]: upward cast
}
}
Either accept the coarser transform, so you promise no more than you hold:
membrane {
location(*) -> others: coarse(city) -- ok: identity cast, M stays fractional
}
or, if others genuinely need street-level truth, refine the source hold: obtain the value at exact yourself, at the origin, where the precision legitimately exists. What you may never do is write a rule that conjures the precision in transit.
In v0.1
This diagnostic cannot fire in the reference interpreter. osmol.py does not track a holding's granularity coordinate: values are opaque strings, and casts are applied only as pressure weights (exact 1.0, coarse 0.7, category 0.5, existence 0.3) plus a textual annotation on the delivered value. With no grain on the holding, there is nothing to compare a rule's output grain against.
The full lattice checker is Stage 3 (semantic analysis) work in the engineering dissertation's compiler pipeline. The corresponding runtime guarantee, Theorem 4 (Granularity monotonicity), which states that along any flow path granularity is non-increasing, is open. Implementers building beyond v0.1 should type every value as a (value, granularity) pair and reject upward casts statically; that single enrichment makes both O-002 and Theorem 4 checkable.
Related
- Granularity: the lattice, in full
- membrane: where casts are declared
- The Open Theorems: the status of Theorem 4