Pre-SIP: Existential types based on path-dependent types

Scala Improvement Process
1

Introduction

The reasons for removing existential types from the language state that:

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

It is assumed that a class with type members can be used instead.

class Container {
  type T
  val x: Either[T, T]
}
// instead of
Either[T, T] forSome { type T }

But this approach requires extra boxing, which adds runtime overhead and is less convenient to use.

Proposal

It seems that using similar semantics of path-dependent types can significantly simplify the implementation of existential types and improve expressiveness. For example, it is possible to use a rule similar to capture conversion: substitute the type member selection for the bound type variables.

def both(e: Either[T, T]): T = ???
def test(x: Either[X, X] forSome { type X }): x.X = {
  both(e)
}

// impossible in Scala 2, but it works with new semantics
// https://stackoverflow.com/questions/39110719/skolemization-of-existentially-typed-expressions
val pair: (A => String, A) forSome { type A } = ( { (a: Int) => a.toString }, 19 )
pair._1(pair._2)

Existential types can also help with the problem of capturing the right capabilities in recent work on reach capabilities.

def fst(@use p: (() ->{C} Unit, () => Unit) forSome { type C^ }): () ->{p.C} Unit = p._1
// instead of
def fst(@use p: (() => Unit, () => Unit)): () ->{p*} Unit = p._1

Implementation

There is a draft implementation using this approach.

Complications

There are also things that are expressible in Scala 2 where skolemization is used, but not expressible in the proposed approach. But it seems that there are not many such cases, and simplification of theory and implementation is much more important.

var x: (A, A => B) forSome { type A; type B } = ???
x match {
 // x is not a valid type prefix, since it is not an immutable path
 case (a, f) => f(a)
}

Future work

Also, as a future work, one could consider adding context bounds for type members of existential types, as in the first-class existential types proposal in Haskell, which suggests the possibility of adding constraints on existentials.

2 Likes