A few comments:
- Rather than talk about
lets specifically, I think the properties you ascribe need to be discussed as applying to values more generally, since they also apply to temporaries, arguments, returns, and such. They only apply tolets insomuch as aletbinding only ever has one value once it's been bound. - You say that there are "several general classes of such types", but I think that's an overcomplication. There's one specific property we're looking for in a value to say that it's sharable—does it not contain references to unsynchronized shared mutable state, transitively? The "general classes" you list afterwards can then be thought of as specific common cases of avoiding unsynchronized shared mutable state—immutable types do so by not having mutable state at all; value types check for uniqueness before mutating, or copy objects when they're shared; and synchronized objects guarantee their own race safety by other means.
- There's also a choice of where to enforce the "no transitive references to unsynchronized mutable state" property. In its full generality, it can be seen as a property of individual values, at a finer granularity than their types. For instance, the one unique reference to any object is theoretically safe to share by moving between tasks, and even sharing multiple references from multiple tasks could be safe if the tasks all agree not to mutate the object. Other languages like Pony use reference capabilities as a way of enforcing these rules at the granularity of individual references. We're making an explicit choice here to instead enforce the property at data type granularity instead.
- As a type trait, I'm not sure it makes sense to refer to
ActorSendable/Shar[e]ableas a protocol—it has no formal requirements, and you can't really retroactively conform a type to it, and we wouldn't want becoming sharable to induce a witness table or other ABI changes that normal protocol conformances do. It's more akin toAnyObject, or some of the other type traits likeTrivialwe'd like to expose in the future—although you can use it as a generic constraint very much like a protocol, the way types "witness" the requirement is through their inherent properties, not by providing any method implementations.