SharedMut[T] Names the Capability, a Call Makes the Hull, and There Is One SpellingStatus: Superseded by ADR-281 — its D1-D3 are D1-D3 there Supersedes: ADR-040 §3 — “the annotation is the constructor” — and the “there must not be a constructor entry” line it put in the ledger Builds: ADR-039 D9, which named the type and was unbuilt Related: ADR-052 (the nullable hull, which stays the compiler’s, and D2 says why), ADR-057 (both lock shapes, chosen per value), ADR-061 D2 (every count plain at one user thread)
Part I 6.2 gives the shared mutable type a short name — “the common case, which is why it has the short name” — and Part II 12.2 writes the counter with it. Measured before deciding:
let counter: SharedMut[i64] = 0 → emitted as `SharedMut<i64>`, and rustc says
"cannot find type `SharedMut` in this scope"The name went through, untranslated, into the language below, about a name the program did write and the specification does promise. Part III C.1’s class.
The long spelling was in better shape and still broken. Shared[Locked[i64]]
made both hulls on one line — except where the value was a number, because a
literal has no type of its own (ADR-060) and the rule that made the
hull needed one. So the language’s own counter did not compile in either spelling.
And the two spellings were not the same type. Rc<Local<i64>> below for both,
two distinct types in the checker: silently interchangeable underneath,
incompatible above.
What the survey said. Every language that gives this capability a name gives it
one name and no composition — Clojure’s atom, Haskell’s MVar and TVar,
Scala’s Ref. None of them can spell it as “a count around a lock”. Rust is the
outlier with Arc<Mutex<T>>, and it is the one everybody complains about. Each of
those also makes the cell with a call, and its change takes a pure function —
which is what allows compare-and-swap with retry instead of locking.
SharedMut[T] means a value several parts own at once and any of them may
change. It does not mean “a count around a lock”. What is under it is the
compiler’s, chosen per value the way the count already is
(ADR-037 D7): the cheap shapes where nothing can cross
(ADR-061 D2), the robust ones where something can.
It is one name up to the emitter and two hulls only there. A name resolved away earlier would put a spelling nobody wrote into every message about the language’s most common type — which ADR-039 D9 named as exactly what having one name buys: “no internal spelling that could appear in a diagnostic, a printed type, or an entry.”
And naming the capability is what keeps the door open. ADR-039
§3 leaves one: update is a pure computation and therefore repeatable, which is
the route to a lock-free implementation by retry. A name that is the mechanism
closes it; a name that is the capability does not. Nothing is promised and nothing
is measured — this decision only declines to make the promise impossible.
Shared(x), SharedMut(x), Locked(x).The annotation stops being the constructor. A hull is made by calling the type’s name, which is a spelling the language already has: a call on a type name resolves to its constructor.
The line this settles, and it settles the nullable case with it:
A hull you cannot observe, the compiler writes. A hull you can observe, you write.
A T? costs nothing and hides nothing — the same value, possibly absent — so its
Some(…) stays the compiler’s (ADR-052). These three change when a
value is cleaned up, which Part I 6.2 says a program can see.
What that buys is that the positions stop being a list. The annotation could
only construct where a position said so — an annotated let and a struct
literal’s field — and a list somebody has to keep complete is a list with holes in
it. Four of them, all the same hole: a number literal (no type, so nothing knew a
hull was wanted), a return into a shared result, an argument, and the field as a
second special case. A call is an expression, and expressions go everywhere.
It is the compiler’s to type, not the ledger’s. A ledger signature binds $T
from the receiver (ADR-031), and a constructor has none: the type
argument comes from what is handed in. So this is written where T?’s wrap is
written.
And it is what makes a literal work at all. SharedMut(0) hands 0 to a call
in the emitted code too, so the language below gives the number its type the way it
gives one to any argument. The annotation could never have answered that.
Shared[Locked[T]] is not a spelling for it.It is refused, and the message carries the replacement. Two ways to write one type is what the short name was given instead of, and here it was worse than untidy: the same bytes below, two types above.
Locked[T] keeps its own second use — individually locked fields inside a
shared structure, one lock per field rather than one around everything — which is
the distinction Part I 6.2 already draws.
Part II 12.2’s counter compiles and runs, at both settings. The program the
whole user_parallelism switch exists to serve:
fn zaehle(counter: SharedMut[i64]) { counter.update fn(alt) { alt + 1 } }
fn main() { let counter = SharedMut(0) counter.set(5) zaehle(counter) … }At no it is Rc<Local<i64>> at both ends; at yes Arc<Crossing<i64>> at both
ends; both print 6.
A refusal names the constructor now, and in one sentence:
“write Shared(db) — a hull you can see is one you write”, where it used to have
to send the reader to another line.
The analysis lost a little precision and says so. A slot with no annotation is
recorded as a Shared rather than as a Shared[Connection], because the
constructor call says which hull and not what it holds. It needs no more than that
to choose a count, and --sharing prints what it knows.
One probe had to be reset to stay a probe. tests/lock_floor.rs asks what an
always-Mutex floor would cost by swapping one ledger entry out. Ledger::infer
runs the sync inference itself against the shipped ledger, which now describes
SharedMut::access — and that inference only ever raises a claim, never lowers
one. Without putting the claim back first, the probe would have measured the
shipped answer and called it the variant’s.
What it cost: twenty-six lets in the tests, seventeen long spellings, and one
test whose premise the change removed — “the idiom is not sync today, because
nothing can resolve access“. Something can now.
Locked[Shared[T]] — a lock around a handle, the other way round. A
different type, probably a useless one, and still permitted.SharedMut reached rustc untranslated because
nothing checks a written type name against anything; that is true of every
misspelling and is not this record’s. A value nothing declares has had
NK1117 since ADR-051; a type has nothing.All three. SharedMut is a type the checker carries whole and the emitter
expands, with the four doors in std.contracts, the handle duplicated when it is
handed on by value, and the count decided for it like any other. The three
constructors are typed in check::Checker::hull and written in emit::hull_new,
and the count they take is looked up through Flow::bound. NK1123 refuses the
long spelling and refuses a hull of a hull. The annotation constructs nothing:
Checked::shared_sites and Emitter::lock_hull are gone, and with them the two
positions.