Disallow consumption through local lets

[kyouko-taiga]

I know it may look extreme, but I'm really tempted to try disallowing the consumption of local let bindings. I'm starting to think that the trick is causing more harm to understandability than it helps writing concise or "traditional-looking" code.

For instance, this is currently allowed (at least in principle):

fun f() -> Int {
  let u = (x: 0, y: 1, z: 2); let y = u.y; let v = u
  print(u.x) // 0
  print(y)   // 1
  print(v.z) // 2
  return y   // OK
}

We can accept this program because the compiler can figure out two things:

• u actually holds ownership of its value, so in fact it's as though it had been introduced with sink let.
• It's OK to consume through u, v, or y because we can just desugar v as u and y as u.y.

None of these conditions holds if a non-trivial projection (e.g., a call to a subscript) is involved or if another use occurs after the consumption of y (e.g., replace return y by y.deinit(); print(v.z)). The the compiler will assume we're dealing with "regular" lets and emit error messages accordingly. So we can build very similar-looking programs and get different behaviors for which an explanation requires a deep dive into the way the compiler thinks about lifetimes. For example

import Geometry
fun g() -> Int {
  let u = Vec3(x: 0, y: 1, z: 2); let y = u.y; let v = u
  print(u.x) // 0
  print(y)   // 1
  print(v.z) // 2
  return y   // error: cannot consume through a let-binding  
}

The problem here is that u.y is a property access on an opaque type and so we cannot partially consume an instance of Vec3.
Everything would be explained more easily if we said that consuming local lets is illegal. Then we'd have to rewrite the program like this:

fun f() Int {
  sink let u = (x: 0, y: 1, z: 2); let y = u.y; let v = u
  print(u.x) // 0
  print(y)   // 1
  print(v.z) // 2
  return u.y // OK
}

For the low cost of 4 characters we get clearer intent and simpler rules.

On the other hand the code looks a little more foreign and we'd likely see more errors when dealing with indestructible types. Optimizations could get a little harder but I'm not too worried because we could probably remove bindings that have an obvious desugaring during access checking.

[dabrahams]

There is currently one simple explanation for when you can consume a value: when you can know (statically and locally) that there will be no live bindings to it immediately thereafter. That is true no matter what the value has been bound to. Adding a rule prohibiting consumption in one case makes the language more complicated, not simpler.

[kyouko-taiga]

It's the mental effort necessary to figure out whether the rule is upheld that is difficult, not the expression of the rule itself. My rule is simpler to state and inspect: no consumption through a let.

[dabrahams]

But it doesn't explain all the other conditions where you can't consume, and to explain those other conditions, you need my rule anyway.

It's almost like saying, “let's make a rule that if you are wearing a hat, you're not allowed to drive a car, because that will be really easy to understand.” It doesn't help me understand that I may not be allowed to drive for lots of other reasons (no license, underage, impairment, blindness). It just adds an unnecessary new restriction because the condition is easily inspectable.

[kyouko-taiga]

I understand your argument and it is true that in general we need to also run a little list of checks to understand why an escape isn't allowed. But I still claim the "hat rule" simplifies the whole picture.

The rules for consumption are as follows:

1. The value of the binding is initialized at the point of consumption.
2. There is no outstanding projection of the consumed value.

The "hat rule" adds a condition, which seems like it won't help my case.

• The binding through which the consumption occurs is introduced by any introducer but let.

But my claim is that it gives us a shortcut. If we order the hat rule before the others, then the first item on the list is to look whether or not the binding is introduced by let. If it is, then there's nothing more to think about.

The reason why I think this shortcut is useful is that let is by far the most common binding we should encounter. Therefore any other binding we choose should be the result of some reasoning that let us conclude we needed more capabilities. That also means any other binding should raise our level of awareness when we look at code. If someone used inout, that's because they couldn't use let and so there must be a reason why this extra capability is needed, otherwise the compiler would have ideally complained. If the ability to let a value escape is part of the possible reasons for choosing something other than let, then we don't need to mentally run the algorithm deciding whether an outstanding projection exists for the most common binding. In other words we don't need to bother asking for a driving license or check the car insurance coverage, we can look at the driver's head.

Another thing to note is that the mental algorithm is more complex for let than it is for any other binding. Because a let-bound value may come as an argument and we can't see the caller's context, there's no way to know whether or not it has outstanding projections and we must make a pessimistic assumption. This strategy is sound but there are two problems:

1. It is not hard to explain if you think like a compiler. If you think like an interpreter, however, then it is more tricky because it's easy to construct an example where it's obviously true that no outstanding projection exists. Besides, if we look at research in HCI trying to understand why people struggle with Rust, one recurring conclusion is that many people do think more like interpreters than compilers.
2. Anyone who'll understand local bindings by relating them to passing conventions will be surprised that the equivalence only partial because of the pessimistic choice we have to make once a local let turns into the parameter of a lambda representing its useful lifetime. For example:

fun main() {
  let v: Array = [1, 2, 3]
  let x = v[0]
  eat(x)
}

// ↑ is not truly equivalent to ↓

fun main() {
  let v: Array = [1, 2, 3]
  v.with_element(at: 0, (x: let Int) => eat(x))
}

In fact, the program that is actually equivalent to the top definition of main is as follows:

fun main() {
  let v: Array = [1, 2, 3]
  v.with_element(at: 0, (x: sink Int) => eat(x))
  //                        ^^^^ aha!
}

[kyouko-taiga]

Also the algorithm for determining the escapability of a local let binding is not obvious IMO.

For any other binding we can just look at its uses up to the point where we want to consume it and inspect the lifetimes of the projections we find. For let we must apply this algorithm recursively on the source of the let binding itself. From my original example, for instance, it is not enough to conclude that y has no outstanding projection, we must also run the same check for x while excluding the uses of y.

You referred to this algorithm as reference counting. I can get behind that but only partially because reference counting suggests an "interpreter-like" understanding of the process, which is inaccurate because we must consider useful lifetime ranges. Reasoning about lifetimes requires a compiler-like mindset because we must think about all program paths simultaneously.