This choice has nice ergonomics but brutal practical cost so that's why languages close to the metal do not want to do this and particularly don't want to go around defaulting to it whereas a language like Typescript is fine with it.
replyMaybe it has "brutal practical cost", I don't know, but even most high-level languages don't have set-theoretic type systems. Perhaps because the approach is relatively new and most popular languages are old.
replySum types in the set theoretic approach can be made with `(A & ¬B) | (¬A & B)`, or equivalently `(A | B) & (¬A | ¬B)`.
replyThere'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.
replyThis is cool. Unfortunately it's also too late now. The machines have taken over programming.