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!

In terms of algebra, union and intersection types form a bounded distributive lattice. If we were to add negation, it would turn it into a boolean algebra. Certainly not impossible :)

wouldn't you need a top element for a boolean algebra though? else there's no identity on intersect and some and some of the complement laws are tricky to do. what would such an element look like for types?