Why is this taken as a given to be a good thing? Our hardware has state. Any IO is a side effect, so what's the non trivial use case for "pure functions" all the way down?
I think FP paradigms can be useful in specific problem domains, I'm skeptical of the general utility (vs resource spend) of strong FP languages.
Pure functions are easier to reason about (there may be exceptions of course), that's why they're interesting.
This paper is not related to side-effects - it's related to "totality", meaning all programs terminate. This could also be interesting for side-effecting programs, but it's of course much harder to verify in this case.
Due to the halting problem's existance a total language can not be Turing complete, but many useful programs can be verified.
I didn't see anything in the paper that claims that pure functions should be "all the way down", and the paper is not about side effects anyway.
Basically it's about the loop making progress on every iteration, but we can have an infinite number of iterations.
I think the distinction is related to the one between data and co-data.
Because that’s the environment that programs are run on, doing anything else is fighting against the environment. I would argue that humans have done this to great effect in some areas, but not in programming.
>Pure functions are easier to reason about (there may be exceptions of course), that's why they're interesting.
Prove it.
Video game programming, where performance really matters, is a great way to see the cost of forcing the hardware to deal with human abstractions (mainly OOP). Rules like "never have a Boolean in a struct" or "an array with linear access can be faster than a tree with log access" wake you up to the reality of the hardware. :p
In academia, and the especially academic, utopian realm of functional programming, you're trained to live in dreamland.
If you can afford it, though, hey, it's a nice place to be.
In many cases performing math again is faster than memoization.
General gist is to try to cram as much in to the cache lines as possible, sometimes even at the “cost” of calculating values again.
OO outside of contexts where every little bit of performance matters suffers in exactly the exact same way.
> If you can afford it, though, hey, it's a nice place to be.
No arguments there! A huge majority of applications can afford to be written this way, even ones where performance is a concern (WhatApp, for example).
This is sometimes true for any one given app but it's not a good overall outcome.
It is why we have today multi-GHz CPUs with lots of cores and dozens of GB of RAM and yet... most actions feel less responsive today than in 1995 with a 120MHz CPU, 1 core and 1MB.
He was never a kind of "lets keep doing C in games" style of developer.
Thankfully, without the likes of Unreal, Unity and similar efforts, we would still be doing like it always was done here, kind of mentality.
And apparently Epic belives enough on this to create Verse, and to quote Tim Sweany point of view on "The Next Mainstream Programming Languages",
Proofs are good evidence that pure functions are easier to reason about. Many proof assistants (Coq, Lean, F*) use the Calculus of Inductive Constructions, a language that only has pure, total functions, as their theoretical foundation. The fact that state of the art tools to reason about programs use pure functions is a a pretty good hint that pure functions are a good tool to reason about behavior. At least, they're the best way we have so far.
This is because of referential transparency. If I see `f n` in a language with pure functions, I can simply lookup the definition of `f` and copy/paste it in the call site with all occurrences of `f`'s parameter replaced with `n`. I can simplify the function as far as possible. Not so in an imperative language. There could be global variables whose state matters. There could be aliasing that changes the behavior of `f`. To actually understand what the imperative version of `f` does, I have to trace the execution of `f`. In the worst case, __every time__ I use `f` I must repeat this work.
I don’t really accept “this group of people who’s heads are super far up the ‘pure functions’ ass choose purity for their solutions” as “evidence” that purity is better.
I’m not saying that purity is bad by any stretch. I just consider it a tool that is occasionally useful. For methods modifying internal state, I think you’ll have a hard time with the assertion that “purity is easier to reason about”.
Modeling the method that modifies internal state as a function from old state to new state is the simplest way to accomplish this goal. I.e., preconditions and postconditions.
What's the point of a callback that doesn't mutate state somewhere?
The framework or runtime calls your function, and the return value tells it what to do next.
Prominent examples include React and Excel.
I think James Mickens in The Night Watch[1] puts it best:
> Pointers are real. They’re what the hardware understands. Somebody has to deal with them. You can’t just place a LISP book on top of an x86 chip and hope that the hardware learns about lambda calculus by osmosis.
[1]: https://www.usenix.org/system/files/1311_05-08_mickens.pdf
What percent of your last program was written in register move commands?
> Registers, addresses, and machine instructions are real. They're what the hardware understands. You can't just place an ALGOL book on top of an IBM 709 and hope that the hardware learns about expressions, variables and records by osmosis.
As far as the IO thing is concerned, one could use pure functions to construct a model of an imperative program. Then you just need something to run it... There is a sense in which this is exactly what is done in practice.
Is it easier to reason about a 10,000-line-long math proof, or a 10,000-line-long program? I'm not sure that the math is actually easier.
Is it easier to write a fully-correct 10,000-line-long math proof, or a 10,000-line-long program? Again, I'm not sure that the math is actually easier.
Is it easier to write a formal prover for the math? Almost certainly. And maybe, with a formal prover, writing the correct math is easier...
Don't compare them on the basis of familiarity. Making your programming language look mathy is not the point.
I'd offer a different comparison:
Reason about a 10,000-line-long math proof, or a 10,000-line-long math proof in which there are instructions to jump back-and-forth with your pencil, crossing out and updating previously-calculated values in-place.
If this idea is new to you and you want to learn more, google "propositions as types" or "the curry howard correspondance".
It is not taken as a given at all. It is an acknowledgment that it makes perfect sense to build on top of centuries of work and theory on well-behaved tools, rather than reinventing the wheel with ill-behaved tools.
But I do think it's valuable to aim for as side-effect-free as possible, and concentrate the statefulness into certain part(s), rather than spread out all over the place, which is the typical way typical.
FP can be used to get you there, but it strongly optimizes for readability of experts in most cases which harms readability in general, as there are always fewer experts.
At least that's been my experience with FP languages in the professional space. People often underestimate the benefits of good tooling, a large community, and deep candidate pool.
Strongly disagree. In the way you speak of "readability", you're confusing simplicity and familiarity, which are really two different things.
If FP if not "familiar" to you, then it will require some effort on your part, sure. But you can teach FP to an absolute beginner, and they will likely find it just as simple, if not simpler, than an imperative mode of reasoning. It's basically just a social and cultural issue at this point.
All programming languages have side effects. The question is what logical constraints limit them.
It's often helpful to distinguish between effects and side-effects. The idea is that an effect is deliberate and explicit, such as, say, sending an email or moving a robot's arm. Whereas a side-effect is one that happens but wasn't your explicit objective - heating the CPU, say, or silently caching a value in thread-local storage. Haskell programs often use the type system to make these kinds of distinction.
Total programming is not useful for everything. Then again, neither is assembly language, or C++, or Rust, or Python. Each has a particular use case in which they are an appropriate tool, and many use cases in which they are not. The job of an engineer is to figure when each tool is appropriate.
Very good engineers keep tabs on lots of tools so that they can choose the best tool when the time calls.
> I think FP paradigms can be useful in specific problem domains, I'm skeptical of the general utility (vs resource spend) of strong FP languages.
The vast majority of FP languages offer no totality checking. Totality checking is mainly used in theorem provers, which are a small subset of FP. I'm not sure what you're going at here, but you're confusing two separate things.
Speaking for myself, when I’m mentally modeling how I logically work through a problem, which concepts I’ve allocated, used, and freed are not a part of my thought process.
Some software necessitates the programmer thinking about memory usage and optimization (games, simulations, machine learning, etc)
There are some cases where novel memory layouts are necessary. Especially in graphics programming where you need to, at times, cleverly lay out memory to use the most of every available buffer to create arbitrary visual effects.
Compilers can’t automatically create novel layouts.
You also need custom hardware sometimes, like TPUs. That doesn't make software unimportant.
The argument for FP was never that it was perfectly well-suited to every application-- merely that it was better-suited for your "typical" engineering tasks of writing business logic. FP, proof languages, and logic programming, are also all uniquely well-suited in situations that require correctness and formal verification (safety, aerospace, testing, etc).
To make a very broad, sweeping statement: if your project has a `node_modules` or a `venv`, then FP is the medicine you didn't know you needed. If you're writing low-level metal code / assembly, then you should already know you're not the target audience.
Maybe on HN 99% of people work on web.
In reality probably like 70%
Agreed, but is FP that?
When I write instructions to someone who does not know how to do something (like for my young kid or an aging parent on using some tech they're no familiar with) it will be strictly procedural. Step 1 do this, then step 2 do that, etc.
Pure functions are memoryless and deterministic.
Total functions are defined for all elements in its domain.
Square (x²) is a total function. Reciprocal (1/x) is not, since 0 is a real number, but has no reciprocal.
“Total” and “pure” are orthogonal concepts.
A pure functions that raises an error with the input 0/0 is not total, and you can have total functions that aren't pure.
Do you include "same-output-for-the-same-input" as part of defined?
But in general no.
I could say have a total function with an internal counter that adds 1 each time it was run.
That would still be a total function, but not pure.
It is no accident that CUDA and SYCL libraries are written in a functional way, or the AI middleware for compute.
A stateful program can execute in 2^n different ways for each bit of state for any given inputs.
If it only computes from an expression to an expression. I think the bound might be higher if you use imperative statements (/effects).
You can fill the whole 2^n output space by calling random(). But in addition to that, the program might also delete an arbitrary file, or deadlock, etc.
I think there's a lot to discover and apply to programming languages, but the successful result of that will be proving largely procedural programming languages as having certain properties such as memory safety.
Correctness itself is overrated (even in a safety critical field - you always assume the software is faulty and try to make a design that mitigates potential faults). Software is for utility, and even buggy software can have great utility.
So that we can prove things about software more easily. If we only write stateful imperative programs, we're stuck with tons of Hoare triples and separation logic rather than being able to use equational reasoning or type-driven deductions. For example, this person wrote a parallel wc in Haskell, and they used semigroups to parallelize the word counting.
Aspiring to rigorous reason and maximum reasonability is necessary for virtue. Maths is the way we reason rigorously about space and time.
Indeed it does. But why is this opposed to a connection to mathematics?