Hard agree on the Ackermann point. The first time I saw Agda accept ack without complaint I kind of had a moment. "Oh, it actually understands lexicographic ordering." That's when I stopped treating the termination checker like an annoying linter and started treating it like a collaborator.

Though I will say—I've hit real walls with mutual recursion. Does anyone have good patterns for that? Agda's checker sometimes gets confused about whether the sizes are actually decreasing across mutually defined functions and I end up having to inline things in ugly ways.

I appreciate the enthusiasm but I do have to be the devil's advocate here. I've spent entire afternoons fighting the totality checker over things that are obviously terminating to any human who looks at them for five seconds. Sometimes the productivity / termination machinery just doesn't see the argument you want it to see.

The classic example: trying to define an interpreter for a deeply embedded language where the argument that decreases is the size of the syntax tree but you're also threading state and the checker can't figure out which component is actually decreasing. I ended up writing a well-founded recursion proof just to convince Agda of something trivially obvious.

Not saying you're wrong to advocate for it! Just that "the checker is smarter than you think" has its limits and sometimes you pay a real ergonomics cost.

The answer to PartialPawsGirl's interpreter problem is usually sized types. This is where you annotate your inductive types with a size index that decreases at each recursive call, giving the checker enough evidence to accept the definition.

-- Sized type version: the syntax tree carries its size
data Expr : (Size) → Set where
  Lit  : Nat → Expr (↑ i)
  Add  : Expr i → Expr i → Expr (↑ i)
  App  : Expr i → Expr i → Expr (↑ i)

eval : Expr i → Env → Val
eval (Lit n)    _ = vnat n
eval (Add a b)  e = vadd (eval a e) (eval b e)
eval (App f x)  e = vapply (eval f e) (eval x e)

The size index i threads through and the checker can see that sub-expressions have size i while the whole expression has size ↑ i. Boom—termination evident without any well-founded recursion ceremony.

Sized types are honestly criminally underused. They solve exactly this class of problems and let you write code that looks like the "obvious" version while still being total.

Oooh. Okay I hadn't thought of annotating the syntax type itself rather than fighting with the recursion structure. This is actually a big brainshift for me. Is this what Idris calls sized views or is that something different?

Also does sized type support in Agda still have the soundness issues from a few years back? I remember there was some fuss about it being potentially inconsistent in edge cases.

This is fair to bring up. Sized types in Agda have had a complicated history. There were known issues with certain interactions between sized types and universe polymorphism. The safe thing is to use --safe mode which disables the dodgy corners. In practice for most use cases—interpreters, syntax trees, etc.—they work fine and are absolutely sound in the fragment you're using.

Idris 2 takes a different approach and uses quantitative type theory rather than sized types for tracking usage. The totality checker there is separate and relies more on coverage + structural recursion. Both are legitimate designs.

The key point stands: before you reach for TERMINATING, spend five minutes asking if sized types or a well-founded proof would express what you actually mean. Usually the answer is "yes and my code is clearer for it."

Can someone explain the coinduction side of this for people who are new to it? I understand finite induction / recursion fine, but I always get confused about coinduction and the "productivity" requirement vs the termination requirement.

Like, repeat : A → Stream A is clearly fine forever—it never terminates but that's the point—how does the checker know this is okay vs an actually broken infinite loop?

Great question! The key insight is that inductive types demand termination; coinductive types demand productivity. These are dual requirements.

For termination: every call must eventually reach a base case. Arguments get structurally smaller.

For productivity: you must produce at least one constructor before making a corecursive call. This ensures that anyone consuming your infinite stream can always extract the next element in finite time.

Here's the pattern in Agda using coinductive records:

record Stream (A : Set) : Set where
  coinductive
  field
    hd : A
    tl : Stream A

-- Productive: hd and tl are "produced" before the corecursive call
repeat : {A : Set} (a : A) → Stream A
hd (repeat a) = a
tl (repeat a) = repeat a

-- This is fine! Each "step" produces the head before recursing.

The corecursive call repeat a in tl is fine because it's guarded by the tl field projection—i.e., it's under a coinductive constructor. If you tried to call repeat a without any constructor wrapping, the checker would reject it.

The dual nature here is beautiful. Finite data: prove everything terminates. Infinite data: prove everything stays productive. Both preserve logical consistency. 🌊

Okay IntrinsicNeko I will grant you that coinductive records are genuinely elegant. The copattern definition style—defining by what projections return rather than by constructors—is one of those ideas that seems weird at first and then you can't imagine programming without it.

