Tier 7: Totality Checking

Section

Mix.install([
  {:haruspex, path: "/Users/quinn/dev/beam_box/haruspex"},
  {:roux, path: "/Users/quinn/dev/beam_box/roux"},
  {:pentiment, path: "/Users/quinn/dev/beam_box/pentiment"},
  {:constrain, path: "/Users/quinn/dev/beam_box/constrain"},
  {:quail, path: "/Users/quinn/dev/beam_box/quail"}
])

Tier 7 adds opt-in totality checking via the @total annotation. When a function is marked @total, the compiler verifies that it terminates by checking structural recursion — at least one parameter must decrease structurally in every recursive call.

This is a classic technique from proof assistants (Agda, Coq, Lean) adapted for a BEAM language. Functions without @total skip the check entirely, preserving Elixir’s default of allowing general recursion.

What this demo covers

1. Direct API — Haruspex.Totality.check_totality/4 on hand-built core terms
2. Accepted examples — Nat addition, list length, trivially total (no recursion)
3. Rejected examples — infinite loop, argument increase, nested recursion f(f(x))
4. Full pipeline — @total functions compile and run; non-total rejected at check time
5. Non-@total functions — recursive but unchecked, type checking succeeds

Setup

alias Haruspex.Totality

# Nat ADT: type Nat = zero | succ(Nat)
nat_decl = %{
  name: :Nat,
  params: [],
  constructors: [
    %{name: :zero, fields: [], return_type: {:data, :Nat, []}, span: nil},
    %{name: :succ, fields: [{:data, :Nat, []}], return_type: {:data, :Nat, []}, span: nil}
  ],
  universe_level: {:llit, 0},
  span: nil
}

# List ADT: type List(a) = nil | cons(a, List(a))
list_decl = %{
  name: :List,
  params: [{:a, {:type, {:llit, 0}}}],
  constructors: [
    %{name: nil, fields: [], return_type: {:data, :List, [{:var, 0}]}, span: nil},
    %{
      name: :cons,
      fields: [{:var, 0}, {:data, :List, [{:var, 0}]}],
      return_type: {:data, :List, [{:var, 0}]},
      span: nil
    }
  ],
  universe_level: {:llit, 0},
  span: nil
}

adts = %{Nat: nat_decl, List: list_decl}

# Helper to create a fresh Roux database with haruspex registered.
new_db = fn ->
  db = Roux.Database.new()
  Roux.Lang.register(db, Haruspex)
  db
end

# Helper to purge compiled modules between examples.
purge = fn mod ->
  :code.purge(mod)
  :code.delete(mod)
end

:ok

How structural recursion checking works

Haruspex.Totality.check_totality/4 operates on checked core terms (post type-checking, de Bruijn indexed). It takes:

• name — the function name (atom)
• type — the function’s Pi type (used to find ADT-typed parameters)
• body — the function body (lambdas wrapping case expressions)
• adts — a map of ADT declarations (to identify which parameters can decrease)

The algorithm:

1. Extract parameters from the Pi type and strip lambdas from the body
2. Find all recursive calls (applications of the self-reference variable)
3. If there are no recursive calls, the function is trivially total
4. Otherwise, try each ADT-typed parameter as a candidate “decreasing argument”
5. A parameter decreases when the recursive call passes a pattern-bound variable from a case that scrutinizes that parameter
6. If any candidate works for ALL recursive calls, the function is total

Returns :total or {:not_total, reason}.

Accepted: Nat addition (decrease on first arg)

The classic example: add(n, m) recurses by pattern matching on n and passing the predecessor k (a structural subterm) in the recursive call. The second argument m is unchanged — only one parameter needs to decrease.

def add(n : Nat, m : Nat) : Nat do
  case n do
    zero -> m
    succ(k) -> succ(add(k, m))
  end
end

_ = {new_db, purge}

