alt Hacker NewsSum types in the set theoretic approach can be made with `(A & ¬B) | (¬A & B)`, or equivalently `(A | B) & (¬A | ¬B)`.
There's no mainstream language with negation types, but a few good research languages with them, eg MLstruct.
[MLstruct]:https://github.com/hkust-taco/mlstruct
> MLstruct supports union, intersection, and complement (or negation) connectives. We make sure they form a Boolean algebra and add enough structure to derive a sound and complete type inference algorithm. For more details, please see the paper mentioned above.
This is cool. Unfortunately it's also too late now. The machines have taken over programming.