Jon Pretty

In Scala, is it possible to "subtract" a type from a composed type like this one: "A with B with C" ?

No, it's not possible.

A with B is the type which represents the set union of the properties of A and the properties of B. We can construct A with B with A, and (by set theory) it's identical to A with B. So including A in the intersection again is idempotent. (1/2)

Therefore, the inverse operation of "intersecting with A" is not well-defined. In general, if you "remove" A from A with B, you're left with... A with B. (2/2)

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...