Proposal to remove Existential Types from the language


#1

Hello Scala Community!

I’d like to open the discussion for the pending SIP on dropping existential types from the language. You can read a full writeup on the details here.

Summary:

Existential types that can be expressed using only wildcards (but not forSome ) are still supported, but are treated as refined types.

Please read the link above for full details.

Implications

I’m aware of two issues (both from my time on SBT). Both of these issues arise from limitations in type inference and using existentials to be able to drop explicit type annotations in two scenarios:

Scenario 1: Higher kinded types

SBT relies on forSome for code like the following:

def joinAny[M[_]](inits: Seq[Initialize[M[T]] forSome { type T }]): Initialize[Seq[M[_]]]

Where “Initialize” is effectively an Applicative functor / Reader-style monad. In the past, existentials were the only way to get Scala’s type inference to handle these styles of methods.

Scenario 2: F-Bounded polymorphism/quantification

SBT has the following:
type Key = K forSome { type K <: Scoped.ScopingSetting[K] with Scoped }

This, again, was used to simplify defining these types and ensuring type inference preserved what was needed in the API.

I believe BOTH of these use cases (not explicitly outlined in the proposal) should be resolved with better type inference generally available in DOTTY. (I have not yet confirmed, but will get back to this thread once I have time too).

Opening this up for general community discussion and insight into any other use cases that would not be covered with wildcards or dependent types.


#2

See also the discussion in https://github.com/lampepfl/dotty/issues/4353


#3

The Java JWT library (https://github.com/jwtk/jjwt) contains the interface io.jsonwebtoken.SigningKeyResover which I could not implement in Scala without using existential types. The interface has a method

Key resolveSigningKey(JwsHeader header, Claims claims);

where JwsHeader is defined as

public interface JwsHeader<T extends JwsHeader<T>> extends Header<T> {
  ...
}

The Scala implementation of that method looks as follows:

new SigningKeyResolver {
   override def resolveSigningKey(header: JwsHeader[X] forSome { type X <: JwsHeader[X]}, claims: Claims): Key = ...
   ...
}

Will Dotty still allow to implement such a Java interface in Scala?


#4

wouldn’t you just use

override def resolveSigningKey[T <: JwsHeader[T]](header: JwsHeader[T]), claims: Claims): Key = ...

instead?


#5

The Scala compiler rejects to compile that variant:

Error:(53, 32) method resolveSigningKey overrides nothing.
Note: the super classes of <$anon: io.jsonwebtoken.SigningKeyResolver> contain the following, non final members named resolveSigningKey:
def resolveSigningKey(x$1: io.jsonwebtoken.JwsHeader,x$2: io.jsonwebtoken.Claims): java.security.Key
                  override def resolveSigningKey[X <: JwsHeader[X]](header: JwsHeader[X] /* forSome { type X <: JwsHeader[X] } */, claims: Claims): Key =

#6

I was expecting that a solution based on a type alias might work, but I couldn’t succeed:

type SomeJwsHeader = {
  type T <: JwsHeader[T]
  type Apply = JwsHeader[T]
}

And then:

trait ScalaSigningKeyResolver extends SigningKeyResolver {
  override def resolveSigningKey(header: SomeJwsHeader#Apply, claims: Claims): Key = ???
}

But I get the same error message :frowning:

method resolveSigningKey overrides nothing.
Note: the super classes contain the following, non final members named resolveSigningKey:
def resolveSigningKey(x$1: io.jsonwebtoken.JwsHeader[T] forSome { type T <: io.jsonwebtoken.JwsHeader[T] },x$2: io.jsonwebtoken.Claims): java.security.Key

I’m curious to know if there is a way to represent this JwsHeader[T] forSome { type T <: io.jsonwebtoken.JwsHeader[T] } type without using forSome.


#7

Since the Java interface has type:

Key resolveSigningKey(JwsHeader header, Claims claims);

I think the correct signature for the override is just:

def resolveSigningKey(header: JwsHeader[_], claims: Claims): Key = ???

This works in Dotty but not in Scala 2 and I think Scala 2 is wrong here to force you to write this crazy existential type, for the same reason that if I declare a class Foo[X <: Int], I can write Foo[_] to talk about any Foo and it’s equivalent to writing Foo[_ <: Int], I should be able to write JwsHeader[_] without specifying a bound for the wildcard.


#8

Hey @jsuereth!

I mentioned 2 more that are present in the sbt codebase:

  • Parser[Seq[ScopedKey[T]] forSome { type T }]
  • Initialize[Task[T]] forSome { type T }

Mentioned in https://github.com/scala/scala-dev/issues/443

I’d love to know how these would be rewritten in Dotty, without losing any expressiveness.


#9

I don’t think they can be rewritten directly. You’d have to introduce intermediate classes and thread them through the whole codebase. E.g.

  class KeyParser[T] {
    val parsed: Seq[ScopedKey[T]]
    ...
  }

These idioms and workarounds demonstrate the additional power of existential types which falls away.

To be clear: Removing existential types is not done in order to save a bit of syntax. The reason for removing them is that they have complicated interactions with almost everything else in the type system, including soundness, and that they overlap sufficiently with dependent types, so that the added complications stand in no relation to the added usefulness.


#10

Can type KeyParser[T] = Seq[ScopedKey[T]]; ... KeyParser[_] be used?


#11

No, that would be too easy… I.e. then it would be syntactic sugar, after all.


#12

Hey @djwijnand,

Those are actually the same “class” of issue as Scenario 1, so I just listed one of the examples. It’s for the same reason and I think is expressable in dotty without requiring the forSome. The primary reason you see the forSome in the type signature there is because you couldn’t write:

def joinAny[M[_]](inits: Seq[Initialization[M[_]]: Initialize[Seq[M[_]]

I’m hoping to find time this week to get a working rewrite in Dotty that solves the same use case but without requiring the existential.