Proposed alias for union types

[mkitti]

@MilesCranmer

Is a PR with a formal proposal from the interested parties the right next step then? We’ve certainly reached a length where it’s evidently hard for people to read the entire thing. I’m wary of this as we are drifting into a meta-discussion about the true meaning of forum polls…

The clearest pull request might be the new method for Base.:| along with tests. Another route would be a Github Discussion RFC for a technical discussion.

What I think we should try to converge on here is what would be the best technical definition to put forth IF we were to try to move forward along with a coherent motivation.

@MilesCranmer

• Edit 6: Changed Base.:|(t::Type, types::Type...) into Base.:|(::Type{A}, ::Type{B}) to reduce surface

Miles has changed the definition a few times, so I think it might be worth discussing the implementation.

1. Base.:|(t::Type...) = Union{t...} # Original
2. Base.:|(t::Type, types::Types...) = Union{t, types...} by Mark Kittisopikul
3. Base.:|(::Type{A}, ::Type{B}) where {A,B} = Union{A, B} by Mason Protter, current

Most of the work is still done by Union{...}. My thought here is that we should minimize additional compilation and despecialize. This is the opposite of the other related discussion on specialization.

4. @inline |(@nospecialize(t::Type), @nospecialize(ts::Type...)) = Union{t, ts...}

It would be good to work out as much as possible here before taking another step.

Whether that pull request would go anywhere is a whole other matter. It might be useful to have a more technical discussion there and perhaps get some comments from triage.

@Mason

I don’t really understand this statement. There’s also an isomorphism between the union of sets and the union of types, and that isomorphism is arguably more straightforward than the one between structural logic and types, so I don’t see why that would be used to disqualify ∪.

Maybe the isomorphism doesn’t have as fancy a name though, so that may be a downside.

What would convince me is if you could find some precedent where ∪ is used in the context of type theory. My first choice here would be the following precedent in programming languages. My second choice is to follow precedent from the mathematical notation used in type theory. What I do not want to do is make up a new notation in a vacuum.