Am Sa., 6. Juni 2020 um 21:07 Uhr schrieb John Cowan <xxxxxx@ccil.org>:

> Yes, it's very coimportant to coput "co-" in cofront of coeverything, as if one were cospeaking kiSwahili or isiZulu.

Joke by Ravi Vakil: "A comathematician is a device for turning
cotheorems into ffee."

> I think this is easier to see with folds than with unfolds.  Left folds require finite lists under both lazy and strict evaluation (for backward compatibility, the properly tail recursive Haskell left fold is called foldl' rather than foldl).  Right folds, on the other hand, can handle infinite lists under lazy evaluation but not under strict evaluation (where they cannot even be constructed).

Note that foldr/fold-right, when applied to streams instead of finite
lists, is no catamorphism anymore (so won't be the categorical
opposite of `unfold' anymore), because catamorphisms have initial
algebras as their domain. (Related to this is that Haskell cannot even
model such inductive types without strictness annotations).

When you apply `fold-right' to an infinite list, using lazy semantics,
the result will again be an object of a coinductive type. And this
version of `fold-right' will be defined through corecursion (over the
result) instead of recursion over the input.

> If I had the time, I'd love to put together a Lisp that uses the principles of Turner's elementary total functional programming <https://homepages.dcc.ufmg.br/~mariza/CELP/sblp2004/papers/turner.pdf>, which obliterates the difference between lazy and strict by allowing codata to be constructed but not accessed, thus making it truly the dual of data.  The language is not Turing-complete, but an amazing number of algorithms are available nonetheless.  The paper is very accessible (as proved by the fact that I understand it) and well worth reading.

Thanks for the reference. I will take a look at it.

Andrzej Filinski's master's thesis seems to be a canonical read when
it comes to this kind of duality:
http://hjemmesider.diku.dk/~andrzej/papers/.

Marc