Am Sa., 6. Juni 2020 um 21:07 Uhr schrieb John Cowan <co...@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
