Purity and mutable types

[Linyxus]

Compiler version

main

Minimized code

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

// 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 main(): Unit =
  val a = allocRef()
  val t1: IRef = a  // should be error too, but ok
  val t2: Ref^{} = a  // error

Output

Only the last line has an error, but not the IRef line.

Expectation

Both line should be an error. They should morally be equivalent.

[hamzaremmal]

This actually highlights a potential issue with type aliases that I've been thinking about last week with IArray. I believe I didn't mention it yet to someone... my focus was on the initialisation of objects.

What does it mean to have a capture set in the rhs of a type alias? Can we then write IRef^{a}? If so, do we combine the underlying capture set with the declared one? This approach will then break purity with aliases, no? What if it is an opaque alias and we cannot see beyond the fact we have a type and a capture set?

[bishabosha]

i thought (Foo^{a})^{b} is already Foo^{a,b}

[Linyxus]

I was a bit lazy when opening this issue so the example is not the best. I think it is not tied to mutable classes but more a notational thing for capability classes in general:

import language.experimental.captureChecking
import caps.*

class Ref extends SharedCapability
def allocRef(): Ref^ = Ref()
type IRef = Ref^{}

def main(): Unit =
  val a = allocRef()
  val t1: IRef = a  // should be error, but ok
  val t2: Ref^{} = a  // error, as expected
  val t3: Ref^{} = t1  // error

We seem to install more capture set variables than what is needed.

Note that this is not a soundness problem, since the last line is rejected properly.

[hamzaremmal]

Note that this is not a soundness problem, since the last line is rejected properly.

I don't see why the last line should be an error. For me, it should pass.

[Linyxus]

What I meant is that if both t1 and t3 pass, it will be a soundness problem. But no, this is more a notation problem.

[hamzaremmal]

Ah yes, yes, indeed. Sorry Yichen, I misread the issue.