7 ms·

Yes, Flow has. https://flow.org/en/docs/types/unions/#toc-disjoint-unions https://flow.org/en/docs/types/unions/#toc-disjoint-unions

catnaroek 9y ago
Sum types are a universal construction: you take any two types, and produce yet another type. In particular, you can sum a type with itself. Disjoint unions give you nothing of the sort. In other words: learn to mathematics.
- dang 9y ago
  > In other words: learn to mathematics That breaks the HN guidelines by crossing into incivility. You'd stopped doing that on HN, which is great, so please don't resume. This comment would be better if it (a) dropped the rude bit and (b) made the distinction from disjoint unions more clearly. https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
- xelxebar 9y ago
  The tone of the parent comment is a bit aggressive, but the content is relevant. Just in case it's not clear, the union of sets "merges" elements that are identical whereas in the (direct) sum each element gets tagged with where it comes from. Formally, we have a set that indexes over the sets we want to sum and then we just Cartesian product each set with it's index before unioning. In abstract nonsense we usually write A ⊕ B = (A × {0}) ∪ (B × {1}) where ⊕ is the direct sum operator. So there direct sum of a set with itself is quite different from a plain union. For more than two sets we just index over things in the obvious way and write ⨁ᵢ Aᵢ = ∪ᵢ (Aᵢ × {i}) What parent means by universal property is that any that collection of functions {fᵢ : Aᵢ → C} can be decomposed into functions {gᵢ : Aᵢ → ⨁ᵢ Aᵢ} and a single, uniquie g: ⨁ᵢ Aᵢ → C where fᵢ = g ∘ gᵢ. With a little thought, the universal property above seems obvious, and with a little more work, you can see that it is actually equivalent to the definition of direct sum above. Thus we can actually take this universal property as the definition of direct sum and derive the original. The cool thing is that the universal property doesn't refer to set-specific operations---just functions/maps---so we actually have a definition for the direct sum of things more general than sets. That is, we can form the direct sum of things like monoids, groups, certain classes of differential functions, etc. I could go on, but this road leads to madness^W category theory.
  - deleted 9y ago
    [deleted]
  - dbaupp 9y ago
    > Just in case it's not clear, the disjoint union of sets "merges" elements that are identical whereas in the (direct) sum each element gets tagged with where it comes from. That's just a union. The disjoint union (https://en.wikipedia.org/wiki/Disjoint_union https://en.wikipedia.org/wiki/Disjoint_union) is what you're calling the direct sum. The direct sum (https://en.wikipedia.org/wiki/Direct_sum https://en.wikipedia.org/wiki/Direct_sum) is an operation on algebraic structures to create new algebraic structures (e.g., one can direct-sum two groups to get a new group, and similarly rings, vector spaces, etc.), not just sets.
    - xelxebar 9y ago
      Whoops. That one slipped past. Thanks. In case it's not clear, I just specialize tensor sum to the category Set; that's all. At the end I do mention how the tensor sum applies on a wider class of objects. In fact, any Cartesian category has (finite) tensor products, even if the objects aren't traditionally thought of as "algebraic structures", e.g. certain classes of topological spaces, Frolicher manifolds, etc.
    - catnaroek 9y ago
      A union type `A | B` in Flow is disjoint if and only if the types `A` and `B` are a prior known to be disjoint. There is no equipping `A` and `B` with fresh new tags to force them to be disjoint.
      - dbaupp 9y ago
        ... Which isn't relevant to the clarification of mathematical terms in my comment.
        catnaroek 9y ago
        It is relevant, because it means that while `|` may produce a disjoint union if its arguments are already disjoint, it is not guaranteed to produce a disjoint union in the general case. Hence, my original comment had a point. As if that weren't enough, any talk about universal properties is utterly pointless as soon as object identities matter everywhere.
- dbaupp 9y ago
  Disjoint union in mathematics is exactly the universal construction you're calling sum types: https://en.wikipedia.org/wiki/Disjoint_union https://en.wikipedia.org/wiki/Disjoint_union (The Flow use of the name doesn't seem to quite match the mathematical definition.)
  - catnaroek 9y ago
    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 9y ago
      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 9y ago
        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 9y ago
