Consolidate CC

[odersky]

A refactored and consolidated capture checker without any drastic changes to the algorithm. The main changes are:

• Go back to the "sealed" policy where we check that type parameters do not contain cap instead of checking that we do not box or unbox cap.
• Rename @unbox to @use
• Fix several soundness holes relating to reach capabilities

Based on #21861

[Linyxus]

At this point, I feel that curried capture for reach capabilities makes sense no more, given that (xs: List[() => Unit]) -> () ->{xs*} Unit behaves the same as (@use xs: List[() => Unit]) -> Unit, in the sense that:

• when applying (xs: List[() => Unit]) -> () ->{xs*} Unit, we need to charge the dcs of the argument;
• a function of (xs: List[() => Unit]) -> () ->{xs*} Unit is second class: they can only be methods, but disallowed as values, so they cannot be freely passed around.

Besides, functions like (xs: List[() => Unit]) -> () ->{xs*} Unit is causing us additional troubles: since {xs*} could be widen to {cap}, we need to conservatively charge dcs of the argument for any function that returns a cap. What is worse, ANY function that returns a cap may need to be treated in a second-class way, since under that cap the reach capability of some parameter may be there.

Given the above, shall we drop the special curried capture mechanism for reach capability completely? Reach capabilities, like other capabilities, bubbles all the way up to the top, unless stopped by a boxed environment. Any function that uses the reach capability of its parameter is then automatically be required to be marked as @use. @use are still second class. But at least the second-class restriction will not contaminate other functions that return a cap.

[odersky]

@yichen

Given the above, shall we drop the special curried capture mechanism for reach capability completely?

In fact that's what is currently implemented. There's a ccConfig option deferredReaches which enables it, but it is unsound. I believe we can make it sound if we implement environment avoidance. I believe (but am not sure) that
environment avoidance alone will be enough to support curried reaches. More precisely, say we have a function

def test3(xs: List[() => Unit]): () ->{xs*} Unit = () =>
  println(xs.head)  // error, ok under deferredReaches

Then test3 can be eta expanded to have type (xs: List[() => Unit]) -> () ->{xs*} Unit. This is still a bit dubious since now the eta expansion counts as pure. But we could imagine it gets expanded polymorphically to have type:

