Hacker News Reader

Comment by Twisol | Hacker News Reader

> Obviously, not. Not even apples versus oranges.

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

View on HN

What is the point of doing forall T but not forall A and 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.

If it helps, the equivalent Java signature is:

    interface Sum<A, B> {
      <T> T visit(Function<A, T> onA, Function<B, T> onB);
    }

Hopefully this makes it more clear that A and B are fixed when you receive a value of type Sum A B, but you get to pick a T when consuming that value.

Thanks

I really don't know how to respond to this sectarian bullshit.

Three is literally nothing in the ability to create another abstraction by finding an isomorphism, which is just a pair of functions.

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.

Let's say it is Hegel all over again.

Reply on news.ycombinator.com