The Verse Calculus: A Mathematical Core for Functional Logic Programming

1. A Game Language with an ICFP Paper

In 2023, eight authors including Simon Peyton Jones, Tim Sweeney, and Lennart Augustsson published the paper “The Verse Calculus: a core calculus for deterministic functional logic programming” at ICFP, the premier conference in functional programming. It is rare enough for industry to write a formalization paper about its own scripting language; rarer still is this author list — the language’s boss (Sweeney) and a grandmaster of functional programming (Peyton Jones) signing side by side.

What the paper does can be explained with one analogy: what the lambda calculus is to functional languages, the Verse calculus is to Verse. The lambda calculus is a minimal set of mathematical rules that every functional language’s behavior ultimately reduces to; the Verse calculus is Verse’s own “minimal core” — strip away all the syntactic sugar, and what remains is the bare machine that never lies.The Verse calculus is Verse stripped down to its skeleton — its “minimal core.” A classic mathematician’s move is to give a language a tiny, honest set of rules, such that everything that happens in the language ultimately reduces to those rules; peel away all the conveniences that merely make code comfortable to write, and this bare machine is what remains.

2. The Core Trio: Unification, Choice, Determinism

The Verse calculus rests on three core ideas, each matching an “odd design” you will meet in the main lessons:

• ◇ Variables are bound by unification. A variable is not “a box that holds a value” but “an unknown waiting to be solved”; running the program feels a bit like solving equations — making both sides of an equality hold. That is why a lone = in Verse is a “failable equality” rather than assignmentrather than stuffing a value into a variable (the stuffing job is a Set node in Blueprints, and is written set in Verse).
• △ Expressions can yield multiple values (choice sequences). The result of an expression is not necessarily one value; it may be a “choice space” made of a string of candidate values. What for does is, at heart, walk through every success value of an expression.
• △ A computation can spit out several values (called a “choice sequence”). The result of a computation is not necessarily a single value; it may be a “choice space” made of a string of candidates. And what for (the ForEach Loop from Blueprints) does is, at heart, walk through that string of successful values one by one.
• ▢ The whole language is “deterministic” functional logic programming. Logic languages are often criticized because results depend on solver order; the Verse calculus guarantees that the same program always has exactly one result. Your level logic will not “produce this result today and that one tomorrow.”
• ▢ The whole language is “deterministic” — the same program only ever runs to one and the same outcome. Some programming traditions give different answers depending on internal evaluation order; Verse closes that door mathematically: your level logic will not “produce this result today and that one tomorrow.”

The paper equips this core with a small-step rewrite semantics — how a program gets rewritten and simplified one small step at a time — and proves that for well-behaved program fragments (the paper calls them “terms”), the rewrite system is confluent: no matter what order you simplify in, everything converges to the same result. That means you can apply equivalence-preserving transformations to Verse programs the way you manipulate math formulas — giving compiler optimization and program verification solid ground to stand on.

3. Mapping the Theory Back to Your Code

Sounds esoteric? You were already standing on this theory back in Lesson 1. Two minimal examples:

# = is not assignment; it is one "failable equality" check
# Failable expressions may only live in a failure context like if
if (2 + 2 = 4):
    Print("Math has not broken")

# for walks the entire "success space" of an expression
for (I := 1..3):
    Print("Round {I}")

Graph translation (Blueprint view): the top half is a Branch node — except instead of asking True/False, it asks “does the path 2 + 2 = 4 go through?”, and only prints once it does. The bottom half is a ForEach Loop: 1..3 acts like an array holding 1, 2, and 3, and the Print in the loop body runs once for each of them, so three “Round” lines show up in the log.

First half: 2 + 2 = 4 is an equality test — if it holds, the if branch runs; if not, it fails quietly. No true/false flows through the code: “failure” itself replaces the boolean. Second half: seen through the calculus, 1..3 is a choice sequence yielding the three values 1, 2, and 3, and for walks that choice space once — hence three “Round” lines in the log. The tutorial’s metaphors — “dice rolls,” “failure contexts” — each have a precise mathematical counterpart in the paper.

If you want to hear the designers explain it themselves, the joint Lambda Days 2023 talk by Peyton Jones and Sweeney, “Beyond functional programming: a taste of Verse”, is the best introduction — one hour that makes “if is a failure context” and “for walks the choice space” crystal clear.

4. Quick Check

Sources & Further Reading

This page draws on the paper page on Simon Peyton Jones’s personal site and the public Lambda Days 2023 talk:

• The Verse Calculus paper page (simon.peytonjones.org) ↗
• Talk: “Beyond functional programming: a taste of Verse” (YouTube) ↗