Introduction
I dug into the topic further to try to find its origins. I was not quite satisfied with the Python discussion that mostly pointed at Scala, but I thought that would make a good starting point. I ended up seeing the origins of this from the Curry-Howard Isomorphism suggesting that logical or is indeed the historical operator.
Scala 3
I was trying to read into the early origins of the use of | in Scala 3. One important note is that in Scala 3 they also have intersection types, which uses & as an operator.
TypeScript
Note that TypeScript similarly used | and & for Union and Intersection types.
Scala.js
Some of the precedent seems to go an earlier implementation in scala.js:
There the original operator proposed was \/.
Curry-Howard Isomorphism (correspondence)
Reading further back, I found this blog post by Miles Sabin in 2011:
https://milessabin.com/blog/2011/06/09/scala-union-types-curry-howard/
This in turn refers to the Curry-Howard isomorpism relating type theory and structural logic.
https://en.m.wikibooks.org/wiki/Haskell/The_Curry–Howard_isomorphism
There the operators are ∨ and ∧, \vee and \wedge respectively. ∨ is the logical disjunction operator.
Note that logical disjunction in terms of boolean algebra is what we usually use | for now.
See W. A. Howard. The Formulae-as-Types Notion of Construction. 1969, 1980.
If we keep reading, I think we will see some origin of using | in ML, particularly Standard ML.
Summary
The use of | for type unions originates from the following.
- The Curry-Howard Isomorphism relates type theory with structural logic. Through the isomorpism a type union corresponds with logical
or. - In programming languages, we usually have written
∨as|.
Several here have proposed using ∪, the set theory union. Note the visual similarity to ∨. Apparently this is not a coincidence. However, Curry-Howard refers to logic not sets.
Above there are arguments that | is the bitwise or as currently documented. I think that definition only makes sense for bitstype instances. Rather the correct definition should be | refers to “logical or” or “logical disjunction”.
I see the points about sum types, tagged unions, but I do not currently see that becoming a fundamental part of the language in Julia 1 beyond its implementation in a package such as SumTypes.jl.
In light of this background, I am more in favor of using | for this purpose than before I started digging into the topic.