agda2bend

Agda in, checked Bend 2 out.

agda2bend translates Agda modules, together with every module they import, into Bend 2. The output is kept only if the stock Bend checker accepts it. Whatever it rejects is dropped, along with everything that depends on it, and a ledger records each item and the reason it was dropped. Nothing is patched into the checker to make the output pass.

Source: github.com/hhefesto/agda2bend (MIT). It's a work in progress.

Why

Bend 2 is a functional language with dependent types. A Bend program can state a theorem in its type and prove it in its body, and bend --check-only verifies the proof. Agda has years of proofs written this way: the standard library, agda-categories, agda-unimath, agda-algebras and PLFA. Bend 2 is new, and little Bend of this kind exists yet. agda2bend turns the Agda proofs into Bend that checks.

That output is training data for ana, a small model that writes Bend. Each checked definition is one example of correct Bend, and the Bend checker is the judge.

An example

Symmetry of equality, in Agda:

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

and what agda2bend writes:

def sym(-A: Type, -x: A, -y: A, x_6: {x == y : A}) -> {y == x : A}:
  %x_6 : {_ == x : A}
  {==}

• Agda's implicit arguments {A} {x y} become erased parameters (-A): they exist only for the checker, not at run time.
• x ≡ y is Bend's equality type {x == y : A}, and refl is {==}.
• Agda matches on refl. Bend can't match on an equation, so the match becomes a rewrite: %x_6 : {_ == x : A} rewrites the goal along x_6, and the hole _ marks where y stands. After that the goal is {x == x : A}, and {==} proves it.

A proof by induction, map id ≡ id on lists:

map-id : {A : Set} (xs : List A) → map (λ a → a) xs ≡ xs
map-id []       = refl
map-id (x ∷ xs) = cong (x ∷_) (map-id xs)

def map_id(-A: Type, xs: List_<A>) -> {map(~A, ~A, ~a => a, xs) == xs : List_<A>}:
  match xs:
    case List_.lb_rb{}:
      {==}
    case List_.cons{x_1, xs_2}:
      cong(List_<A>, List_<A>, eta1 => List_.cons{x_1, eta1}, map(~A, ~A, ~a => a, xs_2), xs_2, map_id(A, xs_2))

Bend has no implicit arguments, so every argument Agda inferred is written out. Names get rewritten for Bend: [] becomes lb_rb, _∷_ becomes cons, and map-id becomes map_id. ~A passes A to a template parameter.

The functor form of the Yoneda lemma's two maps:

Yo : (F : Set → Set) (A : Set) → Set₁
Yo F A = {B : Set} → (A → B) → F B

fto : {F : Set → Set} {A : Set} → Yo F A → F A
fto α = α (λ a → a)

def Yo(-F: @-x:Type -> Type, -A: Type) -> Type:
  @-B:Type -> (A -> B) -> F(B)

def fto(-F: @-x:Type -> Type, -A: Type, x: Yo(F, A)) -> F(A):
  x(A, a => a)

@x:T -> U is Bend's dependent function type, and @-x erases the binder. Universe levels aren't kept, so Agda's Set and Set₁ both become Type. In fto, the {B} that Agda inferred is passed explicitly as A.

How it works

1. Agda elaborates. agda-export is an Agda 2.8.0 backend, the only part not written in Bend. It writes every definition in the import closure as an S-expression of Agda's internal syntax: types, clauses, compiled case trees, records, data types and constructors. It decides nothing.
2. Everything after that is written in Bend: a streaming S-expression reader, a parser of Agda's syntax, a fold from Agda into a Bend syntax tree, then Bend-side passes (names, ordering, a quantity pass that decides what's erased, copied or live, and universe levels as quantities), and a printer.
3. The gate. The pinned bend checks each module. A failing item is dropped with its dependents, and OUT/ledger.tsv records every item's fate and reason. agda2bend report ranks the reasons by how many items each blocks, so work on the translator goes where it unblocks the most.

Some of the translation choices:

Where it stands

As of 2026-10-29, the runs over the standard library, agda-unimath, agda-categories, agda-algebras and PLFA have produced 10,911 distinct definitions that check: 6.45 MB of Bend. By source: standard library 7,079, agda-unimath 1,501, agda-categories 1,101, agda-algebras 714, PLFA 430.

On the import cone of agda-categories' Categories.Yoneda (121 modules, 2,527 items), 2,256 items check (run of 2026-10-25). The Yoneda module itself doesn't check yet: its 12 items depend on Setoids, which still fails. A smaller Yoneda file written as a test does better. Its identity-type version and its functor version (the Yo example above) check in full. Its categorical version checks only in part: the unit laws and the two round trips are dropped.

Things that don't translate yet, or not always:

• eta for records and for ⊤: stock Bend has no record eta, and some proofs rely on it;
• nested constructor patterns on indexed families, where an inner pattern's indices come from the outer one's fields (<⇒<ᵇ in Data.Nat.Properties; 122 definitions depend on it);
• a polymorphic value used twice (Bend copies only Data);
• records over a carrier of an arbitrary kind (expected Data observed Kind(a));
• an erased binder used live, when the erasure guess is wrong;
• cubical Agda (1lab, cubical) isn't attempted.

Use

# translate a file and the modules it imports; out/src holds the Bend that checks
nix run github:hhefesto/agda2bend -- translate Foo.agda out

# translate an existing export (agda-export's --export-dir): a module's cone, or all of it
nix run github:hhefesto/agda2bend -- emit EXPORT_DIR out Categories.Yoneda

# the ledger summed up: the reasons, ranked by the items they block
nix run github:hhefesto/agda2bend -- report out

translate runs from the root of the file's Agda library. By default, agda-export resolves the standard library and agda-categories. Set AGDA_DIR to use other libraries.

agda2bend is MIT-licensed. Agda, the Agda standard library, agda-categories, agda-unimath, agda-algebras, PLFA and Bend belong to their authors, under their own licenses.