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.
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.
That's just a union. The 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) 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.
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.
As if that weren't enough, any talk about universal properties is utterly pointless as soon as object identities matter everywhere.
> A ⊕ B = (A × {0}) ∪ (B × {1})
Hardly nonsense! This makes clear the connection to sets in a way that words weren't doing for me.
(The Flow use of the name doesn't seem to quite match the mathematical definition.)
In any case, Flow doesn't require that the sides of the | are different.
> 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!
}
}
type X = { foo: string }
type Y = { foo: string, bar: string }
type Foo = X | Y
The way you sum a type with itself in Haskell would be something like
data Response = Success { result :: String }
| Failure { reason :: String }
From my understanding of the Flow documentation, the equivalent would be
type Response = {| success: true, result: string |}
| {| failure: true, reason: string |};
So although sum types and disjoint unions are different concepts, they can easily be used to simulate each other.
(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
ERR_DOUGLAS_ADAMS : The answer to the Ultimate Question of Life,
the Universe and Everything is the number forty-two.
I agree that being able to change the internals of a module without breaking external code is a good thing, but unlike other security guarantees, abstract types can break merely by having a stronger type system which is able to prove strictly more things (such as whether two types are equal). That makes implementing completely leak-free abstractions quite difficult.
It can even be hard to tell which language feature exactly causes the leak. In your example, it is not just the existence of the union type that causes the problem, but the operation "is T", which you probably assume to be of type "forall a. (a | T) -> Bool" or something. Obviously, that operation is doing all the work of looking at the underlying implementation and leaking it.
While you couldn't meaningfully type such an operation without union types, having unions in your type system does not mean that such a function will be available. Although working with unions without being able to tell the types apart would be quite inconvenient, you could nonetheless remove that ability from the language, either completely (effectively requiring all unions to be disjoint) or by having special markers to enable or disable it (similar to Haskell's type class constraints).
Flow doesn't go to such great lengths because it is still built on JavaScript objects, which don't really have a concept of privacy. If there were private symbols (i.e. unique properties which can only be accessed by the module which defines them), you could trivially implement abstract types similar to Haskell's newtype wrapper as { [some private symbol]: implementation-type }. Until such a thing is added, you'll have to limit yourself to disjoint unions to avoid abstraction leaks.
Indeed, which is why I'm not such a huge fan of overly powerful type systems.
> That makes implementing completely leak-free abstractions quite difficult.
It means the type system has to have the right amount of expressive power. Too little, and separation of concerns becomes difficult. Too much, and separation of concerns becomes difficult too!
It also means that we can't rely on types to prove everything we would like to prove about programs. This seems intuitively right, because type systems are first and foremost meant to be mechanically checkable, not to be flexible enough to express every possible software requirement.
> In your example, it is not just the existence of the union type that causes the problem, but the operation "is T", which you probably assume to be of type "forall a. (a | T) -> Bool" or something.
This is correct. But removing this `is T` operation would greatly reduce the appeal of union types in practice.
> you could trivially implement abstract types similar to Haskell's newtype wrapper as { [some private symbol]: implementation-type }.
Both Haskell's `newtype` and your proposal are poor replacements for actual abstract types.