Confusion about type refinement syntax

On Type Level, i stumble upon the following:

sealed abstract class StSource[A] {
  type S
  def init: S            // create the initial state
  def emit(s: S): (A, S) // emit a value, and update state
}

object StSource {
  type Aux[A, S0] = StSource[A] {type S = S0}

  def apply[A, S0](i: S0)(f: S0 => (A, S0)): Aux[A, S0] =
    new StSource[A] {
      type S = S0
      def init = i
      def emit(s: S0) = f(s)
    }
}

The line that intrigued me is type Aux[A, S0] = StSource[A] {type S = S0}

In paerticular {type S = S0} in StSource[A] {type S = S0}

I do not really know how to read this, as in interpreting the construct involved here.

What is StSource[A] {type S = S0} ??? is that a structural type (part of it looks like it)

When defining type like trait, or class, Is the body of a class part of the type constructor represented by the class itself? what happened to the method in it ?

Really confused. Can someone deconstruct that please ?

StSource[A] {type S = S0} is a refined type. {type S = S0} is a type refinement.

From one side, StSource[A] {type S = S0} is a subtype of StSource[A].

From the other side, StSource[A] is also an existential type with respect to StSource[A] {type S = S0}, namely StSource[A] is StSource.Aux[A, _] (aka StSource.Aux[A, X] forSome {type X}).

def test[A, S] = {
  implicitly[StSource.Aux[A, S] <:< StSource[A]]
  implicitly[StSource.Aux[A, _] =:= StSource[A]]
  implicitly[StSource[A] =:= StSource.Aux[A, _]]
}

https://scala-lang.org/files/archive/spec/2.13/03-types.html#compound-types

A compound type 𝑇1 with … with 𝑇𝑛{𝑅} represents objects with members as given in the component types 𝑇1,…,𝑇𝑛 and the refinement {𝑅}. A refinement {𝑅} contains declarations and type definitions. If a declaration or definition overrides a declaration or definition in one of the component types 𝑇1,…,𝑇𝑛, the usual rules for overriding apply; otherwise the declaration or definition is said to be “structural”.

See also examples how to use refined types:

https://typelevel.org/blog/2015/07/19/forget-refinement-aux.html

How can I have a method parameter with type dependent on an implicit parameter?

When are dependent types needed in Shapeless?

Why is the Aux technique required for type-level computations?

Understanding the Aux pattern in Scala Type System

Enforcing that dependent return type must implement typeclass

When defining type like trait, or class, Is the body of a class part of the type constructor represented by the class itself? what happened to the method in it ?

You can replace

def apply[A, S0](i: S0)(f: S0 => (A, S0)): Aux[A, S0] =
  new StSource[A] {
    override type S = S0
    override def init = i
    override def emit(s: S0) = f(s)
  }

aka

def apply[A, S0](i: S0)(f: S0 => (A, S0)): StSource[A] {type S = S0} =
  new StSource[A] {
    override type S = S0
    override def init = i
    override def emit(s: S0) = f(s)
  }

with

def apply[A, S0](i: S0)(f: S0 => (A, S0)): StSource[A] {
  type S = S0
  def init: S
  def emit(s: S): (A, S)
} =
  new StSource[A] {
    override type S = S0
    override def init = i
    override def emit(s: S0) = f(s)
  }

but there is no sense in that because the type remains the same

def test[A, S0] = {
  implicitly[(StSource[A] {
    type S = S0
    def init: S
    def emit(s: S): (A, S)
  }) =:= (StSource[A] {type S = S0})]
}

When you add type S = S0 to the type you provide additional information (that type S is specific) but when you add def init: S, def emit(s: S): (A, S) to the type you don't provide additional information (methods init, emit being there is clear from the definition of class StSource[A]).

Other situation would be if the class were defined as just

sealed abstract class StSource[A] {
  type S
}

or even

sealed abstract class StSource[A]

Then

StSource[A] {
  type S = S0
  def init: S
  def emit(s: S): (A, S)
}

would be a type different from StSource[A] or StSource[A] {type S = S0} (a subtype of them). It would be a structural type (existence of init, emit would be checked using runtime reflection). Here

{
  type S = S0
  def init: S
  def emit(s: S): (A, S)
}

is a refinement but not type refinement.

Unlike defs (init, emit) type members don't have runtime representation (unless you persist them, e.g. with TypeTags) so using type refinement doesn't have runtime overhead.