Tangent(0.3 spec) uses something akin to this. (disclaimer: this is my own little research project)

Currently with acts as a union operator modelling inheritance, though pragmatism has made it not commutative. Once you introduce implementations to methods, a strict union of methods with the same name is often not what you want and impossible to do right anyways.

intersect is supported that models type inference for something like foo(T,T) where the parameters are different.

Complements were interesting, but led to partial types that seemed not so useful and/or troublesome to include correctly – so are not included.

I know there are a few other research languages I ran across that had something similar, but cannot remember them at the moment. The main issue is that the things aren’t really useful without structural typing, which isn’t terribly popular itself. The other is that you need some sort of kind (type of types) to store the constructed type, or else it’s just shorthand for something that isn’t particularly idiomatic without that capability. And that’s far less common than even structural typing.

It’s biased, and it’s not much, but there it is.

Yes, Ceylon is a language with ad hoc union and intersection types, as described in this chapter from the Ceylon tour:

http://ceylon-lang.org/documentation/1.0/tour/types/

It’s amazing the number of cool idioms you get out of this. Here’s one interesting example I blogged recently. And here’s a short presentation where I quickly gloss over several simple idioms.

Even better, union/intersection types are the “missing link” that makes generic type argument inference really work right in Ceylon as opposed to other languages which combine subtype and parametric polymorphism.

Note that there are limitations to this sort of “type arithmetic”, as you’ve described it. For example, you can’t have a set complement operator at the type level, at least not without introducing undecidability.

HTH

Scala supports it partially (intersections but not unions), and any language with structural subtyping (I think OCaml is an example) or a type system powerful enough to emulate that (Haskell is a classic one) will have full “types-as-sets” capabilities, at least within the fragment of its type system that accepts such things (relevant when it’s emulated ala HList/OOHaskell).

Since I don’t know OCaml very well, I’ll give the portion of your example that works in Scala:

trait A {
  def a(): Unit
  def b(): Unit
}

abstract class B { // just to prove it works with both traits and classes
  def b(): Unit
  def c(): Unit
}

type C = A with B
type D = { def b(): Unit } // not an exact translation, because unions aren't directly available
// type `E` is unrepresentable

A version for Haskell would depend on the record system you were using, and would likely be somewhat clunky, because it would be emulated rather than natively supported.

As far as I know, Ceylon has both intersection and union types built into the language in full power, so you could presumable encode a type-level “xor” in terms of those.

Java supports intersections of interface types in some contexts, though it does not so far as I can tell allow the creation of variables of intersection types. Intersection types may come into play, for example, when using the ? : operator. If the second and third operands to that operator are unrelated interfaces which inherit from overlapping sets of interfaces, the result of the operator will be the set of interfaces which are common to both.

Common Lisp allows you do define new type using not, and, and or operators (see Type specifiers That Combine).