Comment by pron | Hacker News Reader

Comment by pron | Hacker News Reader

> functional programming ... is based on mathematics

Can we stop with this nonsense? I don't even know what "based on mathematics" means. All programming languages are formal languages, and all formal languages are inspired by mathematics in their design, and we can use mathematical reasoning to reason about them (although the form of mathematical reasoning can differ; pure FP strives to use equational reasoning, while imperative code uses assertional reasoning). While it is true that functional programs bear more resemblance to mathematical notation than imperative programs, but the majority of elementary mathematics cannot be directly expressed in FP in a similar notation -- or in any programming language with some computational complexity features (in the computational, "executable" part of the language; it can be expressed in the specification part, like a type system or a contract system).

E.g. x + 4 = 5 cannot be directly expressed in the computational part of the language, let alone f(x) = 5. Nothing that's nondeterministic can be expressed, either, such as x < 10, or x > y. Some of those can be expressed in logic programming (so it's even more "based on mathematics" than FP!), but at a cost in computational complexity.

But while glibly dismissing silly strawman arguments (which, I assume, some do make), the author contributes some silly claims of his own. For example:

> This has [the] consequence of reducing complexity, and thus reducing the number of bugs.

So, seeing as the author is so interested in precision and mathematics, I'd like to enquire where he pulled this fact from. But let me put this more generally: if pure functional programming has such obvious huge advantages over OOP with a big, real, impact and all, then a curious person with a scientific mind would ask what is the average difference in cost/quality that a company should expect when switching to pure FP? This should be a very easy question, because clear, obvious, large effects are easy to find (in fact, they're hard to hide) even over small samples. If a prediction of an easily observable effect does not turn out an easily observable effect, could there be something wrong with the hypothesis? And if the hypothesis makes a prediction of an effect that is hard to observe in practice, is it really so clear and obvious?

But that's precisely the point of functions (not methods, not procedures).

Could you be a bit more specific here? So far, your statement seems like a complete non sequitur.

absolutely!

> I don't even know what "based on mathematics" means.

Sure - it's too broad to be a useful definition. Perhaps it would be better to say "based on mathematical functions". Function outputs depend only on their inputs. So you can take f(x) == f(x) as true.

> Nothing that's nondeterministic can be expressed

Sweet! This way my production code can do the same thing as my test code. My job is to know what my code will do. I'll take all the determinism I can get.

> Perhaps it would be better to say "based on mathematical functions"

OK, and imperative code is "based on mathematical predicate transformers." My point is that some FP advocates use the "based on mathematics" as some marketing tagline that mostly shows they understand neither mathematics nor FP.

> Sweet! This way my production code can do the same thing as my test code. My job is to know what my code will do. I'll take all the determinism I can get.

That wasn't my point. The expression x ∈ ℕ ∧ x > 10 ∧ x < 12 is perfectly deterministic, but because its components are nondeterministic it cannot be expressed in FP, even though it is very convenient to do so (and commonly done in mathematics).

You are correct that the semantics (meaning) of subroutines in pure functional languages resembles mathematical functions more than their semantics in imperative languages (which is a different mathematical object [1]). But so what?

[1]: https://en.wikipedia.org/wiki/Predicate_transformer_semantic...

"Philip Wadler believes that typed lambda calculus was discovered not invented"

https://corecursive.com/021-gods-programming-language-with-p...

Well, he's wrong:

> We do not attach any character of uniqueness or absolute truth to any particular system of logic. The entities of formal logic are abstractions, invented because of their use in describing and systematizing facts of experience or observation, and their properties, determined in rough outline by this intended use, depend for their exact character on the arbitrary choice of the inventor.

That's the American logician Alonzo Church (1903-1995) in his 1932 paper, A Set of Postulates for the Foundation of Logic, in which he expresses his disagreement with Wadler and also invents the (untyped) lambda calculus [1]. You can find this passage and many more in a 300-page anthology of (mostly) primary sources that I composed over a year ago [2], many of them describing the meticulous, intentional invention of various formalisms over the centuries, as well as aesthetic concerns which have led some to prefer one formalism over another (e.g. the invention of a logical algebra by Boole, and its later amendment into what we know as the Boolean algebra, by Jevons, Peirce and Schröder to make it more pleasing). In fact, Alan Turing's 1937 paper directly demonstrates the essence of computation and the "accident" of formalisms, which are linguistic, aesthetic, subjective formulations of a fundamental, non-linguistic idea (as Gödel said, when he called Turing's discovery a miracle, it does not just show that one formalism is equivalent to another, but uncovering the essence of all formalisms at once).

Wadler is not an authority on the history of logic, and his perspective (which, unlike his actual academic work, is not based on serious scholarship), combined with his guru stance, is one of the causes for the deep confusion among functional programmers about FP and mathematics, and fosters a mystical adoration of mathematics, one of whose symptoms are nonsensical statements like "based on mathematics," rather than understanding. I wish he'd stop doing that, as I don't think it's helpful.

[1]: In that paper the lambda calculus appears as a proof calculus for a logic that was later proven unsound. The calculus itself was then extracted and used in Church's more famous 1936 paper, An Unsolvable Problem of Elementary Number Theory in an almost-successful attempt to describe the essence of computation. That feat was finally achieved by Turing a few months later.

[2]: https://pron.github.io/computation-logic-algebra

Reply on news.ycombinator.com