Add freeze wrapper

[odersky]

Based on #24352

[bishabosha]

to me this sounds like a block where mutability should be prevented on the inside, (i.e. like its some pure scope). Alternatively this has an effect similar to "freeze" in other languages (i.e the result is now immutable).

[odersky]

Yes, I was unsure as well. I also thought of freeze before. Do you know which other languages have a construct like this?

[odersky]

OK, I renamed to freeze. A search showed that it is used like this in Javascript and Haskell and it was proposed for beta.

[bishabosha]

I think the mechanism in most cases is assignment to an immutable variable (const in C++, let in Swift, Rust), so not a property of the type. Javascript has Objects.freeze. .NET has a Freezable abstract class

[bishabosha]

Ruby's root Object class also has a universal freeze method

[Linyxus]

This is not yet renamed to freeze.

[Linyxus]

A soundness issue related to boxes:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.{Mutable, immutable}

// A mutable ref and its immutable version
class Ref extends Mutable:
  private var data: Int = 0
  def get: Int = data
  update def set(x: Int): Unit = data = x
def allocRef(): Ref^ = Ref()
type IRef = Ref^{}

// Boxes
case class Box[+T](unbox: T)

// Parallelism
def par(op1: () => Unit, op2: () => Unit): Unit = ()

def test1(): Unit =
  val a = allocRef()
  val xs = immutable:
    Box(a)
  val b = xs.unbox
  par(() => a.set(42), () => println(b.get))  // data race! boom

[Linyxus]

Another counter-example related to double-flips:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.{Mutable, immutable}

// A mutable ref and its immutable version
class Ref extends Mutable:
  private var data: Int = 0
  def get: Int = data
  update def set(x: Int): Unit = data = x
def allocRef(): Ref^ = Ref()
type IRef = Ref^{}

def test1(): Unit =
  val magic = immutable: // should be error, but ok
    (x: Ref^) => (op: Ref^ => IRef) => op(x)
  val reallybad: Ref^ -> Ref^{} = x => magic(x)(x => x)

reallybad says that: give me any tracked Refs, I will erase the capture for you!

[odersky]

@Linyxus Can you try to make this work to fix the unsoundness?

[natsukagami]

Is the first example compiling because putting a into a Box is a pure operation (doesn't charge a)?