# Pi type: Nat -> Nat -> Nat (both omega multiplicity).
add_type = {:pi, :omega, {:data, :Nat, []}, {:pi, :omega, {:data, :Nat, []}, {:data, :Nat, []}}}

# Body as core term (de Bruijn indexed):
#   lam(n). lam(m). case n of
#     zero -> m
#     succ(k) -> succ(add(k, m))
#
# Under 2 lambdas: n=var(1), m=var(0), add=var(2)
# In succ branch (arity 1): k=var(0), m=var(1), n=var(2), add=var(3)
add_body =
  {:lam, :omega,
   {:lam, :omega,
    {:case, {:var, 1},
     [
       {:zero, 0, {:var, 0}},
       {:succ, 1, {:con, :Nat, :succ, [{:app, {:app, {:var, 3}, {:var, 0}}, {:var, 1}}]}}
     ]}}}

IO.inspect(Totality.check_totality(:add, add_type, add_body, adts), label: "add")

Accepted: list length (decrease on list arg)

length(xs) pattern matches on the list and passes the tail rest — a structural subterm of xs — in the recursive call. The cons constructor has arity 2 (head and tail), so rest is at de Bruijn index 0 in the branch body.

def length(xs : List(a)) : Nat do
  case xs do
    nil -> zero
    cons(_, rest) -> succ(length(rest))
  end
end

_ = {new_db, purge}

# Pi type: List(a) -> Nat
length_type = {:pi, :omega, {:data, :List, [{:var, 0}]}, {:data, :Nat, []}}

# Body:
#   lam(xs). case xs of
#     nil -> zero
#     cons(_, rest) -> succ(length(rest))
#
# Under 1 lambda: xs=var(0), length=var(1)
# In cons branch (arity 2): _=var(1), rest=var(0), xs=var(2), length=var(3)
length_body =
  {:lam, :omega,
   {:case, {:var, 0},
    [
      {nil, 0, {:con, :Nat, :zero, []}},
      {:cons, 2, {:con, :Nat, :succ, [{:app, {:var, 3}, {:var, 0}}]}}
    ]}}

IO.inspect(Totality.check_totality(:length, length_type, length_body, adts), label: "length")

Accepted: trivially total (no recursion)

A function with no recursive calls is trivially total — there is nothing to check. The identity function is the simplest example. Note that the parameter type here is Int (a builtin, not an ADT), which is fine since there is no recursion at all.

_ = {new_db, purge}

# def id(x : Int) : Int do x end
id_type = {:pi, :omega, {:builtin, :Int}, {:builtin, :Int}}
id_body = {:lam, :omega, {:var, 0}}

IO.inspect(Totality.check_totality(:id, id_type, id_body, adts), label: "id")

Rejected: loop (no decrease)

loop(n) calls itself with the same argument — no parameter decreases. The checker reports {:no_decreasing_arg, :loop, nil} because no candidate parameter passes the structural decrease test.

def loop(n : Nat) : Nat do loop(n) end

_ = {new_db, purge}

# def loop(n : Nat) : Nat do loop(n) end
# Under 1 lambda: n=var(0), loop=var(1)
loop_type = {:pi, :omega, {:data, :Nat, []}, {:data, :Nat, []}}
loop_body = {:lam, :omega, {:app, {:var, 1}, {:var, 0}}}

IO.inspect(Totality.check_totality(:loop, loop_type, loop_body, adts), label: "loop")

Rejected: bad (argument increases)

bad(n) wraps its argument in succ before recursing — the argument grows rather than shrinks. The recursive call’s argument is a constructor application, not a pattern-bound variable, so it cannot be a structural subterm.

def bad(n : Nat) : Nat do bad(succ(n)) end

_ = {new_db, purge}

# def bad(n : Nat) : Nat do bad(succ(n)) end
# Under 1 lambda: n=var(0), bad=var(1)
bad_type = {:pi, :omega, {:data, :Nat, []}, {:data, :Nat, []}}
bad_body = {:lam, :omega, {:app, {:var, 1}, {:con, :Nat, :succ, [{:var, 0}]}}}