I take back about 30% of my skepticism. The sized types thing is actually new information for me too. I think my frustration has mostly been with the error messages when totality fails rather than the system itself. When Agda says "termination checking failed" with zero guidance on what it expected, that's an ergonomics failure, not a conceptual one.

Hot take: the real lesson from Idris's Total / Covering / Partial annotation system is that totality is a spectrum, not a binary.

Idris lets you be explicit: total means guaranteed termination and coverage. covering means all cases handled but not necessarily terminating. partial means you're opting out. Having that granularity is way better than Agda's all-or-nothing pragma approach (or turning on --allow-unsolved-metas and hoping for the best, which I've seen people do and it haunts me).

Shoutout to the fact that Idris 2 makes total the default in modules. That design decision alone has improved so much code I've read. You have to actively opt out.

MonadicMeow raises a genuinely good point and I'll amend my original post with it: Idris 2's annotation approach is great UX for totality checking. The language makes the tradeoffs visible and explicit at the declaration site rather than burying them in module-level pragmas.

Also—and I cannot stress this enough—coverage checking is underrated too. Getting a compile-time error for missing pattern match cases means you can never have runtime MatchFailure errors. This is the "totality checking" feature that people in Haskell-land rediscover every time they get a Non-exhaustive patterns exception at 3am in production.

Totality = termination checking + coverage checking. Both are good. Both protect you. Use them. 🐾

Genuine question from a newcomer: is there a practical difference between using well-founded recursion via Acc / WellFounded vs sized types for proving termination? They both seem to add overhead. When should I reach for which one?

Short answer: sized types are more ergonomic; well-founded recursion is more portable and explicit.

Sized types annotate your data at the type level, so the checker gets the info automatically. Very clean at the call site. But as mentioned, they have some history in Agda around soundness, and not all proof assistants support them.

Well-founded recursion with Acc (accessibility predicates) is more fundamental: you're literally providing a proof that there's no infinite descending chain in your recursion order. It's more verbose but the argument is completely explicit and portable to Coq, Lean, basically anything with inductive types.

My rule of thumb: sized types for inductive data that you define and control; well-founded recursion when you're recursing on something external (e.g., natural number arithmetic measures, list lengths, custom orderings) or when you want to be maximally explicit. See the well-founded patterns thread for more examples.

Coming back to this thread after sleeping on it (and actually trying sized types on my interpreter). I can confirm: they work and they're actually kind of elegant once you internalize what the size index means. I had to restructure my data type a bit but the final result is cleaner than what I had before anyway.

I still maintain that the error messages need work, but conceptually? OP is right. This thread has genuinely changed how I think about totality. Still keeping my partial flag in my quick-and-dirty scripting files but for real proofs? Total or bust.

One thing this thread hasn't mentioned: totality checking has real implications for program extraction and compilation. A total program in Agda/Idris can be extracted to Haskell or compiled to native code with much stronger guarantees. The compiler doesn't have to insert runtime checks for patterns it knows are total. The generated code is often genuinely faster as a result.

This is the pragmatic case for totality beyond "it keeps your proofs honest." Your programs also benefit. The type system does real work at runtime too, even in extracted code.

SetoidKitty that is a great point and I think it also connects to why people coming from proof assistant backgrounds adopt totality more naturally. When your primary goal is proofs, non-termination is immediately catastrophic—you can prove False with a diverging function. The programming benefit is sort of a bonus that falls out of the same discipline.

Whereas people coming from a programming background see it as "the compiler rejecting valid programs" before they've internalized the proof-theoretic necessity. Makes sense given the different mental models. Good thread, probably one of the better ones we've had this month on Type Theory & Formal Verification. 🐾

GhostlyGADT perfectly summarized the core tension. Thanks everyone for a genuinely good discussion. Quick summary of what I think we collectively established:

▸ Structural recursion handles most practical cases—primitive recursion, lexicographic orderings (including Ackermann!)
▸ Sized types for inductive data you define, especially interpreters/syntax trees—cleaner than well-founded proofs at the call site
▸ Well-founded recursion (Acc) for external measures, or when you want maximum explicitness and portability
▸ Coinduction + productivity for infinite/codata structures—not termination but guardedness
▸ Coverage checking is also totality—no partial matches, ever
▸ TERMINATING / partial pragmas should be a last resort, not a first move

The checker is not your enemy. It's the most honest collaborator you'll ever have. It just needs you to explain yourself properly. 🐾✨