How do existential types overlap with path-dependent types?

Question

Starting Scala 3 existential types have been dropped and one of the reasons is stated as

Existential types largely overlap with path-dependent types, so the gain of having them is relatively minor.

Given "largely", so not always, I was wondering if a concrete example can be provided demonstrating how to rewrite an existential type as path-dependent type, and an example when such replacement is not possible?

Answer 1

Suppose that T is the type we want to bind by the existential quantifier, and F[T] is some type that depends on T, so that

type A = F[T] forSome { type T }

is our existential type.

Providing an instance of type A means that:

• there exists some type t that can be bound by T
• there exists a value of type F[t]

But we could just as well put both components into a single type, and make T a path-dependent type member:

type B = { type T; val value: F[T] }

Instances of type B are described by same data:

• Some type t that can be bound by the name T.
• A value of type F[t]

The values of both A and B carry around roughly the same information, the main difference is how we can access the type T over which we are quantifying. In case of b: B, we can get it as path-dependent type p.T, whereas for a: A, we could use type-variables in pattern matching.

Here is an example that demonstrates how to map between the existentially quantified and the path dependent types:

def example[F[_]]: Unit = {
  type A = F[T] forSome { type T }
  type B = { type T; val value: F[T] }
  def ex2pd(a: A): B = a match {
    case v: F[t] => new { type T = t; val value = v }
  }
  def pd2ex(b: B): A = b.value
}

(this compiles on 2.13)

I would guess that the "largely" is there, because unlike Scala 3 / Dotty, previous versions of Scala did not have any rigorously formalized foundations, so maybe the author of this sentence just did not want to invoke the impression that every existential type from 2.13 could be exactly represented by path dependent types, because such a claim could not be made rigorous anyway.