- yorwba 9y ago
  > In particular, you can sum a type with itself. The way you sum a type with itself in Haskell would be something like data Response = Success { result :: String } | Failure { reason :: String } where each component of the sum is uniquely tagged. From my understanding of the Flow documentation, the equivalent would be type Response = {| success: true, result: string |} | {| failure: true, reason: string |}; where the only material difference is that Flow needs to work with JavaScript, which doesn't have a built-in tagging mechanism, unlike Haskell. So although sum types and disjoint unions are different concepts, they can easily be used to simulate each other.
  - catnaroek 9y ago
    What you propose breaks completely as soon as you want to define and use abstract types.
    - yorwba 9y ago
      I think it should be possible. Can you give an example that can't be translated?
      - deleted 9y ago
        [deleted]
      - catnaroek 9y ago
        Union and intersection types make the following assumptions: (0) There is a single physical universe that contains all values. (1) The role of types is to “carve out” fragments of this universe. (2) Say you have two values `x` and `y` of types `A` and `B`. Because it is possible to form the union type `A | B`, to which both `x` and `y` belong, the only way to make sure `x` and `y` cannot be conflated with each other is to make them physically distinct elements of the universe. On the other hand, abstract types make the following assumptions: (0) Each type is a “world” of its own, defined in terms of its logical structure. The values of a type are a mere consequence of this logical structure. Hence, it doesn't make sense to try to “split” or “merge” types. (1) It doesn't make sense to argue that an int is different from a string, because it's just as nonsensical as arguing that they are equal. What they are is incommensurable. (2) Say you have type two different abstract types `A` and `B`. Because they could share an underlying representation type `T`, you cannot rely on values of different types having physically distinct representations. --- Suppose we had a language with both union and abstract types. The contradictions between the assumptions behind union and abstract types would lead to hilarious consequences: signature ERROR_CODE = sig type error_code (* specification of operations on error codes *) end (* we use opaque ascription, so that the internal representation * of error codes becomes inaccessible to external parties *) structure ErrorCode :> ERROR_CODE = struct type error_code = int (* prosaic representation *) (* implementation of operations on error codes *) end type union = error_code | int (* union *) (* suppose we also have flow typing so that this example works *) fun test (u : union) = if u is error_code then ErrorCode.printErrMsg u else printInt u val _ = test 42 You'd expect this code to print the integer `42`, but it actually prints: ERR_DOUGLAS_ADAMS : The answer to the Ultimate Question of Life, the Universe and Everything is the number forty-two. Wasn't the fact error codes are internally represented as ints supposed to be unknowable to external parties?

catnaroek 9y ago

Sum types are a universal construction: you take any two types, and produce yet another type. In particular, you can sum a type with itself. Disjoint unions give you nothing of the sort. In other words: learn to mathematics.

dang 9y ago
> In other words: learn to mathematics That breaks the HN guidelines by crossing into incivility. You'd stopped doing that on HN, which is great, so please don't resume. This comment would be better if it (a) dropped the rude bit and (b) made the distinction from disjoint unions more clearly. https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
xelxebar 9y ago
The tone of the parent comment is a bit aggressive, but the content is relevant. Just in case it's not clear, the union of sets "merges" elements that are identical whereas in the (direct) sum each element gets tagged with where it comes from. Formally, we have a set that indexes over the sets we want to sum and then we just Cartesian product each set with it's index before unioning. In abstract nonsense we usually write A ⊕ B = (A × {0}) ∪ (B × {1}) where ⊕ is the direct sum operator. So there direct sum of a set with itself is quite different from a plain union. For more than two sets we just index over things in the obvious way and write ⨁ᵢ Aᵢ = ∪ᵢ (Aᵢ × {i}) What parent means by universal property is that any that collection of functions {fᵢ : Aᵢ → C} can be decomposed into functions {gᵢ : Aᵢ → ⨁ᵢ Aᵢ} and a single, uniquie g: ⨁ᵢ Aᵢ → C where fᵢ = g ∘ gᵢ. With a little thought, the universal property above seems obvious, and with a little more work, you can see that it is actually equivalent to the definition of direct sum above. Thus we can actually take this universal property as the definition of direct sum and derive the original. The cool thing is that the universal property doesn't refer to set-specific operations---just functions/maps---so we actually have a definition for the direct sum of things more general than sets. That is, we can form the direct sum of things like monoids, groups, certain classes of differential functions, etc. I could go on, but this road leads to madness^W category theory.
- deleted 9y ago
  [deleted]
