Yes, final/terminal/coinitial. I'm sorry if this caused some confusion.
Yes, it's very coimportant to coput "co-" in cofront of coeverything, as if one were cospeaking kiSwahili or isiZulu.
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.
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).
Any computation that does not lead to bottom does not take infinitely
long in Haskell. Or what do you mean?
Lazy lists are infinite in the sense that you don't know until you force strictness whether the next component of the list is forthcoming or not: potentially rather than actually infinite.
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.
> 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.
Indeed, it is the lazy version of a deque.