Dear Marc,

I'm sorry, there is some typo in my last message.

> Given a functor F(S)=1+N×S, the carry object of the final coalgebra for F is List(T)∪Stream(T), where T is the type of the elements. The set List(T)∪Stream(T) can not be expressed by lists in Scheme, because lists in Scheme are finite and Scheme is a strict language.

I mean "Given a functor F(S)=1+T×S,", not "F(S)=1+N×S".

PS: I first wrote down F(S)=1+N×S, then saw you used symbol "T". To be consistent,  I changed the symbol "N" to "T" but forgot to replace all the "N" to "T".

Thanks.

Best regards,
Siyuan Chen


On Fri, Jun 5, 2020 at 10:56 PM Siyuan Chen <xxxxxx@gmail.com> wrote:
Dear Marc,

Thanks for your explanation.
I re-explain below to ensure my understanding is correct.

> (The type of finite lists does not form an initial coalgebra so the
> notion of anamorphism does not really apply.)

You mean "final coalgebra" rather than "initial coalgebra", right?
Given a functor F(S)=1+N×S, the carry object of the final coalgebra for F is List(T)∪Stream(T), where T is the type of the elements. The set List(T)∪Stream(T) can not be expressed by lists in Scheme, because lists in Scheme are finite and Scheme is a strict language.
So the notion of anamorphism does not really apply. (But it is OK in Haskell)

> If we could define a `reverse` for infinite lists, we could explain `unfold-right`.

So this is why Scheme has `unfold-right` and Haskell has not `unfold-right`, is that right?
Because lists in Haskell are potentially infinite, we can not define a `reverse` for these infinite lists. (But it is OK in Scheme)

> But why can't we define a `reverse' for infinite lists? This is basically because the cartesian product has a right adjoint (the exponential) in our cases but not a left adjoint. (Do you see what I mean?)

I have a little background in category theory.
I know - × a ⊣ (-)ᵃ. This formula sometimes expresses currying, but what does it mean here?
Could you give me some hints?

> We could only circumvent this restriction by changing our underlying model and allowing computations that take infinitely long ...

This exactly Haskell do.

> In order to make sense of the right version in the context of coinitial coalgebras, a naive way to incorporate them is through double-ended streams.

So the rest of your mail is to explain how to implement `unfold-right` in Haskell, right?
We will use two left/right symmetry lists to express a reversible list.

> The endofunctor G underlying a double-ended stream whose elements are of type T would be X |-> 1 + (T * X * T * X)

So the mathematical name behind "unfold-right" is G-coalgebra, is that right?

> We could then unfold any G-coalgebra into a double-ended stream (the coinitial coalgebra of G);

That means `unfold-right` can be generalized to other data types by G-coalgebra and thisis the answer to my second question, right?

Could you recommend some references about this `unfold-right` stuff or G-coalgebra?
For example, is there any Haskell library implement `unfold-right` or G-coalgebra?
Or any papers explain this stuff in more detail?

Thanks again.

PS:
Sorry for the late reply.
It seems that the xxxxxx@srfi.schemers.org doesn't send any mail except daily digest.
I did not receive any mails until daily digest. I even I can't see your email address.
So this mail may not be merged into the reply-tree.
I have re-subscribed xxxxxx@srfi.schemers.org and xxxxxx@srfi.schemers.org instead.

Best regards,
Siyuan Chen


Re: The mathematical name behind "unfold-right" in srfi-1 Marc Nieper-Wißkirchen 04 Jun 2020 12:47 UTC

    Hi Siyuan,

    first of all, note that `unfold' in SRFI 1 is not a complete
    anamorphism because the anamorphism would produce potentially infinite
    lists (in case the stop? predicate never returns #t). A more
    satisfying version from a theoretical point of view is `stream-unfold'
    of SRFI 41.

    (The type of finite lists does not form an initial coalgebra so the
    notion of anamorphism does not really apply.)

    Now to `unfold-right': Its net effect is the same as `unfold' followed
    by a `reverse'. This already shows that it is a bit more complicated
    because `reverse' can only be applied to a finite list but not to the
    more general infinite lists.

    If we could define a `reverse' for infinite lists, we could explain
    `unfold-right'. But why can't we define a `reverse' for infinite
    lists? This is basically because the cartesian product has a right
    adjoint (the exponential) in our cases but not a left adjoint. (Do you
    see what I mean?) We could only circumvent this restriction by
    changing our underlying model and allowing computations that take
    infinitely long (thus computation would become coinductive instead of
    inductive, which would be the right notion for a truly lazy language;
    note that while most programming languages are strict, Haskell (even
    without strictness annotations) is neither strict nor lazy).

    In order to make sense of the right version in the context of
    coinitial coalgebras, a naive way to incorporate them is through
    double-ended streams. The endofunctor G underlying a double-ended
    stream whose elements are of type T would be X |-> 1 + (T * X * T * X)
    and the type of streams would be the coinitial coalgebra to this
    endofunctor. The terminal object 1 is for the indication of the empty
    stream that neither has head nor tail. The four factors in T * X * T *
    X correspond to the left car and cdr and to the right car and cdr,
    respectively. Compare with the endofunctor F: X |-> 1 + T * X
    modelling usual streams (infinite lists). Projecting to the first two
    or the last two factors yield two canonical natural transformations l,
    r: G => F, corresponding to view a double-ended stream as an ordinary
    stream (view it from the left or view it from the right). Switching
    the first two with the last two factors yields the obvious left/right
    symmetry (and corresponds to the reverse operation from above).

    We could then unfold any G-coalgebra into a double-ended stream (the
    coinitial coalgebra of G); unfold-right would be the same but with the
    symmetry applied afterward.

    Marc


    Am Do., 4. Juni 2020 um 12:46 Uhr schrieb Siyuan Chen :
    >
    > Hi,
    >
    > I'm reading srfi-1 document from https://srfi.schemers.org/srfi-1/srfi-1.html#FoldUnfoldMap.
    >
    > In "Fold, unfold & map" section, it says that
    >
    > > This combinator presumably has some pretentious mathematical name; interested readers are invited to communicate it to the author.
    >
    > I am very curious about the mathematical name of this function because, before that, I've never heard of it.
    >
    > For example,
    >
    > Haskell provides `unfoldr` in its`Data.List` library. This `unfoldr` corresponds `unfold` in srfi-1, but Haskell does not provide a function, something called `unfoldl`, which corresponds to `unfold-right` in srfi-1.
    >
    > My question is:
    >
    > 1. Is there any mathematical name behind `unfold-right` in srfi-1?
    > 2. Can `unfold-right` be generalized to other data types, e.g. Tree? We know that `unfold` can be generalized to any recursive types (i.e. anamorphism).
    >
    > Thanks.
    >
    > Best regards,
    > Siyuan Chen