# Proposed alias for union types

**URL:** <https://discourse.julialang.org/t/proposed-alias-for-union-types/108205>\
**Category:** Internals & Design\
**Tags:** question, proposal\
**Created:** [December 31, 2023, 1:43pm UTC](https://discourse.julialang.org/t/proposed-alias-for-union-types/108205 "2023-12-31T13:43:56Z")\
**Posts on this page:** 1\
**Showing post:** 80

<div class="post-metadata">

**Author:** ![mkitti](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/mkitti/32/12459_2.png) [@mkitti](https://discourse.julialang.org/u/mkitti)\
**Post date:** [January 3, 2024, 2:34am UTC](https://discourse.julialang.org/t/proposed-alias-for-union-types/108205/80 "2024-01-03T02:34:55Z")

</div>

# Introduction

I dug into the topic further to try to find its origins. I was not quite satisfied with the [Python discussion](https://mail.python.org/archives/list/python-ideas@python.org/thread/FCTXGDT2NNKRJQ6CDEPWUXHVG2AAQZZY/) 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.

- [Intersection Types - More Details](https://dotty.epfl.ch/docs/reference/new-types/intersection-types-spec.html)
- [Union Types - More Details](https://dotty.epfl.ch/docs/reference/new-types/union-types-spec.html)

## TypeScript

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

> **[Documentation - Everyday Types](https://www.typescriptlang.org/docs/handbook/unions-and-intersections.html)**
>
> The language primitives.

# Scala.js

Some of the precedent seems to go an earlier implementation in scala.js:

> <https://github.com/scala-js/scala-js/issues/1824>
>
> Edit: the original proposal was to name it \`\\/\`.
> 
> It would be worth thinking abo…ut a union type constructor for facade types. Similar to \`js.UndefOr\[+A\]\` in its construction, \`js.|\[+A, +B\]\`, or whatever it's called, would represent a value of type \`A\` or \`B\`. It would have zero API, though. The basic idea is the following:
> 
> \`\`\` scala
> @RawJSType // don't do this at home
> sealed trait |\[+A, +B\]
> 
> object | {
> implicit def fromA\[A\](a: A): A | Nothing = a.asInstanceOf\[A | Nothing\]
> implicit def fromB\[B\](b: B): Nothing | B = b.asInstanceOf\[Nothing | B\]
> }
> \`\`\`
> 
> Then of course we need ways to transitively convert an \`A\`, a \`B\`, or a \`C\` to an \`A | B | C\`. This probably needs a bit of recursive implicit magic. Even trickier: convert \`A | B\`, \`A | C\` and \`B | C\` to \`A | B | C\` ^^

There the original operator proposed was `\/`.

# Curry-Howard Isomorphism (correspondence)

Reading further back, I found this blog post by Miles Sabin in 2011:

> **[Unboxed union types in Scala via the Curry-Howard isomorphism - Miles Sabin](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.

> **[Haskell/The Curry–Howard isomorphism - Wikibooks, open books for an open world](https://en.wikibooks.org/wiki/Haskell/The_Curry%E2%80%93Howard_isomorphism)**

There the operators are `∨` and `∧`, `\vee` and `\wedge` respectively. `∨` is the logical disjunction operator.

> **[Logical disjunction](https://en.wikipedia.org/wiki/Logical_disjunction)**
>
> In logic, disjunction (also known as logical disjunction, logical or, logical addition, or inclusive disjunction) is a logical connective typically notated as 
>   
>     
>       
> ∨
>       
>     
> {\\displaystyle \\lor }
>   
> and read aloud as "or". For instance, the English language sentence "it is sunny or it is warm" can be represented in logic using the disjunctive formula 
>   
>     
>       
> S
> ∨
> W
>       
>     
> {\\displaystyle S\\lor W}
>   
> , assuming that 
>   
>     
> ...

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.](https://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf)

If we keep reading, I think we will see some origin of using `|` in ML, particularly [Standard ML](https://en.m.wikibooks.org/wiki/Standard_ML_Programming/Types).

# 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](https://math.stackexchange.com/questions/3867554/the-formal-difference-between-cup-and-vee). 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.

---

_[View the full topic](https://discourse.julialang.org/t/proposed-alias-for-union-types/108205)._