3 ms·

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):

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.

tel 12y ago
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.
- jonsterling 12y ago
  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.).
  - tel 12y ago
    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.

tel 12y ago

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.

jonsterling 12y ago
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.).
- tel 12y ago
  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.