Those are good points, but I think your assumption is a bit off. I would argue, that Vehicle =!= (Vehicle & ~Tank).
If we assume a Set S than S != S/X.
Therefore the following shouldn’t be permitted:
trait Vehicle
class Tank extends Vehicle
def enterGarage(v: Vehicle & ~Tank) = ???
val tank = new Tank
enterGarage(tank: Vehicle) // what now? => TypeError
Because the function should’t be able to take any vehicle, but only concrete subclasses, that are indeed not of type Tank.
if that’s the idea, you need to make sure they can’t be extended with Tank tho. If Tank is a trait, such a subclass must be final. Or sealed with no descendent extending it and Tank.
Yes, I thought about that after initially responding. But I doubt that you can (or whether it would be a good idea to) add that to a typesystem in general. As far as I know Scala’s typesystem doesn’t generally care about whether a type is a final class or not. While for Vehicle & ~Tank to function like you want to, only final (or sealed) classes can be a subtype. That feels like a strange complication to the type system.
More concretely, right now when I ask the typesystem if A is a subtype of B, I don’t think it matters if the types or their constituents are classes, traits, sealed or final. While in the query X <: (Vehicle & ~Tank) the answer depends on whether X, Vehicle and Tank are classes or traits, and whether they are final or sealed.
Maybe I am wrong here, but one can check if a class extends Tank, right?
So ~Tank would also exclude everything, that is a subtype of Tank.
Since Vehicle must be sealed for this to work, the checker would only need to check if the input to enterGarage is a sub type of Vehicle and does not extend Tank
In theory at least; I don’t know how hard this would be to implement.
Yes, if Tank is a class, then any class C that does not extend Tank is a subtype of ~Tank, even if neither Tank nor C is final or sealed.
My fear is that such a type would be rather unreliable. Since _ \ T would not be a real type constructor, but more like an annotation intended for type inference, we would have to make sure it subsists long enough through type transformations to remain useful in common scenarios. But since type inference often has to make some premature choices and cannot backtrack (as @smarter says), that would not likely be a reliable mechanism.
A general-purpose complement also is limited by the no-backtracking requirement, but there are ways to normalize type expressions which may alleviate (though not eliminate) this. @Blaisorblade pointed me to this paper: Sound and Complete Flow Typing with Unions, Intersections and Negations.
Even that is not enough, since we have all sorts of complex type constructors in Scala, which means we can construct an S such that S <: Vehicle and S =!= Vehicle and X </: Tank that still is not a subtype of `~Tank~. Off the top of my head we can at least easily declare
sealed abstract class Vehicle { def name: String }
final class Tank extends Vehicle { def name: "tank" = "tank" }
// other kinds of vehicle
Now S = Vehicle { def name: "tank" } is a strict subtype of Vehicle (S <: Vehicle but Vehicle </: S), that is not a subtype of Tank (S </: Tank), and yet we cannot say that S <: ~Tank, let alone S <: Vehicle & ~Tank.
And that example even uses a sealed Vehicle class and a final class Tank!
I only used _ \ T as a transient support for the thought process. At the end of the day I would not introduce _ \ T at all. I would only rely on the R | T-based mechanism.
That’s right, this S is not a subtype of ~Tank. That’s as intended — you would not want your enterGarage function to accept something that is not not a Tank (i.e., that could be a Tank).
But how would that mechanism work, specifically? The subtractT method you gave does not work as is, as pointed out by @smarter.
Of course it’s as intended. I showed that example as a counter-example for my post’s parent who said that
It seems to me that we could at least make type inference smart enough that, in the situation where it needs to unify a union type A | B with another union type T | U, that if B =:= U then it pushes downward the unification of A with T (or, of course, the other combinations). I’m not sure what backtracking really entails here, but I assume that anyway it’s got to do some combination of subtyping checks, so in that process it should be able to eliminate some unifications. Hopefully.
Given the example:
sealed abstract class Vehicle { def name: String }
final class Tank extends Vehicle { def name: String("tank") = "tank" }
S = Vehicle { def name: "tank" } is structurally a subtype of Tank, but not nominal.
So nominally we can say S <: ~Tank.
But what is the standard to compare entities with each other: syntactical or structural?
I agree that it would be nice if Dotty tried harder to match the components of unions and intersections during subtyping checks. It may solve the original problem of this thread in common cases, and would also make life simpler for people who use the “phantom intersection” trick I mentioned earlier.
AFAIK there is no notion of unification in the type inference of a language like Scala, which is based on subtyping. There is only subtyping constraint solving. From what I can gather, when the current algorithm finds something like A | B <: T | U, it first tries to widen the LHS, then tries to join the LHS (i.e., compute the non-union LUB of A and B), and otherwise decomposes the constraint as A <: T | U /\ B <: T | U (which is sound but not complete). It does not seem to match components in a smart way.
FWIW, there is at least one documented case where some sort of “smart matching” happens (tho not that one).
OTOH, there are also performance costs — so that code does not use B =:= U, it just tests pointer equality of types — and IIRC thanks to hash-consing, that checks structural equality.
Sure you can. If T is a concrete type, then
u match {
case t: T => ...
case s => ... // s: ~T
}
Furthermore,
type A = U & ~T
type B = V & ~T
type C = A | B
Guess what! C <: ~T.
So I don’t agree that it’s not useful. It may require somewhat different patterns than we’re used to, but complement in set theory has been around, and has been very useful, for a very long time. I’d be surprised if suddenly became pointless now.
(A | B) \ B is not the same set as A (unless A and B are non-intersecting), so anything that remotely resembles complement should behave the same way (i.e. B should actually be missing). You should have to write (A | B) \ (B \ A) to get back to A in the general case. (A | B) \ B is fine for the case where A and B are provably non-intersecting, but if we are happy with dealing with non-intersecting stuff only, there’s no problem with ~A either.
With that you’ve not proven that S <: ~T. You’ve only proven that s.type <: ~T. Now what are you going to do with that knowledge?
I only used \ as a thought process, and said at least twice that we cannot construct it as is and that my actual “implementation” of a similar but different thing is less precise than that. I only argued that my alternative is useful/precise enough for the use cases discussed.
This is true… the use cases mostly involve mechanically removing a type from a union or intersection, but that’s not what a true relative complement would do when subtyping is involved.
At least, the use cases I wanted when I asked about it were around just removing the type from the list. So if even if B <: A, I’d be happy with some way to specify that I want A from A | B, or A | C from A | B | C. But that’s not a real relative complement in this case, because you can still pass B as an A and it wouldn’t necessarily be desirable to add a runtime restriction.
I think the concrete use cases only wanted ~T as a guide for type inference – when either A | B | C or A | C could satisfy a type constraint for a type variable X, you could say something like X <: ~T in order to make sure the latter is inferred. Dotty can already be “convinced” to infer the smaller list:
(based on)
but some mechanism for specifying this less awkwardly was what I was after with ~T.
Edit: it’s also not clear if it works like that for unions rather than intersections – I haven’t tested it
Pass it in to a method that has an argument type of ~T, of course! Just like you always do when your types are refined via pattern matching.
That’s a strawman. What is that method then going to do with it? Pass it further around? If all you do is pass a value around it’s useless. Can you call a method on s that you could not otherwise? Select a field of it? Select a type member? Decompose it in any other way?
Sure you can. If
Tis a concrete type, then
Because you consider a single instance, but to argue for the whole subtyping relationship, see:
Int | Float !<: String | Int
Int | Float !<: ~(String | Int)
The point @sjrd refers to is that the semantic complement ~A known from set theory is different than just to say we remove A from the type set Type by refining: NewType={T:Type | T!=A} .
Good grief. It’s not a strawman at all. You use it to select the right code path, not to gain new functionality, just like the fall-through path of a match statement. You could just as well say “what is the point of case x => ...”. Can you call a method on x that you could not otherwise? Of course not, but that’s not the point!
So, for instance,
// Ensure that we cannot double-box `Int` values
sealed trait Box[A] { def value: A }
object Box {
final case class BoxInt(value: Int) extends Box[A] {}
final case class BoxWhatever[A <: ~Int](value: A) extends Box[A] {}
def apply(value: Int) = new BoxInt(value)
def apply[A <: ~Int](value: A) = new BoxWhatever(value)
}
Now you can Box(5) and Box("salmon") without thinking about it, but if (a: Any) you can’t just Box(a), even if you can write a match { case i: Int => Box(i); case x => Box(x) }.
I’m not sure what the point of this is. If S and T are sets, S may be a subset of neither T nor ~T. That’s absolutely right. Why is it any different for types?