bend-emit

Turn a pure Bend core into a typed ES module.

Write your pure functions and proofs in Bend, then call the generated functions from TypeScript. bend-emit generates named exports and TypeScript declarations, and applies conservative runtime optimizations to Bend's JavaScript output.

Quick Start

Install Bend 2.0.39 and Bun, with both bend and bun on PATH. The commands below also require Node.js and npm for npx. Installing this npm package does not install Bend or Bun.

Save this as core.bend:

import Base

def add(a: Nat, b: Nat) -> Nat:
  (a + b : Nat)

Build it:

npx --yes --package [email protected] -- bend-emit core.bend dist

Then import the generated module:

import { add } from "./dist/core.mjs";

add(2, 3); // 5; the generated signature uses number

For a project-local installation:

npm install --save-dev --save-exact [email protected]
npx bend-emit core.bend dist

Bun users can install and run the same package:

bun add --dev --exact [email protected]
bunx bend-emit core.bend dist

Generated Files

bend-emit <core.bend> <outdir>

For core.bend, the command writes:

• core.mjs: an ES module with named exports and a default export.
• core.d.mts: declarations for the supported public definitions and data types.

The .mjs extension makes the module load as ESM in both CommonJS and ESM packages. The matching .d.mts extension lets TypeScript resolve its types.

Commit or distribute both files with your application or library. Consumers of these generated files do not need Bend, Bun, or bend-emit at runtime. They need a JavaScript runtime with ES-module support.

Why Bend

Bend lets you state laws about pure functions and prove them for all inputs covered by those laws. This is useful for parsers, validators, codecs, and other pure logic with precise requirements.

bend-emit uses Bend's JavaScript backend rather than a second implementation of your core. Your TypeScript application calls the generated functions, with declarations derived from the Bend source.

The generated JavaScript is not independently proved. Its behavior also depends on Bend's backend and bend-emit's transformations. Tests compare transformed output with Bend's output; they do not replace a proof of the compiler or this tool.

For a worked example, see bend-schema, which builds a typed JavaScript interface to a schema checker written in Bend.

How It Works

bend-emit runs bend <core.bend> -o <out>.mjs, then processes the emitted module and reads the source's data declarations and definition headers.

Bend exports a default object. bend-emit adds named exports for its definitions while retaining the default export's interface. It checks that the source names and compiled export names agree before writing the output.

Supported types follow Bend's runtime representation:

| Bend | JavaScript / TypeScript | | --- | --- | | Nat | number: a whole number from 0 to 2^53 | | U32 | number | | Bool | boolean | | String | string | | Char | string containing one code point | | Map<A> | BendMap<A>: a tagged tree with MTip, MLeaf, and MNode |

The generated declaration preamble defines BendList, BendMap, BendMaybe, BendResult, and BendEither using the runtime's tagged constructors. A BendMap is not a native JavaScript Map; its MNode.pos field is a number, like Bend's Nat representation. The map's structural invariants are those of the Bend Map implementation; bend-emit only describes its runtime shape.

Runtime Transformations

The generated module is not byte-for-byte identical to Bend's output. bend-emit applies these transformations:

• Lazy selectors: bend evaluates call arguments eagerly, so pick(c, f(x), g(y)) runs both f and g. A def whose emitted body is exactly if (b) return p; else return q over its own parameters (in Bend: a match on one Bool parameter whose arms each return a parameter unchanged; -A and +/- marks are irrelevant) is a selector, wherever it is defined in the bundled core, imported or not. A call that is all of a return becomes if (b) { return X; } else { return Y; }, so only the chosen argument runs and a self-call stays at the end of its branch for the loop pass below. Elsewhere the call becomes (b ? X : Y), unless X or Y call the enclosing def (that call stays eager). The selector def stays exported.
• Recursive list traversal: turn recursion on the tail of a list into a loop. In a return expression with self-calls, the self-call evaluated last (the "hole") is replaced by a loop step: what is evaluated before it is evaluated first, in the same order; what follows it is pushed on a per-call stack as a closure; the parameters are rebound to the hole's arguments. Each other return folds the stack. This covers Con{head: f(x), tail: f(t)}, and(f(h), f(t)), n + f(t), pick(c, v, f(t)) and a self-call bound in a const just before the return, also inside bend's own for (;;) loops. It reads shapes only and knows no names. Self-calls other than the hole (the head, a nested child) stay real calls, so nesting depth is still bounded by the stack. A def whose self-call is under ||, && or ?:, is not at the end of its branch, or uses its own name as a value stays unchanged and produces a still recursive: <name> (<why>) diagnostic.
• Zero-field constructors: reuse singleton values rather than allocating a new object for each occurrence.
• String comparison: replace Base's String.order.go, which every String.eq, String.order and String.is_* calls, with a native loop that returns the same Cmp: by Char code, then the shorter string first. bend's own version slices both strings and allocates a Cmp at every character. The replacement happens only when the emitted def is exactly the text this bend version produces; otherwise the def stays as bend wrote it and produces a not made native: <name> (<why>) diagnostic.
• String traversal: replace eligible string-head/string-tail traversal with an index into the original string. Each step moves by one Char, as bend's own does: a surrogate pair or a packed non-scalar Char is one step. Uses outside the recognized shapes remain unchanged and produce a string still sliced: ... diagnostic.

These passes recognize specific output shapes. They do not guarantee that all recursion becomes stack-safe or that every core uses less memory. Review the diagnostics and measure your own workload.

Laws and Facts Files

A file that holds laws and lemmas, such as a LAWS.bend with reference definitions beside its laws, can be built directly. bend-emit builds a copy of the file, and of every .bend file it imports, without:

• every law;
• every def whose header line contains == (a lemma), and every def named like a law (its proof);
• every def or type that names a skipped one, directly or through an import alias such as KF.lemma;
• every import bend-mathlib... line.

What remains is emitted as usual. A lemma whose == is not on the def's header line is not recognized. A file with nothing to skip is built from its own path, exactly as before.

In such a build, a def with no TypeScript encoding (for example one whose type is a Base type such as Cmp) stays in the .mjs and is left out of the .d.mts, with one warning line naming it. In an ordinary core it is still an error.

Undeclared Definitions

Some definitions have no generated TypeScript signature:

• Definitions returning IO(...).
• Definitions with template parameters such as ~f.
• Definitions returning Data or Type, using computed types, or carrying erased parameters.

Where Bend includes such a definition in its emitted module, bend-emit does not remove it. The absence of a declaration is not a supported typed API. Template definitions are not exported by Bend's ES-module target.

Toolchain Requirements

The build tool requires Bun and exactly Bend 2.0.39, the version recorded in BEND_VERSION. Another Bend version is rejected before compilation.

The emitter reads and transforms compiler output, so a different compiler version could change the shapes it relies on. Pin bend-emit and use the Bend version required by that release.

Development

From a checkout, install the development dependencies and run the gate:

bun install --frozen-lockfile
sh test.sh

The gate builds fixture cores, checks runtime values and declarations, compares optimized output with Bend's output, and tests refusal paths. It also typechecks valid and invalid TypeScript calls and loads a generated module with Node in both CommonJS and ESM packages.

License

MIT. See LICENSE.