Jon Pretty

That doesn't strike me as true, `A with B` represents the set intersection. `A | B` represents set union. You claim idempotency is why you can't have negation, but both intersection and union are idempotent!

Well, to put it another way, we need to solve the equation, x with B = A with B for x. We want the solution to be x = A, but x = A with B is also a solution...

You would just need to normalize the type before applying the Negation, it doesn't seem like an insurmountable problem to me at all

I think you're misreading... there are literally two distinct solutions for x in that example, regardless of whether you normalize (plus potentially others). This could work if type intersections formed a free monoid, but it's not free...

We can use the same example with set intersection: x ∩ B = A ∩ B Yes, x could be both A or (A ∩ B) or (A ∩ A ∩ B ∩ B ∩ B), that doesn't mean that (A ∩ B) \ B = A. It is NOT subtraction, but difference or negation. I.e. the difference between a Group and a Boolean algebra

Ok, but what should (A ∩ B) \ B give if A = C ∩ B? A might be abstract. Here's a concrete example with types. What is, (Some[Int] with Product) \ Product ?

I think that would just be Some[Int] \ Product (maybe the scala compiler can prove this is Nothing, but it's not a deal breaker either way)

You mean Any, not Nothing, surely?