Am Sa., 6. Juni 2020 um 11:12 Uhr schrieb chansey97 <xxxxxx@gmail.com>:
>
>
> 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".

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

> > (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?

Yes, final/terminal/coinitial. I'm sorry if this caused some confusion.

> 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)

Scheme's evaluation model uses strict semantics by default but you
have promises in Scheme, When you use them systematically (see SRFI
41, for example), Scheme gains lazy semantics. So the notion of
anamorphism applies to Scheme as well. It doesn't really apply to
Scheme's list type, though, because the list type is inductive and not
coinductive. Likewise, one can build the type of finite lists with
Haskell by using the strictness modifier.

> > 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?

We could add it to Haskell as well, but it would fail as soon as
`unfold' produces an infinite list. (This is exactly what happens with
Haskell's `foldl'.) The same problem would occur if we tried to add
`stream-unfold-right' to SRFI 41. So, it doesn't really have anything
to do with Haskell or with Scheme, but more about the underlying data
type.

> > 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?

Let X be the type of streams (potentially infinite lists). It is the
coinitial coalgebra for the functor F(A) = 1 + T * A. A reverse
operation would be a morphism X -> X. As X is the coinitial
F-coalgebra, we know what morphisms into X are, namely F-coalgebra
structures on the domain of the morphism. So to get an arrow X -> X
that corresponds to reversal, we have to choose a suitable F-coalgebra
structure on the domain X, which is a morphism X -> FX, which is a
morphism X -> 1 + T * X.

In order to define such a morphism, we want to use again that we know
what morphisms into the X on the right-hand side are. If F had a left
adjoint, a map X -> 1 + T * X would be just a map GX -> X.

To understand this idea, let us drop the "co" everywhere. So X becomes
the type of finite lists and is the initial F-algebra. We want to
define a reverse morphisms X -> X. This is equivalent to choosing an
F-algebra structure on the codomain X, which is a morphism FX -> X.
Now, according to your adjunction from above, such a morphism if given
by a morphism 1 -> X (what is the reversal of the empty list) and a
morphism X -> X^T. The latter is the curried version of the append to
the right operation. This can be defined through a `fold-right' (i.e.
by using the initiality of the X on the left hand side).

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

Any computation that does not lead to bottom does not take infinitely
long in Haskell. Or what do you mean?

> > 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?

I doubt that there is a mathematical name. A G-coalgebra would have
`unfold' and `unfold-right', but it is really a different type.

> 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?

I don't know; I just thought of this when I wrote the email.

Actually, I am not sure whether it makes a lot of sense to talk about
`fold' (Haskell's `foldl') and `unfold-right' on the level of
catamorphisms and anamorphisms. From the point of the concrete
evaluator, the main difference between the left and the right versions
is that one is iterative while the other one is recursive. One should
first describe a mathematical framework that allows one to talk about
the difference between iteration and recursion. (See SRFI 157 for a
Scheme-way to make this difference observable.)

Marc