Proposal to add Intersection Types to the Language


#1

Here’s a proposal to add intersection types to Scala 3. An intersection type A & B replaces a compound type A with B. Intersection types have nice algebraic properties, in particular, they are commutative. Intersection types have been studied formally in DOT and are implemented in Dotty.

Here’s a link to the doc page: https://dotty.epfl.ch/docs/reference/intersection-types.html

Motivation

Intersection types have a solid theory and nice algebraic laws. They greatly improve in both respects on compound types.

Migration

For the moment, the compound syntax A with B is still available, in order to allow cross building between Scala 2 and 3. But it maps already to the intersection type semantics of A & B. Compound types will be deprecated in Scala 3.1. There is a already an implemented rewrite rule to move from with to &.

This proposal is open for discussion in the community and will be discussed in our next SIP meeting, where we’ll take all your feedback into account for the approval/dismissal of this feature.


Second batch of Scala 3 SIPs: additions to Scala's type system
#2

I don’t understand something. with is not commutative and when we generate new classes/traits the order is important.

trait A {
  val foo = 1
}
trait B extends A {
  override val foo = 2
}
trait C extends A {
  override val foo = 3
}
trait BC extends B with C
trait CB extends C with B

Why do we limit writing val bc : B with C and val cb : C with B ?


#3

For this purpose I propose to deprecate types/classes named & in Scala 2.14.


#4

You mean, why not allow A with B in addition to A & B under the old non-commutative meaning? It would complicate the type system to no small degree. You’d have to think through all the interactions with other features. How does A with B relate to A & B? Can A with (B & A) be simplified? And so on…

Also, used as a type A with B does not seem to be that useful on its own. For what it’s worth in Dotty we always map it to A & B and have not found an incompatibility because of it.

Finally, we have the invariant that any class inheriting A with B must be a subtype of A & B. So the two types would be very closely related anyway.


#5

OK, understood.


#6

Maybe that’s not the right place to clarify this but it may help understanding the proposal’s motivation. I don’t understand in what way compound types are not commutative. If I open a sbt console with scala 2.12.6, I can do the following:

scala> trait A
defined trait A

scala> trait B
defined trait B

scala> class C extends A with B
defined class C

scala> new C: A with B
res0: A with B = C@273fe26

scala> res0: B with A
res1: B with A = C@273fe26


#7

The discussion in Dotty issue #5139 is relevant to this SIP (and it appears that no conclusion has been reached there).


#8

You are talking about (up)casting, but commutativity is rather about type calculus.

For instance, if you have some method like

def x[A, B](implicit ev: (A with B) =:= (B with A)) = ()

then you cannot do something like

x == ()

because you have a compilation error

Cannot prove that A with B =:= B with A.

Compiler does not think this types are equivalent. This is a lack of commutativity.


#9

If you provide type parameters it works, so I share @markarasev’s question.

scala> x[Int, String] == ()
res5: Boolean = true

scala> implicitly[(Int with String) =:= (String with Int)]
res6: Int with String =:= String with Int = generalized constraint

#10

The problem is that the “user-level reflection” of the type system relation =:= is not really accurate. It actually tells you whether A <:< B and B <:< A, which is not the same thing as the type system’s idea of two types being the same. See this ticket, in which I document getting confused by this myself :slight_smile:

scala> :power
Power mode enabled. :phase is at typer.

scala> trait A
defined trait A

scala> trait B
defined trait B

scala> typeOf[A with B] =:= typeOf[B with A]
res0: Boolean = false

scala> typeOf[A with B] <:< typeOf[B with A]
res1: Boolean = true

scala> typeOf[B with A] <:< typeOf[A with B]
res2: Boolean = true

#11

AFAIK, a type is a set of possible values. Since A with B and B with A have the same possible values, they must be the same type. Or do you have a different definition of type?

There only is a difference when you are extending A with B. The way I see it, is that A with B is not just a type, but a type plus some extra information on how to extend it.


#12

Because the with operator is not commutative in Scala 2, these types don’t have the same values. The order of the types in the intersection matters. Linearisation will come up with e.g., different result types for methods (last one wins).

Dotty fixes this by pushing down the intersection/union to union/intersection (for contravariant occurrences) or intersection/union (in covariant positions) in signatures of the type’s members. This is commutative.


#13

A reference of type A with B can accept exactly the same values as a reference of type B with A. If you want to dispute that, then show me a value that one can accept but not the other one.


#14

Here’s a contrived example of what I was thinking of:

scala> trait Base { def foo: Any }
defined trait Base

scala> trait A extends Base { override def foo: Int = 1 }
defined trait A

scala> trait B extends Base { override def foo: Any = "1" }
defined trait B

scala> new A with B
           ^
       error: overriding method foo in trait A of type => Int;
         method foo in trait B of type => Any has incompatible type

scala> new B with A
res1: B with A = $anon$1@7e62cfa3

scala> lazy val fooAB = (??? : A with B).foo
fooAB: Any = <lazy>

scala> lazy val fooBA = (??? : B with A).foo
fooBA: Int = <lazy>

These types don’t behave the same way in terms of generating values, nor in the typing of member selection. I believe these differences will go away in Scala 3.


#15

@adriaanm Good example. Yes, these differences go away.

The tutorial page was a bit too simplistic here. Essentially, in DOT/Scala 3: A & B == B & A in the sense that they are mutually subtypes of each other. That implies that they “have the same values”.

In Scala 3, A with B and B with A are also mutually subtypes of each other. But as you note, applying an operation like member selection can give different results for A with B and B with A. This is excluded for intersection types.


#16

I see what you mean.

I see that the difference between A with B and B with A matters not only after extends, but also after new. But it should still not matter for reference types.

That fooAB is inferred as Any, is a bug in the type inference. It must be Int.


#17

No, the type is inferred as specified. Compound types follow linearisation to determine member signatures.


#18

But that doesn’t make sense. Since A with B is a subtype of A, we know that foo needs to return Int.


#19

But that doesn’t make sense. Since A with B is a subtype of A , we know that foo needs to return Int .

That’s precisely the problem with A with B.


#20

I see - this is about way more than commutativity.

So what will happen to with in new or extends clauses?