Am Sa., 6. Juni 2020 um 21:23 Uhr schrieb Marc Nieper-Wißkirchen
<xxxxxx@nieper-wisskirchen.de>:

> > 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.

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.

There is, however, one claim in the paper that doesn't make too much
sense to me: 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. It isn't much better for a
total language, though. In section 3.1, the rule "0 / 0 = 0" is added
to make the division function total. As we all know from school, there
are no such rules that allow us to extend all the arithmetic laws to
all integers. So, to apply algebraic reasoning we would again have to
consider different cases, leading to the same complexity as in the
non-total case.

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.

If Z are the integers, what would be the correct "subtype" on which
the inverse can be defined? The naive answer, namely Z \ {0},
considered as a subset defined by an inequality is wrong. The correct
answer is the equation-defined subset of those pairs (x, y) in Z x Z
such that xy = 1. Projecting onto the first coordinate defines an
injection into Z. The inverse is just the flip that maps (x, y) to (y,
x). The reason for this comes from topology. If Z is not the integers
but some topological ring, the inverse won't be necessarily continuous
on the topological subspace of the units of the ring. It is, however,
continuous when the units of the ring are topologized as an
equation-defined subspace of the product as above.