[C^] -> (xs: List[() ->{C^} Unit]) -> () ->{C^} Unit`

That's a pure function, so we have some justification to treat (xs: List[() => Unit]) -> () ->{xs*} Unit as pure as well.

[Linyxus]

I see, I agree. Environment avoidance can make deferred reaches sound, since it is basically a mechanism for charging effects on subsequent arrows of a function spine correctly. (note that since effects can not only be those of function itself, but can also be some effect variable instantiated by the application of the function, like capture variables or reach capabilities)

[Linyxus]

It turns out that the subcapturing rule between a reach capability and its dcs is not sound. The problem is that type substitution breaks it.

In other words, this rule is unsound:

x: T ∈ Γ
--------------------
Γ ⊢ {x*} <: dcs(T)

Type preservation does not preserve it. As an example, given the following context:

X <: ⊤
x: List[(X, Op^{async})]

Note that

dcs(List[(X, Op^{async})])
  = dcs(X) ∪ dcs(Op^{async})
  = dcs(⊤) ∪ {async}
  = {} ∪ {async}
  = {async}

Therefore, under this context, one may derive:

{x*} <: {async}

And this will not be preserved by a type substitution, for instance, [X := Op^{io}]. After applying the type substitution, the context becomes:

x: List[(Op^{io}, Op^{async})]

and we have

dcs(List[(Op^{io}, Op^{async})]) = {io, async}

Therefore, under this context, we can only derive:

{x*} <: {async, io}

And the relation `{x*} <: {async}` is falsified after the type substitution!

In other words, type application could break typing. Based on this idea, we could construct the following example:

import language.experimental.captureChecking
import caps.cap

def test(io: Object^, async: Object^) =
  def compose(op: List[(() ->{cap} Unit, () ->{cap} Unit)]): List[() ->{op*} Unit] =
    List(() => op.foreach((f,g) => { f(); g() }))

  def compose1(op: List[(() ->{async} Unit, () ->{io} Unit)]): List[() ->{op*} Unit] =
    compose(op)

  def foo[X](op: (xs: List[(X, () ->{io} Unit)]) => List[() ->{xs*} Unit]): List[(X, () ->{io} Unit)] => List[() ->{} Unit] =
    op

  def boom(op: List[(() ->{async} Unit, () ->{io} Unit)]): List[() ->{} Unit] =
    foo(compose1)(op)

The boom function in the end, turns a list of impure operations into a pure one. It should not compile, but it does.

[odersky]

Yes, that's bad. The alternative would be to always take cap as the underlying type of a reach capability. Unfortunately that breaks useful idioms. For instance, in reach-problem.scala:

import language.experimental.captureChecking
import caps.use

class Box[T](items: Seq[T^]):
  def getOne: T^{items*} = ???

object Box:
  def getOne[T](@use items: Seq[T^]): T^{items*} =
    val bx = Box(items)
    bx.getOne

we'd get with that change:

~/workspace/dotty/tests/neg-custom-args/captures> scc ../../pos/reach-problem.scala
-- Error: ../../pos/reach-problem.scala:10:7 -----------------------------------
10 |    bx.getOne
   |    ^^^^^^^^^
   |Local reach capability bx.items* leaks into capture scope of method getOne
1 error found

Other tests failing in similar ways are:

    tests/pos/reach-problem.scala failed
    tests/pos/gears-probem-1.scala failed
    tests/pos-custom-args/captures/gears-problem.scala failed

What can we do to accept these, but rule out the unsound one?

[odersky]

In the previous example, bx has type

val bx: Box[T]{val items: Seq[T^{items*}]}

[odersky]

In your example, where would you expect to see an error?

[Linyxus]

In the status quo, the reach capabilities are purely a device for polymorphism. That makes a lot of stuff counter-intuitive. Among them, one is that given x, x* is not an inherent property of the object cluster pointed to by x, but an abstract variable associated with x. The association is even syntactical: it stands for the capabilities into which the cap in the type of x will be instantiated into in the future.

Now let's consider an example. Given

  f : (@use x: List[Op^{cap}]) -> () ->{x*} Unit
  y : Op^{async,io}

what should f(y) charge to the environment? what should be the result type?

A tempting answer maybe: this term charges y* to the environment, and the result type is () ->{y*} Unit. It should be like that, no?

But actually NO. Let's translate the function type:

  f : [@use C^] -> (@use x: List[Op^{C^}]) -> () ->{C^} Unit
  y : Op^{async,io}

and the application should then be in the form f[?D](y). This term should charge ?D to the environment, and the result type should be () ->?D Unit. But what is ?D? Apparently it is the instantiation of the capture parameter C. Going back to caps, it is the instance of the caps in the argument type of f when applying the function in f(y). To compute it is to solve this problem: given y : Op^{async,io} and the expected type Op^{cap}, what capabilities get widen to cap? We could use dcs(Op^{async,io}) to overapproximate the solution to this problem.

Therefore the answer can be: the application should charge {async,io} to the environment, and the result type should be () ->{async,io} Unit.

More generally, when type checking the application f(x) given:

  f : (@use z: T) ->C U
  x : T'

we should charge dcs(T') (not x*) to the environment, and the result type should be [z:=x][z*:=dcs(T')]U (not [z*:=x*]!!).

Going back to the example, I think it is compose1 that should not be well-typed:

def compose(op: List[(() ->{cap} Unit, () ->{cap} Unit)]): List[() ->{op*} Unit] = ...
def compose1(op: List[(() ->{async} Unit, () ->{io} Unit)]): List[() ->{op*} Unit] =
  compose(op)

The result type of compose1 should be List[() ->{async,io} Unit], but not List[() ->{op*} Unit].

[odersky]

In fact, the problem shown by the unsoundness example was something completely different. Function foo makes clearly no sense.

  def foo[X](op: (xs: List[(X, () ->{io} Unit)]) => List[() ->{xs*} Unit])
               : (xs: List[(X, () ->{io} Unit)]) => List[() ->{} Unit] =
    op // error

This should have given a type error, but it passed since the encoding of a function type with reach capabilities in the result was wrong. It took me quite a long time to find the cause. It's because we unfortunately have this super-complex encoding of dependent function types as refinement types with a parametric function type as parent. The generation of this parametric parent function type was wrong for results containing reach capabilities.

So, it would be good to find a test that demonstrates the original unsoundness argument.

[odersky]

It would be really good if we could use a different function type encoding in the style of PolyTypes. That will require quite a lot of engineering, in particular for backwards compatibility but it would be a big simplification. So if somebody wants to take this on, this would be much appreciated.

[odersky]

We currently have have for any reference x that {x} <: {x*} and cs(x) <: dcs(x). This is not justified by the capless translation. But dropping these conventions breaks tests:

    tests/neg-custom-args/captures/refine-reach-shallow.scala failed
    tests/neg-custom-args/captures/inner-classes.scala failed
    tests/neg/i19470.scala failed
    tests/neg-custom-args/captures/leaking-iterators.scala failed
    tests/neg-custom-args/captures/lazylists-exceptions.scala failed
    tests/neg-custom-args/captures/lazylist.scala failed
    tests/run-custom-args/captures/colltest5 failed
    tests/pos-custom-args/captures/logger-tracked.scala failed
    tests/pos-custom-args/captures/boxed-use.scala failed
    tests/pos-custom-args/captures/lazylists-exceptions.scala failed
    tests/pos-custom-args/captures/lazylists1.scala failed
    tests/pos-custom-args/captures/logger.scala failed
    tests/pos-custom-args/captures/iterators.scala failed

Since colltest5 fails, the stdlib is likely to fail as well.

The problem is demonstrated in this extract of colltest5:

trait Iterator[+A]:
  self: Iterator[A]^ =>

trait View[+A]:
  def iterator: Iterator[A]^{this}

object View:
  def fromIterator[A](it: => Iterator[A]^): View[A]^{it} = new View[A]:
    def iterator: Iterator[A]^{this} = it

When we change the rules it fails with:

-- [E007] Type Mismatch Error: /Users/odersky/workspace/dotty/tests/new/test.scala:8:63 
8 |  def fromIterator[A](it: => Iterator[A]^): View[A]^{it} = new View[A]:
  |                                                               ^
  |                                         Found:    View[box A^?]^{it, it*}
  |                                         Required: View[A]^{it}
9 |    def iterator: Iterator[A]^{this} = it
  |
  | longer explanation available when compiling with `-explain`

The root cause is that given it: A => Iterator[B]^, we currently narrow the ^ after Iterator to it*
and we need the relationship {it} <: {it*} to then make the test compile. An alternative would be to narrow the ^ to it, but that requires that we work out span captures.

So I think until we work out span captures we are stuck on this one.

[odersky]

About adding environment avoidance. I tried that as well, but a great number of tests (>40) break. One problem is that we often treat cap as being informally the same as fresh. E.g.

def f() = 
  val r: Ref^ = newRef(1)
  r.get

But that causes a failure when we use r since we now have to avoid the r binding which gives us cap, which is not allowed. So before we can do that we have to get to a more refined treatment of cap.

[Linyxus]

It would be really good if we could use a different function type encoding in the style of PolyTypes. That will require quite a lot of engineering, in particular for backwards compatibility but it would be a big simplification. So if somebody wants to take this on, this would be much appreciated.

I could give it a try after the submission. It's been some while since my last compiler hacking.

[Linyxus]

About adding environment avoidance. I tried that as well, but a great number of tests (>40) break. One problem is that we often treat cap as being informally the same as fresh. E.g.

def f() = 
  val r: Ref^ = newRef(1)
  r.get

But that causes a failure when we use r since we now have to avoid the r binding which gives us cap, which is not allowed. So before we can do that we have to get to a more refined treatment of cap.

That's right. This leads me to the realisation that right now with the addition of environment avoidance existential types are useless in Capless:

1. Existentials only appear in function results.
2. When an existential is returned from a function, to make use of it one needs to use let-ex to bind it. Let's say we unpack the existential as (c,x).
3. Any use of x cannot be allowed then, since if c appears under a box it can never be unboxed, and if c appears as the top-level capture set of x with environment avoidance x cannot be used at all.

This seems really bad.

[Linyxus]

So, it would be good to find a test that demonstrates the original unsoundness argument.

Here it is!

import language.experimental.captureChecking
import caps.{cap, use}

trait IO
trait Async

def main(io: IO^, async: Async^) =
  def bad[X](ops: List[(X, () ->{io} Unit)])(f: () ->{ops*} Unit): () ->{io} Unit = f
  def runOps(@use ops: List[(() => Unit, () => Unit)]): () ->{ops*} Unit =
    () => ops.foreach((f1, f2) => { f1(); f2() })
  def delayOps(@use ops: List[(() ->{async} Unit, () ->{io} Unit)]): () ->{io} Unit =
    val runner: () ->{ops*} Unit = runOps(ops)
    val badRunner: () ->{io} Unit = bad[() ->{async} Unit](ops)(runner)
      // it uses both async and io, but we losed track of async.
    badRunner

(ps: Sorry for accidentally closing this PR, I misclicked)

[odersky]

@noti0na1 All suggestions implemented, waiting for your approval.

[noti0na1]

LGTM