What's @& ?

Stream: lean4

[Daniel Weber]

I see in some places in the code @& in a type annotation, for instance in docs#Nat.log2 and docs#Nat.gcd. What does it mean?

[Henrik Böving]

They are ref count borrowing annotations, usually they are inferred by the compiler but for external functions the tags need to be provided explicitly. The tags instruct the compiler to not increment the ref count before sending a value to the function but instead assume that the function will not free the value.

[Kyle Miller]

I think that description might be misunderstood. Normally, the semantics are that ownership of a value is transferred in a function call, but @& indicates that the ownership is borrowed instead.

Normally, if a value is used after the function returns, then the compiler inserts a ref count increase before the call, but if it is not used, it's not inserted. (The function is responsible for a ref count decrement for that argument.)

When @& is used, then instead it's sort of dualized. If a value is not used after the function returns, the compiler inserts a ref count decrement after the call, but if it is used it's not inserted. (The function is not responsible for a ref count decrement for that argument.)

(I think I got this right, correct me if I'm wrong.)

[Eric Wieser]

Any change you could take over lean4#4305 for me, Kyle?