Proposed alias for union types

mkitti · January 3, 2024, 2:34am

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:

github.com/scala-js/scala-js

js.| union type

opened 04:44PM - 24 Jul 15 UTC

closed 08:41PM - 28 Jul 15 UTC

sjrd

enhancement

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:

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.