On: Sum Types Are Coming (2015)

[dbaupp]

Disjoint union in mathematics is exactly the universal construction you're calling sum types: https://en.wikipedia.org/wiki/Disjoint_union

(The Flow use of the name doesn't seem to quite match the mathematical definition.)

[catnaroek → dbaupp]

Confusingly, there are two different things called disjoint union in mathematics. One is what you mentioned, which is indeed the coproduct in the category of sets. But another one is simply the union of two disjoint sets, which might not be too common in programming, but is used quite a lot, say, in analysis and point-set topology. Flow's use of the term obviously refers to the latter.

[dbaupp → catnaroek]

The former is a (small) generalization of the latter, tacking on a tag to forcibly ensure the sets are disjoint. It's not worth thinking of them as different.

In any case, Flow doesn't require that the sides of the | are different.

[catnaroek → dbaupp]

Um, re-read the documentation:

> These disjoint unions are made up of any number of object types which are each tagged by a single property.

It is clearly a disjoint union in the set-theoretical, not category-theoretical sense.

Let's see their own example:

    // @flow
    type Success = { success: true, value: boolean };
    type Failed  = { success: false, error: string };
    
    type Response = Success | Failed;
    
    function handleResponse(response: Response) {
      if (response.success) {
        var value: boolean = response.value; // Works!
      } else {
        var error: string = response.error; // Works!
      }
    }

Clearly, this union is disjoint because the types `Success` and `Failed` were a priori known to be disjoint.

[dbaupp → catnaroek]

It doesn't require that. Flow seems to accept all sorts of variations on the following (including X | X):

   type X = { foo: string }
   type Y = { foo: string, bar: string }

   type Foo = X | Y

(Y is a subset of X in that case.)

[catnaroek → dbaupp]

But then it isn't disjoint.