Clarify the reasons for dropping existentials

[TomasMikula]

Dotty documentation lists three reasons why existentials were dropped.

• Existential types violate a type soundness principle on which DOT
  and Dotty are constructed. That principle says that every
  prefix (p, respectvely S) of a type selection p.T or S#T
  must either come from a value constructed at runtime or refer to a
  type that is known to have only good bounds.

Can this be illustrated on an example? What's a snippet of code that uses existentials and is problematic in this respect?

• Existential types create many difficult feature interactions
  with other Scala constructs.

This is a little too vague of an explanation for users who are going to miss existentials.

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

I disagree that the gain is minor.

[smarter]

I disagree that the gain is minor.

Can you give an example where it gives a major gain?

[TomasMikula]

I can. I suppose that what is meant is that a type

F[A] forSome { type A }

can be replaced by

Exists[F]

where

trait Exists[F[_]] {
  type A
  val get: F[A]
}

The first problem with that is the extra boxing.

The second problem is that we need one version of such Exists for each number and shape of existentially quantified type parameters:

Exists2[F[_,_]]
Exists3[F[_,_,_]]
ExistsH[F[_[_]]]
ExistsHA[F[_[_], _]]
ExistsFoo[F[_[_,_], _[_], _]]
// ...
// not to mention versions with bounds and variance

I do find this a major loss.

Now, if only we could make Exists kind-polymorphic:

trait Exists[F <: AnyKind] {
  type A <: AnyKind
  val get: F[A]
}

but that won't work, because

An any-kinded type can be neither the type of a value, nor can it be instantiated with type parameters.

[smarter]

Wildcards are still supported so you can express your example as F[_]

[Blaisorblade]

There's a misunderstanding I think. Wildcards won't work as well for any type mentioning the existential type more than once, such as Map[Tag[A], A] forSome {type A}. I think in @TomasMikula's message F ranges over type lambdas, not just classes.

---

The first problem with that is the extra boxing.

Sure, and I guess one could in principle try to design features to address this if needed — something like Haskell's existentials comes to mind* — but my first guess is that the problem isn't important enough (either for that or for having existentials). I'm open to evidence.

---

I agree that documentation could say more, as always. I'm not sure what to write though, apart from the kind-monomorphic encoding you sketch. I also agree you can't abstract over it easily.

For more info on the motivation, one reference (off the top of my head, with some googling) is https://groups.google.com/d/msg/scala-language/PV4q6O1qIh8/yG4p8PA2Jf8J and its discussion of existentials. Among other things:

One particularly amusing twist is that this could in one fell sweep
eliminate what I consider the worst part of the Scala compiler.

Another email is:

https://groups.google.com/d/msg/scala-internals/lCIcSDHSCyg/kkN4382tVHUJ

Existential types do not behave nicely under tree rewritings, which is a potential troublespot for macros that rewrite trees carrying existential types. The problem has no easy fix. That was the "incompatibility with macros" that Josh and I were referring to. (In detail the problem is that "opened existentials" lead to type skolems and some common tree transformations such as substitutions do not extend cleanly to type skolems.)

I'm not 100% sure of the details, but it seems relevant that in Coq, substituting X by S in an existential variable ?Y (which is the equivalent a skolem) gives ?Y[X:=S], because once you replace ?Y by T you must apply the substitution to T.

Some discussion with more references is in http://guillaume.martres.me/publications/dotty-hk.pdf — basically, it explains that Scala "existentials" aren't usual existentials because they have no introduction and elimination forms (which, concretely, goes together with the fact that they're unboxed, though you could have as introduction form an unboxed (newtype-like) constructor) — and then it gives a reference to a paper by @RossTate and others.

Tate, Leung and Learner have explored some possible explanations in [11], but their treatment raises about as many questions as it answers.

I confess I don't know what those problems are. I know I looked at that paper years ago and it was pretty tough, and it's just for Java.

[TomasMikula]

I agree that documentation could say more, as always. I'm not sure what to write though, apart from the kind-monomorphic encoding you sketch. I also agree you can't abstract over it easily.

Then maybe it just shouldn't say that the gain is minor.

One particularly amusing twist is that this could in one fell sweep
eliminate what I consider the worst part of the Scala compiler.

Existential types do not behave nicely under tree rewritings, which is a potential troublespot for macros that rewrite trees carrying existential types. The problem has no easy fix. That was the "incompatibility with macros" that Josh and I were referring to. (In detail the problem is that "opened existentials" lead to type skolems and some common tree transformations such as substitutions do not extend cleanly to type skolems.)

