Formally, `A + B` is isomorphic to `forall T. (A -> T, B -> T) -> T`, where the inner `(A -> T, B -> T)` is the type of a visitor.
a + b
-- CPS transform
= forall t. ((a + b) -> t) -> t
-- distribute -> over +
= forall t. (a -> t, b -> t) -> t
-- if you want to drop even the product, distribute -> over *
-- but this loses you the ability to name a separable Visitor
= forall t. (a -> t) -> (b -> t) -> t
type Visitor a b t = (a -> t, b -> t)
type Sum a b = forall t. Visitor a b t -> t
iso :: Sum a b -> (a + b)
iso s = s (Left, Right)
osi :: (a + b) -> Sum a b
osi (Left a) = \(onA, onB) -> onA a
osi (Right b) = \(onA, onB) -> onB b
A and B are free to be chosen by a producer of the generic Sum type. However, T can be chosen "late", by a consumer of Sum; a value of type Sum A B must work for any T you decide to use down the line.
You're right that there is no benefit in creating another abstraction, but the point of the post is sometimes the language doesn't have support for the original abstraction (e.g. sum types), so in some cases the other abstraction (e.g. visitor pattern or Church encoding) is the only available abstraction.
Look, I never tried to be offensive or even bully. But I care about the principle of calling things by its proper names and precise language usage. I am describing things exactly how I see them.
And I have reasons to do so. Like so many others I have traveled that road, from Haskell basics up to the latest writings and courses of that self-propelled category theory expert - Bartosz, for whom I have great respect.
However, at the end of the journey I came to different conclusions, that the whole subfield is nothing but a sect (the definition is a consensus based group of eager supporters) and the whole set of nested abstractions is empty of meaning, except in producing deeper and deeper nested abstractions. I cold provide analogies with Eastern religious sects, which I have studied too, where abstract things are described in minute details, and the merit is in the knowledge of these minute details, but I won't. It will only complicate this discussion.
So I don't see any meaning, and I see socially constructed interested, identical to esoteric teachings, which is even better definition of what Bartosz and others are doing.
Formally, `A + B` is isomorphic to `forall T. (A -> T, B -> T) -> T`, where the inner `(A -> T, B -> T)` is the type of a visitor.