Jon Pretty

@LukaJacobowitz I thought about the problems with type subtraction in Scala some more. The types A and B represent sets of properties provable on values of those types. They must have a least upper-bound, which will be the (nonempty) intersection of those sets. (1/11)

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)