[bPspGiJT8Y]

> Because your code might not need to care about the position you insert your A or B

This is understandable. But what does it have to do with "collapsing" `a | a` into `a`? Throughout your post I think you're talking about plain untagged union types but that's something the guy I've been replying to already ruled out. Position problem can be handled beautifully by variants based on row polymorphism, such as in OCaml or PureScript. There you can access the fields not by their position but by a key, like keys in objects in JS, meaning that they don't have to be ordered at all. It's like an inverse of a struct: in a struct all fields/keys are guaranteed to exist, but in a variant only one of them exists. Due to row polymorphism they can also be extensible. You can even "handle" a particular field/key and remove it from the type but keep all the other ones and delay handling them.

> you also might not care whether it's an (encoding as) Either<A,B> or SomeoneElsesEither<A,B>

This is a theoretical issue but in practice I don't think I've ever seen anyone using some non-standard Either-like datatype in languages I've dealt with. Where Either needs to be used people just use Either.

> and you also don't want to have to deal with flattening nested Either's as in the example

What would "flattening" mean here? Fundamentally there are only 2 operations you can do on a generic sum type like this: either inject a value (construct the type) or try to get the value at a certain position. You might also think pattern matching will get tedious, but that's not the case either, you can just have a function `actOnAorBorC` and call it with `actOnA`, `actOnB` and `actOnC` and do the pattern matching inside these functions.

[k_g_b_]

> Position problem can be handled beautifully by variants based on row polymorphism, such as in OCaml or PureScript. There you can access the fields not by their position but by a key, like keys in objects in JS, meaning that they don't have to be ordered at all. It's like an inverse of a struct: in a struct all fields/keys are guaranteed to exist, but in a variant only one of them exists. Due to row polymorphism they can also be extensible. You can even "handle" a particular field/key and remove it from the type but keep all the other ones and delay handling them.

Exactly. OCaml's polymorpic variants implement a subset of set theoretic types for specifically defined types - see also this ICFP'16 paper https://dl.acm.org/doi/abs/10.1145/2951913.2951928

For languages with more first-class/principles set-theoretic types see the Ceylon type system (sadly dead and archived at Eclipse ceylon-lang.org) or TypeScript (though they obviously also have to deal with JS which makes everything more messy than necessary).

With "Flattening" I mean applying the usual laws of set theory for simplified types: Either<Either<A,B>,A>> is doesn't express our intent for a function return or parameter type if we don't care about the position of A, just whether it is an A, the same with Either<A, Either<A,B>>>/etc, so we'd want all nested variations normalized to Either<A,B>. But we also don't care about the difference between Either<A,B> and Either<B,A> - normalizing this is already not easy without metaprogramming/type reflection. At this point it ceases to have any significant relationship to the original Either type. If we'd use it still to signify A|B and would actively need to call normalizing functions to keep our types clean and simple in this way, that adds non-semantic (regarding the intent of our code) noise to our code or we need to hide the complexity by using more abstract tools like e.g. monad transformers. If instead the language already provided these types, this complexity caused by embedding set theory inside the language doesn't leak into our code and our intent can be expressed more clearly in types without "bookkeeping" artifacts. This is only exacerbated when going to higher arities of sets/Either.

[bPspGiJT8Y]

> Either<Either<A,B>,A>> doesn't express our intent for a function return or parameter type if we don't care about the position of A, just whether it is an A

> so we'd want all nested variations normalized to Either<A,B>.

Sorry, perhaps my thinking is shaped by nominal type systems rather than structural, but if the only thing we care about is whether the type is A, then how do we end up having Either<Either<A, B>, A>> in the first place? Thinking about this in terms of a nominal type system, the specific type you present here has to have some specific meaning associated with, specifically, this type, otherwise we would have chosen some other type. So the key thing here is that if we have Either<A, A> then it HAS to be distinct from simply A, otherwise we wouldn't have this type in the first place. Us constructing it means we associate it with a specific meaning so it has to be distinct from A. But if we DON'T care, then, I guess, we shouldn't use this type? Use the type we do care about? The same goes for Either<A, B> and Either<B, A>.

> or we need to hide the complexity by using more abstract tools like e.g. monad transformers

This is interesting, how do monad transformers relate to this problem?