Perhaps I'm poisoned by my love of strong static types, but... what would you ever use union types like that for? I'm having trouble imagining scenarios where a "list that might have strings or integers" is a good idea. (I know that's likely just a silly example, but I'm not able to think of any non-silly ones right now, either.)
Interop with existing JS libraries, mostly. JavaScript people do this all over the place. It's considered "convenient" to not have to pass an array for a function's argument when you only want it to operate on a single element. Whether that's a good idea or not is mostly a matter of taste, but it's a fact that it's a really common JS pattern and now TypeScript supports better-than-nothing typechecking for calling such functions. That's pretty cool.
To take your silly example, the first thing that comes to mind is error handling, kind of like Haskell's Either.
I could have a function
function foo(x):
if(x===0) {
return "Not a number";
}
return 360/x;
}
Then apply foo to every value in a list of numbers to get a result that it either a string or an integer. Finally, use another function that filters out all of the string values to get a list of valid integers.
This is perhaps not the best example since string and int are easy to distinguish. The real advantage is that a type like `Either Int a` is more useful than `Int | a` since if it is ever the case that `a = Int` the first is still useful while the second has collapsed.
Homotopy Type Theory has wonderful results about this due to their study of "truncation" which turns `Either a b` into `a | b` so as to mimic classical logic.
What is the meaning of `Int | a` in your parlance? Is it a propositional disjunction, or is it a non-disjoint union type? Or is it something else? And what is the connection to classical logic that you are drawing?
If you are referring to a propositional truncation of the disjoint union, then this doesn't need to come from HoTT, but can be done in any framework strong enough to support setoids (either directly, as in ETT and OTT, or indirectly as you do in ITT). HoTT is cool, but it seems like a lot of the hubbub about it is concerning things that we already had no trouble doing at all in type theory without the homotopy interpretation.
On the other hand, if you are talking about a true union type (not a sum type), then I think that the presence of "type guards" sort of ruins the interesting properties that distinguish union types from sum types (except, as you point out, the fact that Int|Int is pretty much (extensionally) equal to the Int type, etc.).
I was thinking truncation to prop. I am sure it doesn't actually take HoTT, but I'm indoctrinated there right now mostly due to the accessibility of the HoTT book. Homotopy feels like a sensible place to do this sort of thing due to the emphasis on higher equality types, but I'm again sure you don't need that much to talk about this.
The type guards are what ruin the original example, but you could get more sophisticated types where sum is more useful than union if it's challenging to distinguish between the two types. You could always build your own tags, but that might not belong on the values.
You would have to think of it in a higher context. This slides could be very insightful for your question about type union and how they are very useful:
A JSON value is best represented as a union type: boolean|string|number|array|dict.
Union types are the natural way to represent the parameters of functions that do typeof and instanceof checks, since you can easily write a list of the types that the function actually checks for.
TypeScript also has structural interface types, which are the natural way to represent the parameters of functions that don't use type guards (duck typing).
Yeah, I noticed the interface types, which seem like a much better/safer design choice. (Again, though, it's entirely possible this is just my strong-typing prejudices coming out.)
