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.I have re-subscribed xxxxxx@srfi.schemers.org and xxxxxx@srfi.schemers.org instead.

So this mail may not be merged into the reply-tree.

Best regards,

Siyuan Chen

Re: The mathematical name behind "unfold-right" in srfi-1Marc Nieper-Wißkirchen04 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