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

## Introduction

Recently, I found myself in need to precisely understand Scala's core typechecking rules. I was particulary interested in understanding rules responsible for typechecking signatures of members defined in classes (and all types derived from them). Scala Language Specification (SLS) contains definition of the rules but lacks any examples. The definition of the rules uses mutual recursion and nested switch-like constructs that make it hard to follow. I've written down examples together with explanation how specific set of rules (grouped thematically) is applied. These notes helped me gain confidence that I fully understand Scala's core typechecking algorithm.

## As Seen From

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:

```scala
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.t`.

  * We ask ASF 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 -- this is an unfortunate name clash in the spec. ASF applies itself recursively to the prefix `A[W]` of the existential type.
  * ASF's query is `A.V` in `A` as seen from `A[W]`. Rule 3.1 extracts the type parameter `W` and returns it. Check the explanation of Rule 3 for details.
  * ASF completes the application of Rule 2 by substituting prefix `A[W]` with `W` in the existential type and returns `W forSome { type W <: X }` as its final answer.

We can simplify the returned existential type by applying Simplification Rules (SRs) specific to existential types. [SLS 3.2.10](http://www.scala-lang.org/files/archive/spec/2.11/03-types.html#existential-types) 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.

```scala
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'll be looking at the type of the term `t`).

  * We ask ASF for `A.T` in `C1` as seen from the prefix `S = x1.b.c.type`. The prefix `S'` is `x1.b.type` (so `C1` can be selected from `S'` with the type projection `x1.b.type#C1` and `C1` is a base class for `S`). Rule 3 applies with `A.T` being the first type paramemter of the class `A`; the class `D` is `A`. The prefix `S` doesn't have an application of the parametric type `A` amongst its base types so Rule 3.1 doesn't apply. Rule 3.2 applies because the class `C1` is nested in the class `B`. ASF applies itself recursively to the same type `A.T` but in the class one level up in the class nesting relationship.
  * ASF's query is `A.T` in `B` as seen from the prefix `S = x1.b.type` (so `S' = x1.type`). By the same reasoning as in the step above, first Rule 3 applies and then Rule 3.2 applies because the class `B` is nested in the class `A`. ASF applies itself recursively to the same type `A.T` but in the class `A`.
  * ASF's query now is `A.T` in `A` as seen from the prefix `S = x1.type` (so `S' = ϵ.type`). Rule 3 still applies because `A.T` is the first type parameter of the class `A`. Rule 3.1 applies because the type `A[X]` is a base type of the prefix `S`; ASF extracts the type argument from the type `A[X]` and returns `X` as its final answer.

In the example above, we only excercised rules 3.1 and 3.2 but not 3.3. The Rule 3.3 is a fallthrough rule that is triggered when a prefix doesn't encode any relevant information about how to resolve a type parameter. For example, you can ask for the type `A.T` in the class `X` as seen from the prefix `x.type` to trigger Rule 3.3. The definition of ASF ties together the class `C` and the prefix type `S` but leaves the type `T` arbitrary. You can ask ASF for a type unrelated to the passed prefix. 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.

### Rule 4: `this` resolution

The fourth rule is about resolving `this`. Let's see it in action based on this example:

```scala
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'll be looking at the type of the term `a`).

  * We ask ASF for `A.this.type` in `C1` as seen from the prefix `S = x1.b.c.type`. The prefix `S'` is `x1.b.type` (so `C1` can be selected from `S'` with the type projection `x1.b.type#C1` and `C1` is a base class for `S`). Rule 4 applies to the singleton type `A.this.type` with the class `A` extracted from it (so `D = A`). Rule 4.1 is skipped because the class `A` is not a subclass of the class `C1`. Rule 3.2 applies because the class `C1` is nested in the class `B1`. ASF applies itself recursively to the same type `A.this.type` but in the class one level up in the class nesting relationship.
  * ASF's query is `A.this.type` in `B1` as seen from the prefix `S = x1.b.type` (so `S' = x1.type`). By the same reasoning as in the step above, first Rule 4 applies and then Rule 4.2 applies because the class `B1` is nested in the class `A`. ASF applies itself recursively to the same type `A.this.type` but in the class `A`.
  * ASF's query is now `A.this.type` in `A` as seen from the prefix `S = x1.type` (so `S' = ϵ.type`). Rule 4 still applies because the singleton type `A.this.type` matches the definition of the rule (with the class `D = A`). Rule 4.1 applies with the class `A` being its own subclass and `A` found amongst base types of the prefix `S` because the class `AA` is a subclass of `A`. ASF's final answer is `x1.type`.

Similarly to Rule 3.3, Rule 4.3 is not covered by the example above. It's again a fallthrough rule. Rule 4.3 can be triggered by asking ASF for `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:

```scala
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 ask ASF for `B.this.type#U` in `B` as seen from the prefix `S = x1.type`. The prefix `S'` is `ϵ.type` (so `B` can be selected from `S'` with the type projection `ϵ.type#B` and `B` is a base class for `S`). The type projection `B.this.type#U` is a selection of a type member `U` from the singleton type `B.this.type`. Rule 5 applies to the singleton type `B.this.type`.
  * ASF's query is now `B.this.type` in `B` as seem from the prefix `S = x1.type`. The prefix `S'` is `ϵ.type`. By the same reasoning as explained `this` resolution section, first Rule 4 applies to the singletion type `B.this.type` with the class `B` extracted from it (so `D = B`) and then Rule 4.1 applies so the answer for this ASF's step is the singleton type `x1.type` (the prefix `S`).
  * ASF completes the application of Rule 5 by returning `x1.type#U` as its final answer.

Now we're done with ASF and we select the member `U` of either the class `BB`, or the class `B` because both classes have instances that are base types of the type `x1.type` (see [SLS 3.4.3](http://www.scala-lang.org/files/archive/spec/2.11/03-types.html#base-types-and-member-definitions) for definition how members of a type are defined). We pick `U` as a member of of the class `BB` because member `U` of the class `BB` subsumes member `U` of the class `B` (see [SLS 5.1.4](http://www.scala-lang.org/files/archive/spec/2.11/05-classes-and-objects.html#overriding). And we get `X` as the final answer by resolving the type alias `U` defined in the class `BB`.

_Thanks to Nada Amin for raising the bar on my note taking skills and Adriaan Moors for comments._