nikomatsakis / babysteps

Babysteps blog
https://smallcultfollowing.com/babysteps/
31 stars 22 forks source link

Some feedback on "Claiming, auto and otherwise" #43

Open eternaleye opened 2 months ago

eternaleye commented 2 months ago

I have mixed feelings about your proposed Claim operation. It feels to me like it's trying to do three things that could meaningfully be distinguished, and as a result, lacks clarity.

  1. On the one hand, it's broadening Copy to include operations that are O(1) and infallible, but are not memcpy.
  2. On the other hand, it's narrowing Copy to exclude "sufficiently large values" based on a heuristic.
  3. On the gripping hand, it's communicating a different intent than Copy would communicate after the change, which is to make the operation implicit.

For me, at least, (2) would result in a reasoning barrier for me - when is a type Claim? When is it not? Heuristics are difficult for me to reason about quickly, and take up disproportionate brainspace. In addition, (2) and (3) prevent Claim from being an intermediate trait between Copy and Clone, i.e. Copy <: Claim <: Clone.

Personally, my preference would be as follows:

  1. Split (1) off from the rest, and use that as the basis of Claim, so that Copy <: Claim <: Clone
  2. Bundle (2) and (3) together, but require implicitness be at least Claim: ImplicitClaim <: Claim.

This would result in the same actual types being implicit or not as when Claim is implicit innately, but keeps heuristics out of the "semantics of the type" trait chain, and instead branches off an "ergonomics of the type" trait at the appropriate point. Authors would accurately describe their type using Copy and Claim (and, in fact, defining Claim this way could potentially have a mechanized checker); they would then decide on the ergonomics of their type using ImplicitClaim. This separates these two different authorial responsibilities, of reporting their type's intrinsic properties to the trait system vs. deciding on their type's ergonomics.

nikomatsakis commented 2 months ago

Some thoughts:

nikomatsakis commented 2 months ago

Oops. I probably should have posted that comment with more context. Let me back up =)

I definitely see the appeal of what you're proposing here. I would prefer something that doesn't have heuristics. But I'm not sure if the split you proposed really adds a lot of value, so that's what I'm poking at -- what would we get out of having more traits?

My inclination is to say that I would keep Copy/Clone/Claim just as I proposed, but maybe add some other subtraits of Clone that capture more "hardened" versions of the Claim, such as O1Clone or TransparentClone.

My other thought is that, of the Claim properties I listed, the one that I see as most obviously useful to pull out is transparent, but unfortunately that already means that Clone: Claim: Copy would not hold. But transparent is the one that is tied to program semantics.

eternaleye commented 2 months ago

A big part of why I'd prefer the system I laid out is that Claim lumps together things on two axes: potentially enforceable vs. unenforceable, and descriptive of the types vs. ascriptive of their intent.

As a result of the first, it would be unclear to me when I could trust a type when it implements Claim.

As a result of the second, it would be unclear to me when I should implement Claim.

With the system I laid out, I lump together potentially-enforceable together with descriptive (as the intermediate trait), and unenforceable together with ascriptive (as the branched trait). As a result, the latter is upper-bounded by the former, and provides me a more solid "barrier of trust" (as a user)/"barrier of sanity" (as an implementer).

Without the more solid barrier of trust, I'm not sure if I'd ever turn on implicit claim for non-Copy types.

Without the more solid barrier of sanity, I'm not sure if I'd ever implement Claim for any non-Copy types.

In addition, this "enforceable/descriptive" combination provides the answer to subtler notions of O(1): No, because they themselves do not meet that criterion. "Direct" O(1) can be validated by a relatively simple check, because it already demands the absence of anything that would complicate the analysis.

As for code that would bound on it, one example would be in soft-realtime systems: bounding on actual O(1) says that the measurements you take when validating that you meet your deadlines are not subject to value-dependent factors that were not observed in the current testing session. It doesn't have to directly provide the property soft-realtime wants: it suffices to provide a property that enables verifying what it really wants.

wbcat commented 2 months ago

I am not a languages person, just a user of Rust. I like the idea to have a distinction between deep / allocating clones and shallow / non allocating clones. I also like the name Claim much more than the alternative Capture. Having some heuristics is fine for me and the possible future extensions via O1Clone / TransparentClone is sufficient for me. Also the lint based approach is my taste. My previous # 1 wish list item was the stabilization of the Never Type, but that got replaced, no it is the Claim Trait.