Total Functional Programming (2004) [pdf]
ncatlab.org
ncatlab.org
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.
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.
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.
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.
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".
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.
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.
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.
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.
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.
Aspiring to rigorous reason and maximum reasonability is necessary for virtue. Maths is the way we reason rigorously about space and time.
It is no accident that CUDA and SYCL libraries are written in a functional way, or the AI middleware for compute.
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.
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.
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.
Indeed it does. But why is this opposed to a connection to mathematics?
Some minor nitpicks:
> In total functional programming ⊥ does not exist.
That doesn't seem right. In total FP, we can still define a ⊥ type that has no values. I think the problem here is that the author uses ⊥ to indicate both a type and a value of that type (e.g. f ⊥ = ⊥), which is confusing.
> 0 / 0 = 0
Surely it would be better to use a Maybe type for this instead?
0 / 1 = Just 0
0 / 0 = Nothing
hd :: List a -> Maybe a
hd (Cons a x) = Just a
hd Nil = Nothing
This would make it impossible to compose mathematical expressions of more than one operation without discharging the Maybe which would get ugly fast.
Practically speaking, languages like Haskell and F# have a monadic syntax that makes this considerably less ugly.
Total functions have to return either true or false explicitly, failure as negation doesn't work.
That is where you get Gödel's 'this statement is false' from.
This is the law of the excluded middle that broke the Mathmatica Principia.
Plato, Aristotle, and Russell's use of the law of the excluded middle is what Gödel, Church, and Turning leverages.
For problems in P this distinction is harder to see because P=co-P but we think NP!=co-NP.
As NP are by definition decision problems this is important.
NP being the provable yes-instances and co-NP being the no-instances, even proving a function is total is hard.
If you accept failure as negation you may be able to build a sun-Turing machine that always halts but you won't be able to show it is complete and consistent.
That is why ZF disallows statements like 'this statement is false'.
It's best left to the compiler.
But if you're considering doing it, don't imagine yourself taking an existing function like qsort and trying to prove it's total. Instead try building up a new function and only build it out of other total functions.
As all primitive recursive functions are provably total, that is a place a compiler can work. But just using for loops gets you there too.
Total functions that are also pure functions are a pretty small set so there may be other reductions like the above. But don't depend on the compiler.
But I agree writing total functions from the start is the ideal if possible.
For example, in Lean4:
def myDiv (numerator : Nat) {denominator : Nat} (denominatorNotZero : denominator ≠ 0) : Nat
:=
if denominator > numerator then
0
else
1 + myDiv (numerator - denominator) denominatorNotZero
-- Example usage.
example : myDiv 1 (denominator := 1) (by simp) = 1 := rfl
example : myDiv 120 (denominator := 10) (by simp) = 12 := rfl
I feel like you would just end up with the equivalent of Maybe, but not sure.
Just in time for people to ignore it and start complaining about the ugliness of flatMap from 2015 onwards.
I'd like to counter that a function from vector of bytes to vector of bytes can be pure, terminating, implement some algorithm of great commercial interest and map exactly onto a program that reads said vector of bytes from stdin and sends them to stdout.
If you're really generous, it can write two vectors of bytes, and tie the other one to stderr.
That covers such useless academic things as your compiler.
IO in -> pure stuff of interest -> IO out
If write is sending bytes to somewhere else, it's pure. In exactly the same way that returning a value type from a function is pure, or passing a value type to some other function is pure. Since they're all the same thing. A unix process is a function in a literal sense.
If you've aliased read and write to the same thing then mutation is back with us and sorrows return.
Vaguely tangential, it's totally possible to write a program that uses read() to copy all of stdin to its own address space allocated with brk(), does whatever maths it wants, then sends some of the result back out with write(). Three syscalls, useful userspace program, no libc involved.
[1] Boundaries by Gary B. from Destroy All Software https://www.youtube.com/watch?v=yTkzNHF6rMs
fib :: Nat->Nat
fib 0 = 0
fib 1 = 1
fib (n+2) = fib (n+1) + fib (n+2)
The last line should be fib (n+2) = fib (n+1) + fib (n). The published version seems to have the same problem: https://pdfs.semanticscholar.org/82b4/ea72b89270c528006dd253...
(which mentions http://pll.cpsc.ucalgary.ca/charity1/www/home.html )
It seems like the big idea here is that Int->Int always, no errors, faults, 'impact by extra data'.
Isn't that all also solved by pure functions? And is incorporated into functional languages at this point?
Regardless, Haskell has turing complete type evaluation (if you turn on UndecidableInstances) and thus potentially non-terminating compilation.
> Type checking in my idea would actually produce artifacts that you’d store with your code essentially saving the state of type checking up to whatever bounds had been reached since the last code change.
The incrementality would be new.
Turner proposes a language for pure total functions.
Well no. This is computer science 101. Anything that can compute anything useful (ie. Turing complete or lambda-calculus-complete... they're equivalent) cannot be said to produce an answer in finite time (or at all really). In FP parlance, we say that such functions are a 'bottom' value. The notation 'Int -> Int' in a language like haskell is a function that takes an Int and returns an Int, if it terminates.
In a total language, you're guaranteed to have an Int after invoking the function within a finite amount of time, even if that time is greater than the age of the universe. But it will eventually return an answer. Whereas a haskell program may truly never terminate.
Here is an example of a haskell program that is syntactically correct and well-typed but is actually a bottom, despite the type signature claiming in returns Int
f :: Int -> Int
f x = f xIf you take any current functional language, and add the criteria that it must only use pure functions, then Int->Int is the same as described in the Total Language. Because if there are no outside interactions inside the function, it's 'pure', then the Int->Int is guaranteed.
Doesn't using only pure functions, equate to this Total Functions.
From random search, seems like some people assume this : Pure=Total
"A pure function must be total Firstly, a function must be total, this means that for each input that is provided to the function there must be a defined output."
The function above is pure. In fact, all functions in Haskell are, even those returning IO.
So they would match the criteria of the original post?
By some definitions, to be 'pure' includes being 'total'.
Guess, back to original question. The ideas in this paper from 2004, seems to have been incorporated into more common languages like Haskell in 2024.