4 ms·
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 t
by 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 agoI 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.