Add exclusion/not type

[Iltotore]

Suggestion: add a way to exclude a type from an union. This could be caracterised by a "not" type to preserve the already used -.

Examples:

trait A
trait B extends A
trait C extends A

A & !B → A and not B. This is equivalent to A - B in mathematics.
A | !B → A or not B. This is equivalent to *
!A | B → Not A or B. Equals to * - (A - B) in mathematics. It forbids all A except B

[Iltotore]

Edit. After small researches about implementing this feature. I think it should become an infix operator like intersection and union:

trait A
trait B extends A
trait C

//A ! B -> A without B.
//B ! A should throw an error because A is a superclass of B
//A ! C should be treated as A by the compiler (maybe a compile-time warning ?)

Reasons of this change

• Other examples showed above aren't relevant and the new schema is type-safer as it doesn't allow unbound type.
• From what I have seen in the compiler, this model should easier to implement.

Goal

The goal is to implement an operator equivalent to the exclusive operator from the set theory in mathematics. Here the proposed model uses the ! operator to avoid possible clash with the contravariant operator -.

Example

Note: Gray means "excluded"

A

A ! B

A ! C (equivalent to A)

[LPTK]

See also the discussion on the contributors forum: https://contributors.scala-lang.org/t/union-types-and-generalisations/3820/9

[jeremyrsmith]

A couple of summary points from the thread that @LPTK mentioned (because it was a while ago!):

1. The original use case was around (to paraphrase) inferring (as a return type from a def) a union type that excludes a particular (possibly inferred) type, given as a type parameter to the method.
2. It was pretty well agreed that a general "not" unary type operator (e.g. ~A meaning "the union of all types which aren't A") is at least intractable, and possibly unsound.
3. The inference use case that was presented for "excluding a type", can already apparently be implemented (at least, in certain variance cases, and with careful attention). After that thread, I found I could even implement in Scala 2.11 the intersection type use case that I brought up, as long as variance was just-so and the with was in a certain order for the value parameter. (This is a pretty opaque thing to say, so LMK if an example is warranted)
4. It was pretty well agreed that there are pretty dramatic runtime implications of an "exclusion" operator (or even a relative complement operator) if they're used anywhere but for inference (and even possibly when they're only used for inference?) because of subtyping and non-sealed things (think SI-7046 but at runtime!)

[Iltotore]

Hello.

(This is a pretty opaque thing to say, so LMK if an example is warranted)

I think I understood but I would like to know how an example using your impl on 2.11 looks.

[jeremyrsmith]

@Iltotore

// this is only to verify the expected type.
import scala.reflect.runtime.universe.{TypeTag, typeTag}

trait SpookyFunction[-In, +Out] {
  def andThen[NextIn <: In, NextOut](
    next: SpookyFunction[Out with NextIn, NextOut]
  ): SpookyFunction[NextIn, Out with NextOut] =
    new SpookyFunction[NextIn, Out with NextOut] {}
}

trait A; trait B; trait C; trait D; trait E

object Foo extends SpookyFunction[A with B, C]
object Bar extends SpookyFunction[C with D, E]

object Example extends App {
  // to see what's inferred
  def showType[T : TypeTag](t: T): Unit = println(typeTag[T])

  // Expected: TypeTag[SpookyFunction[A with B with D,C with E]]
  // Why? Because even though Bar requires C, it is provided by Foo and so it can be eliminated.
  showType(Foo andThen Bar)
}

This works in Scala 2.11, 2.12, 2.13, and 3. (The type inference part, not necessarily the syntax and TypeTag stuff)

[jeremyrsmith]

Note that it's very important in Scala 2.x to say:

next: SpookyFunction[Out with NextIn, NextOut]

rather than

next: SpookyFunction[NextIn with Out, NextOut]

(i.e. if you don't put the "thing to eliminate" first, it won't work.)

Not sure if this caveat applies to Scala 3 or not.

[LPTK]

A couple of summary points from the thread that @LPTK mentioned

Well it looks like we haven't read the same thread.

2. It was pretty well agreed that a general "not" unary type operator (e.g. ~A meaning "the union of all types which aren't A") is at least intractable, and possibly unsound.

This was not well-agreed at all. A general negation type would in fact be a lot more tractable than smart matching in type inference. Currently, matching components in these types breaks in surprising ways if types are reordered (violating the commutativity property), because it's the problem of smartly matching unions and intersection during type inference that is intractable, not negation types.

The potential soundness issue is more of a technicality in DOT as far as I can see. It's a safe initialization problem, and there are already many like it, so negation types don't meaningfully change anything here: #11716

4. It was pretty well agreed that there are pretty dramatic runtime implications of an "exclusion" operator (or even a relative complement operator) if they're used anywhere but for inference (and even possibly when they're only used for inference?) because of subtyping and non-sealed things (think SI-7046 but at runtime!)

Again, I think you have it backwards. Negation types do not any dramatic runtime implications; smarter type matching does, and it's necessary for a good library implementation of type subtraction.

[jeremyrsmith]

@LPTK I agree with you that it would be useful (I suggested it on the thread, even). But a lot of folks smarter than me pointed out soundness issues with it. Apologies if I was mistaken about the level of consensus.

[LPTK]

You say "a lot of folks" pointed out soundness issues, but only two people made concrete arguments regarding soundness issues AFAIK.

• LukaJCB was just confused (as remarked by Martin, he mixed up & and |).

• Blaisorblade was pointing out a technicality in the DOT encoding to show that the soundness of negation types was "tricky". But it's been well-known for a long time that DOT without an initialization checker is tricky, and can't even encode paths of length greater than one! So there are no surprises there.

[Iltotore]

The mentioned thread is a bit inactive so I will continue to write here.

Icharan proposed a negation type ~A usable like this:

x match {
  case ~A => doStuff()
}

This is readable but for the reasons talked above, I think an "exclusion type" should be more appropriate so I sent an example of pattern matching with this:

x match {
  case _ \ A => doStuff() //Or Any \ A
}

This notation is the same like exclusion with Maths and it takes only one more character.

I also find it more readable in more complex situations:

trait A
trait B extends A
//Other child traits...
x match {
  case A & ~B => doStuff()
}

versus

trait A
trait B extends A
//Other child traits...
x match {
  case A \ B => doStuff()
}