IO.inspect(Totality.check_totality(:bad, bad_type, bad_body, adts), label: "bad")

Rejected: nested recursion f(f(x))

nested(n) passes a structural subterm k to the inner call, but the outer call receives nested(k) — an application, not a variable. The checker requires every recursive call’s decreasing argument to be a bare variable from a constructor pattern. Nested recursion like f(f(k)) is correctly rejected.

def nested(n : Nat) : Nat do
  case n do
    zero -> zero
    succ(k) -> nested(nested(k))
  end
end

_ = {new_db, purge}

# def nested(n : Nat) : Nat do
#   case n do zero -> zero; succ(k) -> nested(nested(k)) end
# end
# In succ branch (arity 1): k=var(0), n=var(1), nested=var(2)
# nested(nested(k)) = app(var(2), app(var(2), var(0)))
nested_type = {:pi, :omega, {:data, :Nat, []}, {:data, :Nat, []}}

nested_body =
  {:lam, :omega,
   {:case, {:var, 0},
    [
      {:zero, 0, {:con, :Nat, :zero, []}},
      {:succ, 1, {:app, {:var, 2}, {:app, {:var, 2}, {:var, 0}}}}
    ]}}

IO.inspect(Totality.check_totality(:nested, nested_type, nested_body, adts), label: "nested")

Full pipeline: @total function compiles and runs

The @total annotation integrates with the full Roux pipeline. When a function marked @total passes the structural recursion check, it compiles to a working BEAM module like any other definition. Here we define add as @total and call it at runtime.

_ = {adts}

db = new_db.()

Roux.Input.set(db, :source_text, "lib/total_add.hx", """
type Nat = zero | succ(Nat)

@total
def add(n : Nat, m : Nat) : Nat do
  case n do
    zero -> m
    succ(k) -> succ(add(k, m))
  end
end

def to_int(n : Nat) : Int do
  case n do
    zero -> 0
    succ(k) -> 1 + to_int(k)
  end
end
""")

{:ok, mod} = Roux.Runtime.query(db, :haruspex_compile, "lib/total_add.hx")

two = mod.succ(mod.succ(mod.zero()))
three = mod.succ(two)
result = mod.add(two, three)

IO.puts("add(2, 3) = #{mod.to_int(result)}")

purge.(mod)
:ok

Full pipeline: non-total rejected at check time

When @total is present but the function does not structurally decrease, the checker rejects it with an error. This happens at check time — the function never reaches codegen.

_ = {adts}

db = new_db.()

Roux.Input.set(db, :source_text, "lib/bad_total.hx", """
type Nat = zero | succ(Nat)

@total
def loop(n : Nat) : Nat do loop(n) end
""")

{:ok, _} = Roux.Runtime.query(db, :haruspex_parse, "lib/bad_total.hx")
result = Roux.Runtime.query(db, :haruspex_check, {"lib/bad_total.hx", :loop})

IO.inspect(result, label: "@total loop")

Non-@total functions skip the check

Without @total, the same non-terminating function passes type checking. This is by design — totality is opt-in. Haruspex is a practical language that allows general recursion by default; @total is for when you want a machine-checked termination guarantee.

_ = {adts}

db = new_db.()

Roux.Input.set(db, :source_text, "lib/no_total.hx", """
type Nat = zero | succ(Nat)

def loop(n : Nat) : Nat do loop(n) end
""")

{:ok, _} = Roux.Runtime.query(db, :haruspex_parse, "lib/no_total.hx")
result = Roux.Runtime.query(db, :haruspex_check, {"lib/no_total.hx", :loop})

IO.inspect(result, label: "loop without @total")

Summary

The @total annotation is fully integrated into the Roux pipeline. Totality checking runs after type checking and before codegen, rejecting non-structural recursion at compile time while leaving un-annotated functions unchecked.