[Answered] Disjunctions in types: Why is this "something that the type system cannot and should not support"?

Evolution Discussion
1

I have read the Commonly Rejected Proposals List and the linked announcement where Chris Lattner states that an anonymous disjoint/discriminated/type-safe union/ad-hoc either type/coproduct is "something that the type system cannot and should not support". I am wondering why that is. Several languages have similar concepts, such as:

  • TypeScript uses the T | U syntax
  • Haskell uses (# T | U #) syntax with the UnboxedSums extension
  • Python writes them T | U as well
  • Julia writes it Union{T,U}

Of course, these languages’ type systems differ from Swift’s and their union types, even if transferable to Swift’s type system, might not behave in the way we would want.

Such types seem particularly useful in light of the new typed throwing functions. It would be helpful to be able to write throws(OSError | DataError) or similar; as-is (if I understand it correctly) any throwing function that throws a different, non-supertype than the throwing functions it calls has to use try? or do-try-catch.

Of course that could also be improved by making try perform some automatic conversion not along subtyping relations, similar to the ? operator in Rust.

Does the Swift type system make a fundamental assumption, in the absence of which either users would be confused or implementation made more complex or inefficient, that is incompatible with the existence of such types?

Or is it believed that such types are inherently confusing or broken and cannot be implemented in an intuitive or sound way?

Or would we need to give up some guarantees or concepts that are incompatible with these types to introduce them, which would be unacceptably backwards-incompatible?

3 Likes
2

Using the search function on these forums for the specific quoted text will lead you to several discussions on the topic. See, for example:

2 Likes
3

Thanks.