Those sound like problems with the compiler implementation, moreover the old one, not necessarily the feature itself.

From the rest of your comment it seems like the real reason is that all the implications of existentials as present in Scala are unknown and the easiest was to just remove them altogether.

[Blaisorblade]

Actually, I should have corrected you earlier:

I suppose that what is meant is that a type F[A] forSome { type A } could be replaced by Exists[F] [...]

Not at all. You couldn't write a kind-polymorphic Exists earlier and you can't write it now (just like Forall is not kind-polymorphic), but you can translate each type F[A] forSome { type A }, where A is used multiple times, to

class WrapF {
  type A
  val v: F[A]
}

and transforming the client code accordingly. Not that the transformation is easy to define generally, but if you wrote such code using existentials, that should be easy enough to do.

I didn't say it earlier because I thought it obvious for this conversation, but I guess this is worth pointing out in the docs?

I agree on the limitations of kind-polymorphism, but since even higher kinds are still waiting for formal proofs (though we're planning an attack), and even in Scalac they have IIUC two users, I'm afraid progress there will have to wait.

Those sound like problems with the compiler implementation, moreover the old one, not necessarily the feature itself.

From the rest of your comment it seems like the real reason is that all the implications of existentials as present in Scala are unknown and the easiest was to just remove them altogether.

My impression is that those are concerns with writing down the typing rules, hence actually defining the semantics of the feature. And between doing, dunno, research or a full PhD on the topic, which might or might not work, and requiring the above encoding, the second seems better.
Scala already offers many ways (sometimes maybe too many) to do the same thing, but doing additional research on one seems overkill?

[TomasMikula]

I should have corrected you earlier [...]

I think the only disagreement there is about whether the gain from having existentials is minor.

I agree on the limitations of kind-polymorphism [...] and even in Scalac they have IIUC two users

It should not be surprising that a non-existent feature has 0 users. Like higher kinds in Java. Or generics in Go.

My impression is that those are concerns with writing down the typing rules, hence actually defining the semantics of the feature. And between doing, dunno, research or a full PhD on the topic, which might or might not work, and requiring the above encoding, the second seems better.

Let's explain as much in the docs ;)

Scala already offers many ways (sometimes maybe too many) to do the same thing, but doing additional research on one seems overkill?

I'm really not sure what you mean. Am I against additional research on existentials? No, I would be the first one to welcome it. The title of this issue is "Clarify the reasons for dropping existentials".

[sirinath]

Wondering if F[G[A, A]] forSome { type A } can be replaced with F[G[A: _, A: _]] or F[G[A: _, A]] as a shorthand to overcome some of the confusions.

[TomasMikula]

@sirinath I think the notation is the last concern, if there isn't an underlying representation in the compiler to support it.

[Blaisorblade]

Action items for me:

• elaborate on issues with the semantics of existential types;
• write down possible translations.

It should not be surprising that a non-existent feature has 0 users. Like higher kinds in Java. Or generics in Go.

They have a prototype in Typelevel Scala. But you're welcome to point to Haskell libraries using it — I don't really have an axe to grind, so if I'm happy to be wrong.

I think the only disagreement there is about whether the gain from having existentials is minor.

That's a hard debate to resolve, but maybe I can try writing something less subjective there. "We have decided to not support existentials given the open questions on the proper meaning of existentials in interaction with other features, and the alternative encodings that are available."

I'm really not sure what you mean. Am I against additional research on existentials?

Well, I was explaining why I, at present, would not recommend research on the topic, based on what the literature suggests. In a sense more research is likely better than nothing, but there are only so many researchers. If somebody makes progress in the upcoming decades, people might reconsider.

[TomasMikula]

Kind-polymorphism in Typelevel Scala is as unsuitable for encoding existentials as the one in dotty, so why even mention it? Due to its limitations, of course it has next to 0 uses. I don't need to point to Haskell libraries. I can name some uses of kind-polymorphism (that I would actually implement and use) off the top of my head: kind-polymorphic versions of Exists, Forall, =:=, <:<, Semigroup, Monoid, ..., NaturalTransformation (FunctionK), encode monad as a monoid (okay, maybe I wouldn't immediately use this last one in practice).

👍 to your effort to make the docs less subjective and more precise!

[TomasMikula]

Tangential thought: Doesn't GADT pattern matching use a lot of the same internal machinery as existentials?

[Blaisorblade]

Meanwhile, @allanrenucci asked a few questions and made me realize there might be a way to ignore boxing — whenever the existential doesn't appear at the top-level, move type T to the containing scope. Gotta ask Martin if/whether this could be automated.

