TypeScript 1.4 sneak peek: union types, type guards, and more
blogs.msdn.com
blogs.msdn.com
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.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.
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.).
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.
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).