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 <[email protected]
<mailto:[email protected]>> 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 [email protected]
<mailto:[email protected]> 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 [email protected]
<mailto:[email protected]> and [email protected]
<mailto:[email protected]> 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
