Skip to content

Instantly share code, notes, and snippets.

@gkossakowski
Last active June 19, 2018 18:27
Show Gist options
  • Select an option

  • Save gkossakowski/2f6fe6b51d1dd640f462a20e5560bcf2 to your computer and use it in GitHub Desktop.

Select an option

Save gkossakowski/2f6fe6b51d1dd640f462a20e5560bcf2 to your computer and use it in GitHub Desktop.
Understand Scala's core typechecking rules

Scala's "type T in class C as seen from a prefix type S" with examples

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.

  1. If S = ϵ.type, then T in C seen from S is T itself.
  2. 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}.
  3. Otherwise, if T is the i'th type parameter of some class D, then
    1. If S has a base type D[U1,…,Un], for some type parameters [U1,…,Un], then T in C seen from S is Ui.
    2. 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′.
    3. Otherwise, if C is not defined in another class, then T in C seen from S is T itself.
  4. Otherwise, if T is the singleton type D.this.type for some class D then
    1. 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.
    2. 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′.
    3. Otherwise, if C is not defined in another class, then T in C seen from S is T itself.
  5. 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: Existential types

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.V in A as seen from a.type. The prefix S' is ϵ.type. Rule 2 applies with the existential type S' forSome {Q} decomposed into the types S' = A[W] and Q = { type W <: X }. Note that the two S'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 prefix A[W] of the existential type.
  • We ask for A.V in A as seen from A[W]. Rule 3.1 extracts the type parameter W and returns it. Check explanation of Rule 3 for details.
  • We complete the application of Rule 2 by substituting prefix A[W] with W in the existential type and we return W 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 X of the type W in the prefix of the existential type W forSome { type W <: X } and we simplify the existential type to X forSome { type W <: X }.
  • By application of SR2, we drop the unused quantification type W <: X in X forSome { type W <: X } and simplify the existential type to X forSome {}.
  • By application of SR3, we drop the empty sequence of quantifications in X forSome {} and further simplify the existential type to X.

Rule 3: Type parameters

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.

this

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".

Type members

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.
@Blaisorblade
Copy link

We ask ASF for A.V in A as seen from a.type. The prefix S' is ϵ.type.

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 for V, not A.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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment