Proposed alias for union types


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.


Note that TypeScript similarly used | and & for Union and Intersection types.


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:

This in turn refers to the Curry-Howard isomorpism relating type theory and structural logic.–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.


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.