(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 20:17 UTC
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.