Assume F is for instance type F = [X] => (X, X), so that F[_] doesn't work in Dotty.
Inside a method:

// Scala 2:
// Defining `Foo` isn't needed
def bar = { type Foo = F[_]; ... }
// Scala 3:
def bar = { type A; type Foo = F[A] }

For class fields:

// Scala 2:
class Bar {
  type Foo = F[_]
  val v: F[_]
}
//Scala 3:
class Bar {
  type A
  type Foo = F[A]
  val v: F[A]  
}

The only loophole I see are types appearing at the top-level, but I can only think of extends clauses.

Loopholes I fear are that now some code might fail after translating because of stability restrictions — new Bar().v must approximate the return type:

scala> type F = [X] => (X, X)
scala> class Bar {
           type A
           type Foo = F[A]
           val v: F[A] = null
         }
// defined class Bar
scala> new Bar().v
val res0: (_, _) = null // approximated type!
scala> val v = new Bar()
val v: Bar = Bar@d5ce97f
scala> v.v
val res1: F[v.A] = null

But I suspect any such restrictions might be necessary for soundness.

[Blaisorblade]

OK, what doesn't work if you lift type A to the outer scope is converting from F[T] to F[A] — for that you need to either set type A = T, or use the solution that involves boxing:

//scala 2:
(1, 1): F[_] // works
//scala 3
trait Bar {
  type A
  val v: F[A]
}
(new Bar { type A = Int; val v = (1, 1) }: Bar) // can abstract over this:
object Bar {
  def apply[X](a: F[X]): Bar = new Bar { type A = X; val v = a }
}
Bar((1, 1))

[TomasMikula]

there might be a way to ignore boxing — whenever the existential doesn't appear at the top-level, move type T to the containing scope.

I think that wouldn't work to translate

trait Bar {
  def go: List[F[A] forSome { type A }]
}

It is not equivalent to

trait Bar {
  type A
  def go: List[F[A]]
}

because in the first case the A might be different for each element of the list.

[Blaisorblade]

Also true. And I don't think CPS-transforming F[A] forSome { type A } into { def apply[A, Z](fa: F[A] => Z): Z } does any less boxing (apart from the inconvenience of writing the latter).

[RossTate]

Tate, Leung and Learner have explored some possible explanations in [11], but their treatment raises about as many questions as it answers.

Hah, I love this quote! I'd never seen it before, but I totally get it. Sorry the work doesn't help y'all except to warn just how complicated the problem gets.

I have other work on checking/inferring existential types, but unfortunately it doesn't work for impredicative existential types, which is the case y'all particularly care about. Nonetheless, there are probably some useful lessons to learn from the predicative case if y'all are interested.

[Blaisorblade]

@RossTate Well "X is hard" can be as useful as "here's how to do it".

Having googled, I guess your other work is https://pdfs.semanticscholar.org/89f8/13248f34a352232f18a6c0771925d0e982b4.pdf and http://cseweb.ucsd.edu/~rtate/publications/italx/existentialstr.pdf? Found those from https://scholar.google.com/citations?user=EiXpVxwAAAAJ..., and then saw the link in http://www.cs.cornell.edu/~ross/publications/italx/ . So you're saying that case is interesting even after looking at your later paper (which I didn't really study)?
You're arguably right since I'm not sure how many people want to instantiate existentials with other existentials (is that what you mean)? And how many expect type inference to work there?

Linking here those papers for when we get back to the question.

[RossTate]

So the key insight/restriction we rely on is that predicative types have limited locations in which existentially quantified variables can go, and that a subtyping between predicative types gives a mapping between these locations. Subtyping and inference then stem from reasoning about and manipulating those mappings.

Unfortunately with impredicative types, pretty much every location is existentially quantifiable. So maybe there's some way to formulate how you'll restrict existential subtyping so that more informative mappings can exist, but without that it's very hard to transfer over my work :(

[sir-wabbit]

@TomasMikula You can make a newtype for existentials which works pretty well in Scala2 and doesn't box.

    type Type[+F[_]] <: (Any { type T })

    def wrap[F[_], A](value: F[A]): Type[F] =
        value.asInstanceOf[Type[F]]

    def unwrap[F[_]](value: Type[F]): F[value.T] =
        value.asInstanceOf[F[value.T]]

[TomasMikula]

@alexknvl OK, that addresses the boxing issue.

[OlivierBlanvillain]

Existential types create many difficult feature interactions with other Scala constructs.

This is a little too vague of an explanation for users who are going to miss existentials.

Another way to read that line is "they are pretty damn hard to implement" :)

I don't think we should spend too much time explaining why they are hard, so I'm going to close this issue.