Local let binding does not prevent mutation

[tcbrindle]

The example given in the documentation is

public fun main() {
  let gravity = 9.81
  &gravity = 11.2 // error: cannot assign, `gravity` is a `let` binding
}

However, this code currently compiles without error

[kyouko-taiga]

That is a good example of why I think we should seriously reconsider the idea of allowing escape through local let bindings. The reason why the access checker doesn't complain is that there is no other use of gravity in this scope and so we can promote any access as though gravity had full ownership. This promotion mechanism is there to allow things like this:

fun gravity() -> Float64 {
  let g = 9.81
  return g
}

IMO there is no formal argument for accepting the function above but not the one from the original post. To me, it means that if we special-case access promotion so that we can only go from let to sink we're making the model more obscure, which undermines the usability argument.

[joehillen]

Could a solution be to require the user to declare intent with a different keyword?

public fun main() {
  sink gravity = 9.81 // error: `gravity` is declared `sink` but is not returned
  &gravity = 11.2 
}

[kyouko-taiga]

There are 4 introducers for binding (5 if we count set which is currently not supported):

• let: immutable access without ownership
• inout: mutable access without ownership
• var: mutable access with ownership
• sink let: immutable access with ownership

The purpose of access promotion is to interpret let as though you had written sink let. The rationale is that the compiler can be clever enough to see that you haven't violated the invariants of MVS.

IMO the right way to write OP's function is as follows:

public fun main() {
  var gravity = 9.81
  &gravity = 11.2
}

And the right way to write the function in my response is:

fun gravity() -> Float64 {
  sink let g = 9.81
  return g
}

[dabrahams]

On Sep 17, 2024, at 11:44 PM, Dimi Racordon ***@***.***> wrote: there is no formal argument for accepting the function above but not the one from the original post

I think that depends entirely on how you describe the system. The principle that an object can move at its point of last use is enough to justify it. I suppose one could misinterpret that phrasing as meaning the object can move into a synthesized mutable binding with the same name as the original, but that would be perverse IMO.

[tcbrindle]

The purpose of access promotion is to interpret let as though you had written sink let. The rationale is that the compiler can be clever enough to see that you haven't violated the invariants of MVS.

This seems very understandable to me -- I can move out of a local let-binding when the compiler knows that it refers to a lifetime-extended temporary (with apologies for my C++ terminology)

So is the problem that the compiler is not enforcing the immutability of sink let bindings, or am I misunderstanding something?

[joehillen]

* `sink let`: immutable access with ownership

sink let implies the existence of sink var. Is such a thing possible? If not, could sink let be reduced to just sink?

[kyouko-taiga]

It cannot, because sink in a parameter gives you write privileges. sink let is really var without the right to mutate. It is an additional restriction w.r.t. to the underlying model.

[dabrahams]

To put it differently, it could be reduced to just sink, but then we'd have the wrong default. You'd be writing a lot of sink vars and few sinks.

[joehillen]

Thank you for the clarification.