How to make shallow capture sets less burdensome?

[odersky]

I am currently trying to make the type checker use shallow capture sets. Two reasons:

• It corresponds to what we have in the paper. 
• Deep capture sets might be too pessimistic. For instance, Int retains cap => Int retains cap has capture set cap under the deep interpretation, even though it might well be the identity over Int retains cap. Similarly,  B => A or A => A has A in its capture set.

But if we do that we need some way to reduce the number of necessary retains annotations. For instance, assume thatA <: Any retains *, then it would be very annoying to have to write List[List[A] retains A] retains A. We can get around it by defining a type alias type List1[+A] = List[A] retains A, but it would be more convenient to roll that information into the class List itself. Something like

    class List[+A] extends Seq[A] retains A

Or, for now, as long as we do not want change the syntax of the language, 

   class List[+A] extends Seq[A], Retains[A]

Another issue is curried function types. Say we have a function of type 

   A => B => C => C

that retains io throughout. Right now it's

  (A => (B => (C => C) retains cap) retains cap) retains cap

Super annoying (in fact that's why we went to prefix syntax for retains sets in the paper to make this less of an eyesore).
One possible way around it is to decree that a curried function type never discards retains sets established to the left. The motivation is that a curried function type often does no computation until all arguments are supplied. So whatever is retained by the outermost function is retained by nested functions. With that convention, the last type could be written

 (A => B => C => C) retains cap

If a curried function does in fact discard a capability before reaching the result part, we can use a type alias to express this:

 type PureRest = B => C => C
 A => PureRest retains cap 

One could also think of inline syntax for this. Maybe A => (B => C => C) retains cap, or is that is too inconspicuous, A => {B => C => C} retains cap? But at least initially it won't be necessary, type aliases will work fine.

By the same reasoning we could then say that tracked arguments in a curried function type are retained by all functions to the right. I.e. assuming the alias X ==> Y for (X => Y) retains *, we could then write

 (Int ==> A) => B => C => C

and it would expand to

 ((x: Int ==> A) => (B => (C => C) retains x) retains x

Aside: In the final version of Scala-CC, we could introduce -> for pure functions that do not capture anything and define A => B as A -> B retains *. With that convention we might be able to keep most function types as they are now in the new cc interpretation.

[odersky]

The capture set info of a class could also be inferred. E.g. if A is tracked, then a class containing a field of type A automatically retains A, no declaration to this effect is needed. Similarly, a class or trait retains A if it has a method with a result type that retains A and the method does not have any arguments that could retain A. With these conventions we might be able to elide the large majority of retains annotations of classes. If the actual convention is too pessimistic we might then need an override with an explicit retains annotation. For instance,

class EmptySet[A <: Any retains *] extends Set[A] retains Nothing

[odersky]

One caveat: If we look at method signatures to deduce retains sets, we have to take partiality into account. For instance, with the scheme I outlined, Option[A] would retain A since it has a method def get(): A. But that is clearly too conservative. The key here is that get throws an exception for the None instance, so there are instances of Option[A] that do not retain A. On the other hand, once we track effects, get could have this signature:

abstract class Option[+A]:
  def get(): A throws NoSuchElementException

And that would disqualify it from contributing to the capture set. So it's a typical bootstrap situation: We can do a better job at capture set inference if we we track exceptions, and to do that ergonomically, we need good capture set inference.

[b-studios]

class List[+A] extends Seq[A] retains A

I think this is a good idea to keep annotations down.

However, I am not yet convinced it is a good idea to look at method signatures to infer retains. On the one hand, it feels a bit too complicated as a rule for users to grasp (fields are much simpler), but we might need to experiment and see. On the other hand, this implementation could resonate quite nicely with what Darya Melicher calls "authority" in her thesis.

[odersky]

The problem is abstract classes. You see fields only in concrete ones. There's not even a field in List, it's all in the subclass ::. So that means that basically every non-case class datatype would need to be annotated with retains. Feasible, sure, but if we can automate it it will make things more convenient.

[abgruszecki]

I meditated about this a bit. Here's what I have:

• In the shallow interpretation, the capture set of a class should accurately reflect all it can possibly capture.
• A class' constructor can store in a field whatever an external object's method returns. Therefore, to infer a class' capture set, we need to look at its body.
  • It doesn't seem fundamentally more complicated to consider both methods and fields, as opposed to only fields, when considering the class' body.
• Should a class automatically retain its co- or in-variant type parameters?

  • If a class is parameterised with a type, it can only (reasonably) obtain an instance of that type by either 1) receiving it as an argument or 2) receiving as an argument something that can create such an instance.

  • In both cases, we should be able to infer a more precise capture information than the type parameter itself.

    • In particular, consider that class Cons[A](head: A, tail: List[A]) should have the capture set of {head, tail}.
    • Observe that if a method receives such an argument that allows it to create an instance of class' type parameter, the class may not need any capture information at all. (Such cases are feasible but probably rare, as the type parameter could be moved to the method).

  • However, a trait could have type parameters unused in its body. Consider:

    trait Either[+L, +R]
    case class Left [+L](value: L) extends Either[L, Nothing]
    case class Right[+R](value: R) extends Either[Nothing, R]

    It seems we should accept this code.

