Why every PFCL function terminates

Published July 2026 · PFCL on Codeberg

Most languages leave termination to the programmer: a loop that never exits is caught only when it runs, if at all. PFCL enforces totality at load time instead. If a catalog loads, every composed function in it terminates on every input of its declared type — not a discipline, a structural guarantee any process with the analyzer can verify.

Historical Lineage

David Turner argued for total functional programming in a 2004 paper, Total Functional Programming:

"The driving idea of functional programming is to make programming more closely related to mathematics. … A total functional language will not have the full expressive power of Turing machines, but it will still be capable enough to express any algorithm which we would ordinarily wish to write."

Turner's proposal: forbid unbounded recursion outright. Admit only structural recursion on inductive types. The result is a language that cannot express every computable function but can express every computation a working programmer needs.

Idris, Coq, Agda, and Dhall took versions of this position. Each pays a price. Idris/Coq/Agda ask the author to discharge a proof obligation the type system enforces — expressive but demanding. Dhall solves the problem by staying small, appropriate for configuration and not much else.

PFCL implements Turner's spirit with a different arrangement. Recursion is fenced, not forbidden. Domain code that needs it declares a witness. A single, explicit escape hatch exists and is named. And the guarantee extends to third-party code without extending trust to third parties.

What Problem Does This Solve?

Termination bugs in production systems are expensive. A parser that loops on adversarial input becomes a denial-of-service vector. A graph walker that recurses forever on a cycle takes down a service. A configuration reducer that never converges silently returns the wrong answer. These aren't hypothetical — they're the class of bug most retrospectives find in the "why didn't we catch this" column.

The received defences are testing, timeouts, and code review. Each is a stopgap. Testing checks the inputs you thought of. Timeouts convert a hang into a partial answer whose correctness is unspecified. Code review scales with the reviewer's attention.

A structural guarantee cuts the problem at the root. If the analyzer admits your body, it terminates. If it does not, you know before you ship.

How It Works

1. Fenced recursion

Recursion enters PFCL through a small set of scheme operators. A scheme operator is a recursion pattern whose termination is a property of the operator, not of any body using it. A fold over a list terminates because the list is finite. A bounded iteration terminates because the bound is a natural number.

Every body that uses only scheme operators, non-recursive primitives, and previously-admitted bodies terminates by construction. Admission composes: a composed function calling other admitted functions is itself admitted.

name: math.mean
type: List<Float> -> Maybe<Float>
body: |
  \(xs).
    match list.is_empty(xs) with
    | true  -> nothing
    | false ->
        just(float.divide(
          list.fold_left(\(acc, x). float.add(acc, x), 0.0, xs),
          int.to_float(list.length(xs))))

No recursion here beyond list.fold_left, a scheme operator. The analyzer admits math.mean immediately.

2. Witnessed exceptions

Some domain code needs recursion that no scheme captures. Parsers of self-referential wire formats, decoders of adversarial input, graph walkers over unknown topology — these are legitimate, common, and not reducible to structural descent without contortion.

Such code carries a witness: a declared, machine-checkable claim about why the recursion terminates. The analyzer discharges the witness syntactically, without executing the body. Three witness kinds are recognized: structural descent on an inductive argument, numeric decrease over a measure expression, and caller-supplied fuel that is verifiably decremented.

The rules are simple enough to inspect by eye. A witness is not a proof in the logical sense — it is a syntactic fact about the body's shape that the analyzer confirms in bounded time. If the witness holds, the body is admitted. If it does not, the body is refused at load time.

3. The one explicit escape hatch

Exactly one shape of recursion cannot be decided from the body alone: bounded iteration whose budget comes from the caller. Parsing an adversarial byte stream, walking a graph you cannot fully enumerate, running a numerical iteration to a fixed precision — the terminating quantity is a policy the caller imposes, not a property the body carries.

PFCL admits this shape through a single operator: fold_until. The caller supplies the budget. Budget exhaustion is a defined outcome — a value the caller receives, not a hang. There is no other channel to undecidability in the language.

fold_until(init, stop, step, max)
  = the state after either `stop` fires or `max` iterations run

A lint rule refuses to admit any body that uses fold_until without declaring where the budget comes from. Callers who want typed exhaustion (rather than a silent partial answer) use the fold_until_or_exhausted variant, which returns a tagged status.

4. Reproducible verdicts

A termination verdict is a fact any party who has the analyzer can independently confirm. This is not a property PFCL states about itself — it is a property PFCL uses.

A third-party author writes a domain module. Their body may need witnessed recursion; they attach the witness. Before shipping, they run the analyzer locally and it admits or refuses. On the user's machine, the analyzer runs again and admits or refuses the same body the same way. The user has not trusted the author; they have trusted their own analyzer.

This is what makes the guarantee extend across authorship boundaries. A user of a third-party module verifies its termination themselves. The trust root is the local analyzer, not the third party.

Why This Beats "Just Test It"

Comparison with Other Total Languages

Idris/Coq/Agda suit authors who are proof engineers — the burden is real but the payoff is unbounded. Dhall suits languages that stay small. PFCL targets domain code authored by working programmers — parser writers, protocol implementers, graph walkers — where end users need to verify what they run without becoming proof engineers themselves.

Current State

Totality in PFCL ships as:

• Load-time analyzer with three witness kinds (structural, numeric, fuel)
• Content-addressed stamp file recording every discharged witness by body hash
• Lint rules enforcing witness declaration on every recursion carrier
• Certificate mechanism for third-party attestation, re-verified locally
• fold_until as the sole channel to undecidability, budget-required, exhaustion-typed

Planned improvements:

• Mechanical soundness proof of the analyzer's own rules (the analyzer is currently trusted-but-not-verified)
• Adversarial test corpus for the certificate checker
• Analyzer versioning discipline for reproducible verdicts across releases

Limitations

Three things this model does not do:

• Analyzer soundness. Not mechanically verified. Rules are simple enough to inspect and are tested against a corpus, but "sound" rests on inspection, not proof. Future work.
• Fuel channel. A body using fold_until can consume its budget without reaching a stop condition, by design — some domain problems need bounded computation over adversarial input. "PFCL is total" carries an implicit "up to the fuel channel" clause. The channel is fenced, declared, and reported.
• Termination ≠ correctness. A total function that returns the wrong answer is still wrong. The guarantee covers whether a function halts, not whether it computes what you meant.