Repost on the list in case anyone is interested.

---------- Forwarded message ---------
Von: John Cowan <xxxxxx@ccil.org>
Date: So., 7. Juni 2020 um 00:30 Uhr
Subject: Re: The mathematical name behind "unfold-right" in srfi-1
To: Marc Nieper-Wißkirchen <xxxxxx@nieper-wisskirchen.de>

No, not intentionally. Use your own judgement about reposting to the list.

On Sat, Jun 6, 2020 at 5:16 PM Marc Nieper-Wißkirchen
<xxxxxx@nieper-wisskirchen.de> wrote:
>
> Hi John,
>
> did you reply intentionally only to me?
>
> Am Sa., 6. Juni 2020 um 22:51 Uhr schrieb John Cowan <xxxxxx@ccil.org>:
>
> >> I agree with the main point of the paper, namely that totality for a
> >> functional programming language would be a boon. All this categorical
> >> abstract nonsense does not really apply to the existing functional
> >> languages because the falsum (bottom) is usually not taken into account.
>
> I meant that bottom is not taken into account when using categorical
> reasoning. (See also:
> http://math.andrej.com/2016/08/06/hask-is-not-a-category/)
>
> > The difference between languages in which  (cons ⊥ ⊥) => (⊥ . ⊥) and those for which it is simply ⊥ is not the same as the lazy/strict division.  As the paper notes, Miranda is lazy but takes the second view nonetheless.  A similar issue arose in WG1; a faction argued that (make-rectangular +nan.0 15.0) should => +nan.0 rather than +nan.0+15.0i, but all the numerical programmers rebelled at that idea.
>
> Isn't the first view the more lazy one? Nevertheless, Haskell's view
> (the first one) has the consequence that there are no product types.
> And we are back to my claim from above that one has to be careful to
> apply the categorical reasoning.
>
> Thanks for mentioning the WG1 issue; this is a nice concrete example.
>
> >> In section 2.1, the author says that the non-totality
> >> makes algebraic reasoning about programs harder and gives the example
> >> of the algebraic rule "e - e = 0". Indeed, this is not always
> >> fulfilled when bottom values are present.
> >
> >
> > See <https://srfi.schemers.org/srfi-73/srfi-73.html>, which adds the exact infinities 1/0 and -1/0 to Scheme; it would be straightforward to add 0/0 as well.
>
> It may make sense to add 1/0 and -1/0. It may even make sense to add
> 0/0 to get total functions. But these new values still won't
> participate in the usual arithmetic rules and won't simplify the
> reasoning.
>
> >> I think the only sensible things instead of adding questionable rules
> >> like "0 / 0 = 0" are either a judicious use of Maybe types or, much
> >> better, the definition of subtypes on which a previously partial
> >> function becomes total.
> >
> >
> > Or supertypes, as above.  (After all, the natural numbers were extended to be total over - by inventing the negative integers.)  Users of inexact arithmetic have learned to use, if not to love, +inf.0 and -inf.0 and +nan.0, which are somewhat arbitrarily treated by Scheme as real but not rational.
>
> +inf.0 and -inf.0 have a nice interpretation as the boundary points of
> the compactification of the real line with respect to its natural
> order. Although arithmetic reasoning has its limits as soon as
> infinities are added, they can be explained topologically. On the
> other hand, +nan.0 is really not a number and cannot be localized
> anywhere. So it is certainly a useful element to make the real type
> automatically a Maybe type, but is it really different from Haskell's
> bottom?
>
> > "Die Consen und die Fixnumen hat der liebe McCARTHY gemacht, alles andere ist Hackerwerk."
>
> :)
>
> You can even drop the fixnums as they can be encoded with pairs so
> that God can stand on the shoulders of McCarthy. And McCarthy can
> stand on the shoulders of Church who knows how to model pairs with
> lambdas. :)