Then, what I'd propose right now is to:

1. Infer the capture set of a class based on the capture sets of parents, fields and methods
2. If that capture set mentions nothing related to some type parameter (where related = subtype of?) and the class is abstract, add that type parameter to the capture set

[odersky]

There's another rule for eliding capture sets

When converting tests to shallow capture sets I repeatedly stumbled over situations like this:

def f[C <: Any retains *] = 
  val x: () => C = ...

That almost never makes sense. () => C only has very uncommon instances, such as () => () where C is instantiated to Unit.
So in almost every situation, this gives a type error down the road. Of course, we need to define it like this:

def f[C <: Any retains *] = 
  val x: (() => C) retains C = ...

We could do one of two things to improve the situation here

1. Warn against a naked occurrence of a type A => B where B is tracked but A is pure. It should most likely be (A => B) retains B instead.
2. Silently fill in the missing retains. I.e. a user-written type A => B where B is tracked but A is pure is taken to be (A => B) retains B.

I think (2) will ultimately be more popular, since even with warnings, a type like (A => B) retains B is clunky to read. In that case we can make use of Function types as the escape hatch. I.e. if you really mean A => B without a retains clause, use Function1[A, B] instead.

[abgruszecki]

Approach 2) sounds more preferable here. Would it be feasible to somehow infer the capture information if the type has no explicit retains annotation? From what you wrote, I understand that you have in mind some sort of decision procedure that would fill in the annotations. What I'm thinking of is more like:

1. If the user-annotated type has any retains information, use that and don't proceed further.
2. Add retains annotations at every function arrow in the type, and use type inference to fill in the information
3. Use the result as the val's type

Why I'm suggesting this: it seems to me that in the example you describe, type inference would find a strictly better type if no type annotation was present. For instance, if x only captured a c : C, then the type should be (() => C) retains c.type.

[odersky]

I think that makes sense. The latest commit I am working on would not synthesize capture sets from the function result if the function is itself wrapped ina retains.

[abgruszecki]

The suggested syntactic shorthands and their escape hatches make sense to me. The basic assumption guiding them (a curried function only performs side effect at its end) seems solid.

1. (A => B => C => C) retains cap === (A => (B => (C => C) retains cap) retains cap) retains cap w/ the suggested escape hatch

   It's unlikely that a curried function only obtains a capability at the last stage.

2. (Int ==> A) => B => C => C === ((x: Int ==> A) => (B => (C => C) retains x) retains x

   Likewise, it's unlikely that a curried function uses a capability to create a function that consumes the rest of its arguments.

[odersky]

We have now shallow capture sets in PR #12875 and the rule proposed in #12871 (comment) as PR #12892.

I am still unsure about the the precise formulation of this rule. Currently is says: If A is pure and B is tracked then A => B is understood as a shorthand for (A => B) retains cv(B) unless the function appears in a user-written retains clause.

In try3.scala we have a handler with two arguments of types: CanThrow[E] ?=> T and E => T. According to our rule, E => T is rewritten to (E => T) retains T but CanThrow[E] ?=> T is left as is since CanThrow[E] is tracked. This might be surprising.

A more aggressive rule would be: If cv(B) does not subcapture cv(A) then A => B is understood as a shorthand for (A => B) retains cv(B) unless the function appears in a user-written retains clause.

Aside: I find ia good way to think about subcapturing (which is in fact modelled like this in the compiler) is to turn things around. If A and B are capture sets then A accounts for B if B <: A. Then the rule above is more intuitive:

If cv(A) does not account for cv(B) then A => B is understood as a shorthand for (A => B) retains cv(B) unless the function appears in a user-written retains clause.

Subcapturing is always a bit hard to wrap

E => R

[abgruszecki]

If cv(A) does not account for cv(B) then A => B is understood as a shorthand for (A => B) retains cv(B) unless the function appears in a user-written retains clause.

I like this rule more than the one that has special-case behaviour for pure A. Intuitively, if A doesn't account for B, then the function itself must have captured B. The only exception I can think of right now is if the function actually returns a subtype of B, a subtype that actually is accounted for by A. That seems like a rare case though, and probably deserves a more verbose type.