- dbaupp 9y ago
  > Just in case it's not clear, the disjoint union of sets "merges" elements that are identical whereas in the (direct) sum each element gets tagged with where it comes from. That's just a union. The disjoint union (https://en.wikipedia.org/wiki/Disjoint_union https://en.wikipedia.org/wiki/Disjoint_union) is what you're calling the direct sum. The direct sum (https://en.wikipedia.org/wiki/Direct_sum https://en.wikipedia.org/wiki/Direct_sum) is an operation on algebraic structures to create new algebraic structures (e.g., one can direct-sum two groups to get a new group, and similarly rings, vector spaces, etc.), not just sets.
  - xelxebar 9y ago
    Whoops. That one slipped past. Thanks. In case it's not clear, I just specialize tensor sum to the category Set; that's all. At the end I do mention how the tensor sum applies on a wider class of objects. In fact, any Cartesian category has (finite) tensor products, even if the objects aren't traditionally thought of as "algebraic structures", e.g. certain classes of topological spaces, Frolicher manifolds, etc.
  - catnaroek 9y ago
    A union type `A | B` in Flow is disjoint if and only if the types `A` and `B` are a prior known to be disjoint. There is no equipping `A` and `B` with fresh new tags to force them to be disjoint.
    - dbaupp 9y ago
      ... Which isn't relevant to the clarification of mathematical terms in my comment.
      - catnaroek 9y ago
        It is relevant, because it means that while `|` may produce a disjoint union if its arguments are already disjoint, it is not guaranteed to produce a disjoint union in the general case. Hence, my original comment had a point. As if that weren't enough, any talk about universal properties is utterly pointless as soon as object identities matter everywhere.
dbaupp 9y ago
Disjoint union in mathematics is exactly the universal construction you're calling sum types: https://en.wikipedia.org/wiki/Disjoint_union https://en.wikipedia.org/wiki/Disjoint_union (The Flow use of the name doesn't seem to quite match the mathematical definition.)
- catnaroek 9y ago
  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 9y ago
    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 9y ago
      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 9y ago
yorwba 9y ago
> In particular, you can sum a type with itself. The way you sum a type with itself in Haskell would be something like data Response = Success { result :: String } | Failure { reason :: String } where each component of the sum is uniquely tagged. From my understanding of the Flow documentation, the equivalent would be type Response = {| success: true, result: string |} | {| failure: true, reason: string |}; where the only material difference is that Flow needs to work with JavaScript, which doesn't have a built-in tagging mechanism, unlike Haskell. So although sum types and disjoint unions are different concepts, they can easily be used to simulate each other.
- catnaroek 9y ago
  What you propose breaks completely as soon as you want to define and use abstract types.
  - yorwba 9y ago
    I think it should be possible. Can you give an example that can't be translated?
    - deleted 9y ago
      [deleted]
    - catnaroek 9y ago
      Union and intersection types make the following assumptions: (0) There is a single physical universe that contains all values. (1) The role of types is to “carve out” fragments of this universe. (2) Say you have two values `x` and `y` of types `A` and `B`. Because it is possible to form the union type `A | B`, to which both `x` and `y` belong, the only way to make sure `x` and `y` cannot be conflated with each other is to make them physically distinct elements of the universe. On the other hand, abstract types make the following assumptions: (0) Each type is a “world” of its own, defined in terms of its logical structure. The values of a type are a mere consequence of this logical structure. Hence, it doesn't make sense to try to “split” or “merge” types. (1) It doesn't make sense to argue that an int is different from a string, because it's just as nonsensical as arguing that they are equal. What they are is incommensurable. (2) Say you have type two different abstract types `A` and `B`. Because they could share an underlying representation type `T`, you cannot rely on values of different types having physically distinct representations. --- Suppose we had a language with both union and abstract types. The contradictions between the assumptions behind union and abstract types would lead to hilarious consequences: signature ERROR_CODE = sig type error_code (* specification of operations on error codes *) end (* we use opaque ascription, so that the internal representation * of error codes becomes inaccessible to external parties *) structure ErrorCode :> ERROR_CODE = struct type error_code = int (* prosaic representation *) (* implementation of operations on error codes *) end type union = error_code | int (* union *) (* suppose we also have flow typing so that this example works *) fun test (u : union) = if u is error_code then ErrorCode.printErrMsg u else printInt u val _ = test 42 You'd expect this code to print the integer `42`, but it actually prints: ERR_DOUGLAS_ADAMS : The answer to the Ultimate Question of Life, the Universe and Everything is the number forty-two. Wasn't the fact error codes are internally represented as ints supposed to be unknowable to external parties?