Jon Pretty

They also have a greatest lower-bound, which is the union of the properties, and (in Dotty) is the intersection type, A & B. (2/11)

If we want to "remove" a type from the intersection, then we need to define ∖ such that (A & B) ∖ B = A. If we try to define that for abstract types in terms of the existing type machinery we have, we can't do it. The result of T ∖ S depends on the T ∩ S. (3/11)

So we would either need to create a new fundamental type structure for representing such types, preserving it until such time as the types are reified, or we restrict usage of ∖ to concrete types, in the same way that type projection (#) is. (4/11)

Supporting the former is a lot of work, I think. It would be a new concept which would need proving (probably at great length) for all of DOT's existing type operations. I'm not certain, but I think that's not an option. (5/11)

If we restrict it to concrete types, it seems a little ugly that it would be another constraint on abstract types. And unfortunately, I think methods like, def foo[T, S](f: F[T], s: S): F[T \ S] = ??? are quite likely to be most—if not all—of the useful cases. (6/11)

Another issue is that the type T \ S probably wouldn't do what we want anyway. A field, val t: T \ S could still quite happily, by Liskov Substitution, hold a value of type S, if that value is also a subtype of T. We couldn't prevent it without redefining Liskov. (7/11)

In general, the compiler could prove that T <: (T \ S), and that (T \ S₂) <: (T \ S₁) ∀ S₁ <: S₂, and that may be useful. But reasoning about more complex types such as wildcards in variant positions, or S \ (T \ U) is less obvious. Not necessarily impossible, though. (8/11)

Note that all this complexity arises because the types aren't disjoint. And that's not a distinction the compiler makes, so we can't even limit the usage of ∖ to disjoint sets of types. (9/11)

So, in general, I think this isn't viable without fundamentally adding complexity to the type system. If there were a way to restrict its use to disjoint types, it might be possible, maybe even sitting "on top of" the existing type system, like exaustivity checking does. (10/11)

But without that constraint, I think that having a value s conform to both S and T \ S would be confusing to say the least. (11/11)