Accumulators in Haskell

(CW: coding exercise/study with zero higher purpose.)

In Paul Graham's 2002 essay, Revenge of the Nerds, Graham suggests one metric for the expressive power of a programming language: the ease of writing an accumulator.

[An accumulator is] a function that takes a number n, and returns a function that takes another number i and returns n incremented by i.

For example:

x = accumulator(7);
x(1); // 8
x(3); // 11
y = accumulator(-1);
y(1); // 0

In the parlance of OOP, an accumulator is a NumberIncrementerFactory. In the parlance of programming language theory, an accumulator produces a canonical example of a closure: a function together with a stateful external environment.

Graham uses the relative difficulty of writing accumulators in various languages to demonstrate the elegance/clumsiness of writing non-trivial code in them. (Of course, along with any notion of a metric comes Goodhart's law: a metric stops measuring anything useful if people start treating it as a target. If there are joke languages purpose-built to make writing quines easy, you can bet someone's written a language where there are accumulators as a language primitive.)

“Mountains should be climbed with as little effort as possible...”

Mountains should be climbed with as little effort as possible and without desire. The reality of your own nature should determine the speed. If you become restless, speed up. If you become winded, slow down. You climb the mountain in an equilibrium between restlessness and exhaustion. Then, when you’re no longer thinking ahead, each footstep isn’t just a means to an end but a unique event in itself. This leaf has jagged edges. This rock looks loose. From this place the snow is less visible, even though closer. These are things you should notice anyway. To live only for some future goal is shallow. It’s the sides of the mountain which sustain life, not the top. Here’s where things grow.

But of course, without the top you can’t have any sides. It’s the top that defines the sides.

Zen and the Art of Motorcycle Maintenance, by Robert Pirsig (1974).

^* Boldface mine.

Knowledge out of nowhere: a note on Löb's theorem

Löb's theorem states that for any extension of Peano arithmetic, any “reasonable” intra-system definition of the term ‘provable’ and any statement \(P\):

If \(PA \vdash (Provable(P) \rightarrow P)\) (“\(PA\) proves that (a proof of \(P\) implies the truth of \(P\))...”), then \(PA \vdash P\) (“\(PA\) proves \(P\)”).

Example. Let \(P\) be “\(0 = 1\)”. Assume \(PA \vdash \lnot Provable(0 = 1)\) (i.e. PA proves that there is no proof of \(0 = 1\), or: \(PA\) proves its own consistency.)

Then by explosion, \(PA \vdash (Provable(0 = 1) \rightarrow 0 = 1)\), and by Löb's theorem, \(PA \vdash 0 = 1\) (i.e. \(PA\) is inconsistent). This result is Gödel's second incompleteness theorem.

There’s a stronger consequence at play from this strategy here — a consistent extension of \(PA\) can’t prove the unprovability of anything within it, even what looks like blindingly obvious examples.

Consider the example of \(PA_x\), which is exactly Peano arithmetic with the introduction of an additional named constant, \(x\). Notably, \(x\) does not appear in any of the axioms. \(PA_x\) implies nothing about \(x\) that it doesn’t already imply about other numbers.

Then by the same reasoning, if \(PA_x \vdash \lnot Provable(x = 0)\), then \(PA_x \vdash x = 0\). This conclusion is ridiculous, since from the “outside view” we can see that there should be no proof of \(x = 0\) within the system. Given a model of \(PA\) (such as the natural numbers), we can easily construct a model of \(PA_x\) where \(x \neq 0\).

Assuming the consistency of \(PA_x\) (which trivially follows from the consistency of \(PA\)), this implies that \(PA_x \not \vdash \lnot Provable(x = 0)\). But why can’t \(PA_x\) prove the unprovability of the statement?

Credit: Geometry Daily