In a discussion with Aly on discord, the following bit of code came up and compiled:
class A[C^](c1: C)
I find it very hard to understand what this code means - in fact, it feels like this shouldn’t compile, because we’re using a capset variable in place of a concrete type.
Can anyone explain how to understand what type c1 is?
I must admit I have no real understanding of capture sets, but in Scala a “decoration” on a type without the type usually means that Any is being decorated
For example {val x: Int} =:= Any{val x: Int}
So you’re saying this might mean:
class A[C^](c1: Any^{C})
Or did I misunderstand?
Yes I think so, but it does seem weird upon closer inspection
The C^ in unbound type param position I guess means that you require c1 to be a capability. Reading from the doc pages here
“The type of a capability must be a capturing type with a non-empty capture set”
So:
The first expression does not compile because c1 does not have a non-empty capture set. The second expresion compiles becasue it is of the “fallback” type CapSet
The type of a capability must be a capturing type with a non-empty capture set
This is where the vocabulary gets a little confusing (for me), by the way - C is not a capability in the sense of inputs to context functions, and I get confused about which kind of capability we’re talking about - the ones from capture sets, or the ones for actual capabilities?
This has led to people asking me surely A^{Rand} is the same as Rand ?-> A…
But to your answer: so C^ here is basically C <: CapSet. This I had gathered through @Aly 's experiences (and the fact that it’s stated explicitly in the doc once I figured out how to read it). But I would, perhaps naively, expect [C^] to mean that C only appears as a capture set, and to fail to compile if it’s used as a type, and [C <: CapSet] to express the subtyping constraint. Simply for clarity for users.
So, in my head:
class A[C^](c: C) // does NOT compile
class A[C <: CapSet](c: Foo^C) // does NOT compile
class A[C <: CapSet](c: C) // does compile
class A[C^](c: Foo^C) // does compile
I’m not trying to imply that it’s how it should be, merely how it was in my mental model and how I end up getting confused, again.
I guess you may be confusing the type and term level. A capture set contains terms that must be capabilties (so the are of a type that is a sub-type of CapSet). So C is not a capabilty (it is a type with a non-empty capture set), but the term c1 must be a capability as you said it is of type C^.
(I hope I’m right… not 100% sure)
Mmm… this is how I understand it, but I’m very open to the idea of being wrong:
[C^] is a capture set, which is conceptually not a type, but something you use to decorate types with (although yes, internally, it is a subtype of CapSet).SharedCapability and its siblings. It’s really a set of tracked terms.C, in our example (that is, [C^]), is not, I think, a type with a non-empty capture set, but an actual capture set - what the documentation refers to as capability polymorphism. And my original question is about how confused I am that it can also be used as a type.
Now your explanation makes sense: if I understand correctly, it’s desugared to C <: CapSet, which is a type. This explains why the compiler accepts it where a type is expected. It’s just really confusing (for me, obviously, but I expect also for people not intimately familiar with how this all works).
But this compiles:
I’m not too surprised by this: you’re merely saying that B is parametric on C, and C is tracked. Unless I’m missing something obvious again, this is only tangentially related to what we’re discussing.
The difference between B and A is that with class A[C^](c1: C) you require that what is bound to C when applied is a type that has a non-empty capture set (i.e a “capability”).
But I would think that the C^ in param position would require the same…
Really?! that is not at all what I understood from the documentation. I honestly, genuinely thought A[C^] meant that C is a capture set, so that you can parameterise over the capture set of your inputs - a little like @Odersky explained here.
With my (incorrect?) mental model, it makes perfect sense that B(new Impure) compiles. B’s constructor takes any tracking type. But since you can pass non-tracking types where tracking types are expected, you really can pass any type to the constructor.
Aha. Thnx. Yes there seems to be another concept “reach capability” when type param hats are involved. I’m really not deeply into this yet, obviously.
Perhaps the difference is between “must capture” and “can capture”. So C^ in unbound type param position perhaps means “must capture” and C^ in bound value type position means “can capture”.
It’s explained here. When you write f[C^] this is treated as a type parameter with CapSet as upper and lower bound:
f[C >: CapSet <: CapSet^]
Since C expands to a regular type parameter it can be used as a type for another parameter. I am not sure whether there are real use cases for this.
When you write
f[C^]this is treated as a type parameter withCapSetas upper and lower bound
Yeah I ended up working that out in the end, between the documentation and the help of @Sporarum and @bjornregnell 
From a user’s perspective, this is (quite clearly) a little confusing - it feels like mixing apples and oranges. I assumed it was done this way because it simplified the underlying implementation.
Perhaps the difference is between “must capture” and “can capture”. So C^ in unbound type param position perhaps means “must capture” and C^ in bound value type position means “can capture”.
I genuinely don’t think so, unless something drastic (other than the name of cap, wink wink) changed recently:
C^ as a type parameter means C is a capture set.C^ as a type means C is tracking - has a capture set.I will admit that I’m not fully certain what you mean by unbound type param position and bound value position here and am assuming the former is what I mean with as a type parameter and the latter as a type, but if not, then I have not at all understood what you meant.