Reversible Functional Programming
Janus is an imperative language: state, updates, loops. But half the programming world thinks in
functions — no
mutable state at all, just values flowing through definitions by pattern matching. Can that
world go reversible? At first the fit looks perfect: a functional program simply is a
function, so "reversible functional programming" should just mean "programming with
injective functions" — functions where distinct inputs always give distinct outputs,
so every output determines its input.
The interesting part is how a language can guarantee injectivity by looking only at the shape of
your code. The answer, worked out in languages like RFUN and its successors, is
a beautifully symmetric discipline: the pattern-matching rules you already apply to
inputs get mirrored onto outputs — plus a strict rule that no value may ever be
silently copied or thrown away.
The symmetric pattern discipline
A first-order functional definition is a list of branches, each matching an input pattern and
producing a result. Ordinary functional languages impose two conditions on the input side,
and reversible ones add the mirror image on the output side:
- Input patterns must be exhaustive (every value matches some branch)
and non-overlapping (no value matches two) — this makes the forward direction a
well-defined function.
- Output shapes of different branches must also be non-overlapping — no
value can be produced by two different branches. This makes the backward direction
well-defined: given a result, its shape alone identifies which branch produced it, and the branch
can be run in reverse.
- Each branch body must itself be built from reversible parts.
The output condition is the functional twin of Janus's exit assertion: where Janus writes
fi e to record which branch ran, a reversible functional program records it in the
shape of the result. Same information, different home. A definition that satisfies both
conditions denotes an injective function, checkable branch by branch, without running anything.
Watch the discipline separate a good definition from a bad one:
// BAD: two branches whose outputs overlap.
// f(0) = 1
// f(n + 1) = n (i.e. subtract one from a positive number)
function bad(n: number): number {
if (n === 0) return 1; // branch 1 can output: 1
return n - 1; // branch 2 can output: 0, 1, 2, ... — overlap!
}
console.log("bad(0) = " + bad(0) + ", bad(2) = " + bad(2));
console.log("two inputs, one output: backward execution is stuck.");
// GOOD: branch outputs kept apart, so the inverse can dispatch on shape.
// g(0) = 0 outputs: { 0 }
// g(n + 1) = n + 2 outputs: { 2, 3, 4, ... } — no overlap
function good(n: number): number {
if (n === 0) return 0;
return n + 1;
}
function goodInv(m: number): number {
if (m === 0) return 0; // only branch 1 outputs 0
if (m === 1) throw new Error("1 is not in the range of good");
return m - 1; // must have been branch 2
}
for (const n of [0, 1, 2, 5]) {
const m = good(n);
console.log("good(" + n + ") = " + m + " goodInv(" + m + ") = " + goodInv(m));
}
Note the little surprise in goodInv: an injective function need not be
surjective, so the inverse is entitled to reject values (here 1)
that the forward function can never produce — just as Janus halts on a failed assertion.
Use everything exactly once
Pattern rules police the branches; a second discipline polices the variables. In a
reversible functional language every bound variable must be used exactly once — the
linear-use discipline. Both ways of breaking it destroy reversibility, for opposite
reasons:
- Zero uses = forgetting. A branch
f(x, y) = y discards
x. Whatever x was, the output is the same — the definition cannot be
injective. Silent discarding is exactly the "overwrite" sin of imperative programming, wearing
functional clothes.
- Two uses = hidden copying. A branch
f(x) = (x, x) duplicates
x. The forward direction is actually injective — the trouble comes backwards: the
inverse receives a pair (a, b) and must check that
a = b before collapsing them, and reject the input otherwise. That
equality check is real computational content, so the language refuses to insert it silently.
Duplication is therefore provided as an explicit operator — often written
\lfloor \cdot \rfloor in the RFUN literature — whose forward direction
copies and whose backward direction is equality-check-then-merge. Copying isn't banned; it
is priced:
// The duplication/equality operator: one operator, two readings.
function dup(x: number): [number, number] { // forward: copy
return [x, x];
}
function dupInv(pair: [number, number]): number { // backward: check, then merge
const [a, b] = pair;
if (a !== b) throw new Error("dup-inverse: " + a + " != " + b + " — this pair was never made by dup");
return a;
}
console.log("dup(7) = " + JSON.stringify(dup(7)));
console.log("dupInv([7, 7]) = " + dupInv(dup(7)));
try {
dupInv([7, 8]);
} catch (err) {
console.log("dupInv([7, 8]) -> " + (err as Error).message);
}
Worked examples: zip, and Fibonacci again
The classic list combinators fit the discipline beautifully. zip pairs up two
equal-length lists; every variable is used once, and the output (a list of pairs) determines both
inputs — so unzip is its exact inverse. And a reversible map works the same
way: mapping an injective function over a list is injective, and its inverse is mapping the inverse.
function zip(xs: number[], ys: number[]): [number, number][] {
if (xs.length !== ys.length) throw new Error("zip: lengths differ");
const out: [number, number][] = [];
for (let i = 0; i < xs.length; i++) out.push([xs[i], ys[i]]);
return out;
}
function unzip(ps: [number, number][]): [number[], number[]] {
const xs: number[] = [], ys: number[] = [];
for (const [x, y] of ps) { xs.push(x); ys.push(y); }
return [xs, ys];
}
const zipped = zip([1, 2, 3], [10, 20, 30]);
console.log("zip -> " + JSON.stringify(zipped));
console.log("unzip -> " + JSON.stringify(unzip(zipped)));
// Reversible map: map an injective f; invert by mapping f's inverse.
function mapF(xs: number[]): number[] { return xs.map(function (x) { return x + 100; }); }
function mapFInv(ys: number[]): number[] { return ys.map(function (y) { return y - 100; }); }
console.log("map -> " + JSON.stringify(mapF([1, 2, 3])));
console.log("unmap -> " + JSON.stringify(mapFInv(mapF([1, 2, 3]))));
Fibonacci — the same example you traced in
Janus — becomes a
pure function from n to a pair of consecutive Fibonacci numbers.
Returning the pair rather than a single number is not a stylistic choice: a single Fibonacci number
would forget n's worth of structure, but the pair
(F_{n+1}, F_{n+2}) determines n uniquely. The
branch outputs stay disjoint — the base case is the only equal pair — so the inverse dispatches on
exactly that:
function fibPair(n: number): [number, number] {
if (n === 0) return [1, 1]; // only branch producing an EQUAL pair
const [a, b] = fibPair(n - 1);
return [b, a + b]; // always unequal beyond [1, 1]
}
function fibPairInv(pair: [number, number]): number {
const [a, b] = pair;
if (a === b) return 0; // shape says: base case
return fibPairInv([b - a, a]) + 1; // un-shuffle, recurse
}
for (let n = 0; n <= 6; n++) {
const p = fibPair(n);
console.log("fibPair(" + n + ") = " + JSON.stringify(p) +
" fibPairInv -> " + fibPairInv(p));
}
Everything that could possibly be left. These languages are r-Turing complete: they
compute exactly the computable injective functions — every injection a Turing machine can
compute, a reversible functional program can compute, and (by construction) nothing non-injective
ever sneaks in. That "exactly" is the healthy notion of completeness here: demanding ordinary Turing
completeness would be demanding the ability to forget. And thanks to the embedding tricks from
reversibility
and computability, any function you actually care about can be made injective by
carrying a little extra output — just as fibPair carried a pair where one number would
have forgotten too much. So the expressive loss is precisely zero, paid for in output width rather
than in erasure.
A common trap: checking that a definition is injective as a whole and declaring victory. The
discipline demands more — each branch's outputs must be recognisably distinct, so
the inverse can decide, from the output alone, which branch to invert without searching.
You can write an injective function whose branches overlap in range (the overlap just never happens
to bite for reachable inputs) — but then backward execution has no local way to dispatch, and the
"inverse" degenerates into generate-and-test. The syntactic output condition is deliberately stricter
than semantic injectivity: it is injectivity with an efficient, checkable witness. That's
the trade running through this whole module — reversible languages restrict how you may write
programs precisely so that inversion stays a compiler pass, not a search problem.