(Previous discussion continued) | ||
Re: The mathematical name behind "unfold-right" in srfi-1 | John Cowan | 06 Jun 2020 19:07 UTC |
Re: The mathematical name behind "unfold-right" in srfi-1 | Marc Nieper-Wißkirchen | 06 Jun 2020 19:23 UTC |
Total functional programming | Lassi Kortela | 06 Jun 2020 19:37 UTC |
Re: The mathematical name behind "unfold-right" in srfi-1 | Marc Nieper-Wißkirchen | 06 Jun 2020 19:37 UTC |
Re: The mathematical name behind "unfold-right" in srfi-1 | Marc Nieper-Wißkirchen | 06 Jun 2020 19:52 UTC |
Re: The mathematical name behind "unfold-right" in srfi-1 | Marc Nieper-Wißkirchen | 06 Jun 2020 20:17 UTC |
Re: The mathematical name behind "unfold-right" in srfi-1 Marc Nieper-WiÃkirchen 06 Jun 2020 19:23 UTC
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