Let's quote the Scala spec for As Seen From (ASF) rules numbered for an easier reference:
The notion of a type T in class C seen from some prefix type S makes sense only if the prefix type S has a type instance of class C as a base type, say S′#C[T1,…,Tn]. Then we define as follows.
- If S = ϵ.type, then T in C seen from S is T itself.
- Otherwise, if S is an existential type S′ forSome { Q }, and T in C seen from S′ is T′, then T in C seen from S is T′ forSome {Q}.
- Otherwise, if T is the i'th type parameter of some class D, then
- If S has a base type D[U1,…,Un], for some type parameters [U1,…,Un], then T in C seen from S is Ui.
- Otherwise, if C is defined in a class C′, then T in C seen from S is the same as T in C′ seen from S′.
- Otherwise, if C is not defined in another class, then T in C seen from S is T itself.
- Otherwise, if T is the singleton type D.this.type for some class D then
- If D is a subclass of C and S has a type instance of class D among its base types, then T in C seen from S is S.
- Otherwise, if C is defined in a class C′, then T in C seen from S is the same as T in C′ seen from S′.
- Otherwise, if C is not defined in another class, then T in C seen from S is T itself.
- If T is some other type, then the described mapping is performed to all its type components.
If T is a possibly parameterized class type, where T's class is defined in some other class D, and S is some prefix type, then we use > "T seen from S" as a shorthand for "T in D seen from S".
Rule 1 is the base case for the recursive definition of ASF. Altough you cannot write ϵ.type in a Scala program, the ASF might be sent to the first rule by rules that strip the prefix: 2, 3.2 and 4.2.
Rule 2 is about seeing through existential types. Let's consider an example:
class X
object Rule2 {
abstract class A[V] {
val t: V
}
val a: A[W] forSome { type W <: X } = null
val x: X = a.t
}To typecheck val x: X = a.t we need to understand the type of a.x.
- First, we ask for
A.VinAas seen froma.type. The prefixS'isϵ.type. Rule 2 applies with the existential typeS' forSome {Q}decomposed into the typesS' = A[W]andQ = { type W <: X }. Note that the twoS's are not the same -- the first is the prefix of the ASF, the second the prefix of the existential type -- his is an unfortunate name clash in the spec. We recursively apply ASF to the prefixA[W]of the existential type. - We ask for
A.VinAas seen fromA[W]. Rule 3.1 extracts the type parameterWand returns it. Check explanation of Rule 3 for details. - We complete the application of Rule 2 by substituting prefix
A[W]withWin the existential type and we returnW forSome { type W <: X }as ASF's final answer.
We can simplify the returned existential type by applying Simplification Rules (SRs) specific to existential types. SLS 3.2.10 contains the definition of SRs.
- By application of SR4, we subsitute the upper bound
Xof the typeWin the prefix of the existential typeW forSome { type W <: X }and we simplify the existential type toX forSome { type W <: X }. - By application of SR2, we drop the unused quantification
type W <: XinX forSome { type W <: X }and simplify the existential type toX forSome {}. - By application of SR3, we drop the empty sequence of quantifications in
X forSome {}and further simplify the existential type toX.
The third rule is about resolution of a type parameter for a given type argument.
object Rule3 {
abstract class A[T] {
abstract class B {
abstract class C1 {
val t: T
}
abstract class C2 extends C1
val c: C2
}
val b: B
}
abstract class AA[T] extends A[T]
val x1: AA[X] = null
// the type of x1.b.c.t.type is type A.T in C1 as seen from x1.b.c.type
val x2: x1.b.c.t.type = null
val x: X = x2
}In order to typecheck val x: X = x2 we need to understand the type of x2.
- We're asking about type A.T in C1 as seen from the prefix S = x1.b.c.type, the is S' = x1.b.type (so C1 = x1.b.type#C1 and C1 is a base class for S). We apply 3. with D = A, and then 3.2 and we get:
- Ask for a type A.T in B as seen from S = x1.b.type (S' = x1.type). We apply 3 with D = A, and then 3.2 and we get:
- Ask for a type A.T in A as seen from S = x1.type (S' = ϵ.type). We apply 3 with D = A, and then 3.1 because A[X] is a base type of x1.type so we get: X as a final answer.
In the example above, we only excercised rules 3.1 and 3.2 but not 3.3. That rule is a fallthrough rule that is triggered when prefix doesn't encode any interesting information about how to resolve a type parameter. For example, you can ask for "A.T in X as seen from x.type". The definition of ASF ties together class C and the prefix type S but leaves type T to be arbitrary. You can ask ASF for an unrelated type. The 3.3 cannot be triggered directly by writing a type in user program because in order to access a type parameter, you have to be inside the class and then other rules will apply.
The fourth rule is about resolution this. Let's use an example again:
object Rule4 {
abstract class A {
abstract class B1 {
abstract class C1 {
val a: A.this.type
}
abstract class C2 extends C1
val c: C2
}
abstract class B2 extends B1
val b: B2
}
abstract class AA extends A
val x1: AA = null
val x2: x1.b.c.a.type = null
val x: AA = x2
}In order to typecheck val x: AA = x2 we need to understand the type of x2.
- We're asking about the type A.this.type in C1 as seen from the prefix S = x1.b.c.type, the is S' = x1.b.type (so C1 = x1.b.type#C1 and C1 is a base class for S). We apply 4. with D = A, and then 4.2 and we get:
- We're asking about the type A.this.type in B1 as seen from the prefix S = x1.b.type (S' = x1.type) We apply 4. with D=A, and then 4.2 and we get:
- We're asking about the type A.this.type in A as seen from the prefix S = x1.type (S' = ϵ.type) We apply 4. with D=A, and then 4.1 and we get: x1.type as a final answer
Similarly to 3.3, the 4.3 rule is not covered by the example. It's again a fallthrough rule. It can be triggered by asking about "X.this.type in AA as seen from x1.type".
We saw that rule 3. in ASF definition is about resolution of type parameters. Where's resolution of type members defined? Let's study this with an example:
object TypeMemberOverride {
abstract class B {
type U
// when you write `U`, this a shorthand for `B.this.type#U` (see Scala spec 3.2.3)
val u: U
}
abstract class BB extends B {
type U = X
}
val x1: BB = null
val x2: X = x1.u
}In order to typecheck the val x2: X = x1.u we have to understand the type of x1.u. We ignore the object TypeMemberOverride to shorten the considered paths so we're looking at x1.u instead of TypeMemberOverride.x1.u, etc.
- We're asking about B.this.type#U in B as seen from the prefix S = x1.type, the S' = ϵ.type so B = ϵ.type#B and B is a base type for S.
- The B.this.type#U is a selection of a type member U from a type B.this.type. By 5. we select U from B.this.type in B as seen from the prefix S = x1.type (the ASF is applied to the
B.this.type). - We're asking now for B.this.type in B as seem from the prefix S = x1.type, the S' = ϵ.type. We apply 4.1 with D = B, x1.type has D as one of its base types, so the answer is x1.type
- We're now at x6.type#U, and we select BB#U because BB is a base type of x6.type and BB#U subsumes B#U (see SLS 5.1.4). We get X as the final answer.
Wait, the empty path? Isn't it
S' = Rule2, or do I miss something? I guess you're ignoring that. Also, technically it seems we're in fact asking ASF forV, notA.V. I know what you mean, but I'm asking just to be sure I'm following along how to apply these rules formally. I'm also not 100% sure on what the empty path means.