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 <xxxxxx@gmail.com>:
>
> 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