I’ve had an idea for a language like this for a while now that wouldn’t exactly “type check” in the sense that the unification finishes but that the “type checking” would be continuously running in the background as you’re programming. This co-data approach seems interesting toward that goal
I’m not too familiar with any of those languages but I’m guessing the difference is that type checking does eventually “finish” in those languages and that to accomplish this, the type systems are necessarily not Turing-complete, whereas I’m suggesting the alternative. 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. Kind of like a combination of type checking and unit testing that takes advantage of pure functional programming
But "type checking" that's Turing complete is not type checking at all, it's just a phase distinction. It's no different than choosing whether to run code at "compile" vs. "run" time, except that in practice, we don't even want to have fully Turing-complete compile workflows that might, e.g. not terminate. Dependently typed languages implement this phase distinction via program extraction: you "extract" the code to be fed into the "runtime" phase of execution.
Agda and Idris have undecidable type systems (in certain circumstances). But otherwise, if you're using the 'safe' versions of those languages, then I believe the language itself is not Turing complete.
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.
No; purity is an orthogonal notion.
Haskell functions are pure in that given the same arguments, a function always produces the same output.
But Haskell functions can be partial; for some arguments there is no output, or the output is undefined.
Turner proposes a language for pure total functions.
> It seems like the big idea here is that Int->Int always, no errors, faults, 'impact by extra data'.
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
If 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."
> If 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.
The function above is pure. In fact, all functions in Haskell are, even those returning IO.
No. Haskell has this notion of what they call "bottom", more easily remembered as what happens if you call undefined. The issue is, your function can be as pure as it wants, as long as you are able to write "f :: T -> T; f = undefined" all your purity based analysis goes to hell.
Think original question I had, was if you make "f = undefined" be Pure. Don't leave undefined. It has a defined signature Int->Int. Then "f" should return Int every time guaranteed, and would be equivalent of the Total Functional case.
Even if undefined were not allowed, you'd still be able to write "f :: Int -> Int; f x = f x" which would never return an Int. Totality is about getting a grip on these cases. As mentioned more elquently then I could in this thread, it has been proven long time ago that termination-analysis is impossible to achieve. What Idris for instance does is to use proofs, adn to an extend heuristcs, to stil decide in special cases that a function is total, IOW terminates. Thats a pretty cool part of CS, since we're basically knowing something is impossible but still make small steps towards tackling the issue at least for some cases we care about.
> to make programming more
closely related to mathematics
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.
As you say, you cannot make a 100% side-effect free program, unless it doesn't do anything at all.
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.
Practicing software architecture should generally lead you to minimize side effects and efficiently manage sections of state small enough to fit into your working memory IMO.
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.
> it strongly optimizes for readability of experts in most cases which harms readability in general
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.
Very much so to all of this. When I started programming I was just messing around and doing so as more of a curiosity than anything. What I came up with on my own was much closer to FP. When I started to really learn and was presented with OO, it took me what felt like a really embarrassingly long time to under how classes worked and why I'd want them. Once I grokked it I had a grand ol' time, but then I learned a functional language and it felt so good to learn an actual well-designed version of how I initially imagined programming should be :)
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.
There are many situations where the extra constraints on pure functions are very useful. Pure functions can't segfault. They can't overwrite memory used by other parts of your program due to stray pointer references. They can't phone home to Google. Verification and optimization is often much simpler when you know that some functions are pure. Reactive programming frameworks that execute callbacks in response to events can cause really weird bugs if the callback mutates state somewhere. I could go on and on. Nobody is arguing for pure functions all the way down. A program's top-level functions will usually be side-effecting, and then you can call out to pure code any time. In practice, a surprising amount of application logic can end up being pure functions.
It allows you to separate non-stateful business logic from the stateful update logic. Reactive frameworks usually handle the state mutation for you, eliminating the potential for UI glitches where something that depends on the updated state doesn't get recomputed/redrawn.
I’d rather a language is designed to accommodate the human mind, and work back from there through the compiler to figure out how to map that to the capabilities of the hardware, than the reverse.
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.
Thinking about memory usage and optimization is the role of the compiler. The fact that some software necessitates the programmer thinking about it is just a consequence of current technology.
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.
We've been waiting for a "sufficiently advanced compiler" for a very long time. If you're going to write programs for real computers, using real compilers, sometimes you have to care about such things. (If you're going to write programs for hypothetical computers, using hypothetical compilers, such constraints don't apply to you. Have fun running them, though...)
That is absolutely and totally true, but 99.9999% of engineers are probably working on things like web apps or other high-level code.
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.
> I’d rather a language is designed to accommodate the human mind
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.
If you have a goal of being able to confidently reason about your code, such as to be confident it won't go "wrong", then making it more math like would seem to make a lot of sense.
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.
> If you have a goal of being able to confidently reason about your code, such as to be confident it won't go "wrong", then making it more math like would seem to make a lot of sense.
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...
> 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.
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.
You don't do a single proof of the entire 10k line program, you do proofs of the many small functions that make it up. If you can use each proof as an axiom going into proving the functions that use it, then each of them becomes easier to prove too. If I have a function that might sometimes mutate a variable off in another part of the program, that's just inherently harder to reason about that one that is idempotent and guaranteed to have no side effects.
The most common proofs are those that the compiler constructs while type checking. The compiled program is the proof witness. All compilers can be thought of as producing a proof-by-construction but they vary wildly in the propositions they can prove.
If this idea is new to you and you want to learn more, google "propositions as types" or "the curry howard correspondance".
Well, why would it be taken as a given that programming should mimic the hardware?
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.
>Well, why would it be taken as a given that programming should mimic the hardware?
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.
> doing anything else is fighting against the environment
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 academia, and the especially academic, utopian realm of functional programming, you're trained to live in dreamland.
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).
> A huge majority of applications can afford to be written this way, even ones where performance is a concern
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.
My comment was in response to the need to squeeze out every last bit of performance you possibly can. You're talking about ignoring performance altogether which is not what I'm talking about.
Then again, abstractions can be helpful too, including in game programming. Epic's heavily invested, for example. Or in databases, relational algebra often beats out an array with linear access. I agree that OOP-in-the-small lacks mechanical sympathy though. That's one reason for entity-component-model, though another, I'd argue, is that it provides abstractions that are easier to reason about.
On Epic's case it helps that Tim Sweany started his game company doing games in VB, and always cared for a good developer experience, that is why Unreal Engine always favoured good abstractions, has a C++ GC, Blueprints and now Verse.
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.
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.
And if I go to a flat earth conference, I will find that they produce lots of “proof” for flat earth.
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”.
>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.
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.
> Why is this taken as a given to be a good thing?
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.
It's honestly wild to see this even being argued about in 2024. Ten years ago, I remember the discussions around FP being universally "yes of course it's better, but what's the best way to make it practical in the real world where you need side effects".
> Why is this taken as a given to be a good thing?
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.
> 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 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.
You could say the same thing about variables, expressions, statements, and structured programming. It's a lot higher level than assembly language or machine code programming.
> 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.
It allows the scalability of algorithms like Star Lisp on the Connection Machine, the abstraction allows algorithms to be easily moved from single thread , to multiple threads, multiple cores, GPGPU.
It is no accident that CUDA and SYCL libraries are written in a functional way, or the AI middleware for compute.
> Why is this taken as a given to be a good thing?
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.
Yeah I don't think this is a good thing, I also wonder; which mathematics? Mathematics is a big field with wildly different and incompatible notations.
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.
I like how Lean4 handles totality. You can tell the compiler to trust you. Or you can provide a proof. The latter is more useful while the former is sometimes pragmatic.
In page 2, there is the theorem: Theorem ∀n in Nat.f n (fib p) (fib (p+1)) = fib (p+n), I think it should be for all p in Nat (fib p) + (fib (p+1)) = fib(p+2), otherwise there is something mysterious here.
The fib' function (the more efficient version of fib) is defined using f. So the goal is to prove that f computes the same thing as fib (given the appropriate arguments to f and fib). Hence the theorem needs to use f on at least one side of the equation.
A few comments have cheerfully reproduced the stock objection that a program with no side effects does nothing and is thus useless. By extension functional programming is useless and it's all pointless.
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.
I guess that depends on whether you consider write(2) to have side effects. No, really, I've been in the room when people debated whether that was pure enough. It's an interesting exercise to talk through, at least.
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.
This talk [1] made me conclude something along these lines. You need side-effects to make anything useful, just make sure they're segregated in a specific place in your program. This makes it easier to make most of the program pure and make it clear where the dangerous stuff happens.
I appreciate this article. It's clear, easy to understand, and uses theory to propose practical improvements to FP.
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
The same approach also addresses the difficulty of hd:
hd :: List a -> Maybe a
hd (Cons a x) = Just a
hd Nil = Nothing
F# has this function, and calls it "tryHead", rather than just "head".
It seems like it would be more practical to create non-zero integer/other number types, and only those can be used as denominators. But it would also be nice to not have to make a custom subtype every time you needed something with a specific property.
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'.
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.
If your language is TC and thus supports general recursion, no algorithm can possibly exist for deciding whether a function is in fact total in the general case.
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.
It was ugly. And then do-notation arrived in around 1999 (I think - I'd be super happy if someone can find a precise year for me) and it became a solved problem.
Just in time for people to ignore it and start complaining about the ugliness of flatMap from 2015 onwards.
101 comments
[ 3.3 ms ] story [ 191 ms ] threadIt 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
If 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.
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",
http://lambda-the-ultimate.org/node/1277
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.
https://chrispenner.ca/posts/wc
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?
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.
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
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?
The same approach also addresses the difficulty of hd: F# has this function, and calls it "tryHead", rather than just "head".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:
You have to submit a proof that the denominator is non-zero in order to use `myDiv`. No monad required ;).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.
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 )