feat: erased vars

[kasiaMarek]

Adds erased vars. For an erased var all rhs's of an assignment must be pure and the assignements are erased.

How much have you relied on LLM-based tools in this contribution?

Moderately. First version (manually adjusted) of typedAssign was generated.

How was the solution tested?

The are new test cases for compilation

[bishabosha]

i am curious how it is useful to have this? can you ever inspect what value is stored there

[mbovel]

i am curious how it is useful to have this? can you ever inspect what value is stored there

No, not in Scala directly. You can reason about the value of the var in Stainless though, that's our use-case.

[vkuncak]

Actually, whenever you have a stateful object whose capabilities (but not identity) change over time, this would be necessary, right @odersky ?

[odersky]

The capability type checker is not flow sensitive, so var's would not help. We need to create objects with the union of all the capabilities they might hold during their lifetime.

[mbovel]

Right, but can we still merge that change?

[kasiaMarek]

Right, but can we still merge that change?

I thought we decided that we will merge this to the epfl-lara fork instead given that there is no benefit for it in plain Scala.

[mbovel]

I thought we decided that we will merge this to the epfl-lara fork instead given that there is no benefit for it in plain Scala.

Even if there is no direct benefit for Scala right now, I believe it wouldn't hurt to merge that small change already.

@odersky: when we discussed, I had the impression you were not against allowing erased var. Were you?

[vkuncak]

Right, the compiler uses erased things only for their type. That said, we might as well allow users to construct the most natural data that witnesses the type using var if that is what makes the construction natural. Note that, as it is, this already passes:

import scala.language.experimental.erasedDefinitions
case class Box[T](var x: T)

def f(erased x: Box[Int]) = 42

@main def main =
  println("Here we go!")
  val t = Box(33)
  f(t)
  t.x = 55
  f(t)

So erased calls can see different run-time values, all of which are erased. Allowing erased var would give more syntactic flexibility. It makes difference for any downstream tool that differentiates mutable values, whether it is a program verifier or some sort of run-time monitor that preserves erased values at run time for debugging purposes.

Currently, I can already mutate t, which was used a witnessed, but I waste computation to do it, even when I use t only as a witness for erased parameters.