Instruction file imported from tiansivive/yap (.cursor/rules/coding-style.mdc). Copyright stays with the author.

Yap coding style

General

• Prefer immutable code
• Prefer declarative over imperative
• Prefer recursion over imperative looping
• Prefer simple, linear effect flow via generator delegation (yield*) over explicit capability rows (src/utils/effects/, src/elaboration/shared/effects.ts)
• Avoid long fp-ts pipelines — they make debugging harder
• Prefer function composition to interstitial variables that add no semantic value
• Prefer iterators and built-in HOFs (map, filter, reduce) over manual loops
• Avoid unnecessary callbacks: Array.map(doStuff) not Array.map(v => doStuff(v))

Naming and structure

• Namespace-based APIs — prefer Category.action over actionCategory. Encode functionality in namespaces (objects with methods/fields), not in function names. Extensible and discoverable.
• One-word names — multi-word names often indicate a function does too much; refactor
• One-letter vars OK in ML style: Array.map(x => ...), const [x, ...xs] = [...]
• KISS and DRY — small functions compose
• Avoid bloated code — strive for minimalism, avoid cryptic cleverness

ts-pattern

• Prefer match with guards over if/else chains and ternaries for multi-way dispatch
• Flatten cases into separate .with clauses; use guards (second arg) rather than nesting conditionals
• Match on the discriminant (e.g. node.type, tuple of values) so ts-pattern narrows types
• Use .otherwise for fallthrough
• See .cursor/rules/pattern-matching.mdc for pattern objects

Elaboration effects

• The freer runtime is canonical — V1 and the fixed V2.Do/RWSE runtime are legacy compatibility surfaces, not the live elaboration architecture
• Elaboration programs yield only the capabilities they need; compose nested programs with yield*
• Install complete handler sets at true boundaries. Inside an active run, use Eff.with for private/scoped effects and forward the remaining row; do not start a nested run that forks ambient state
• The metacontext registry is separate from lexical EB.Context; do not recreate ctx.metas, ctx.zonker, or writer-to-reader synchronization
• NbE owns its callstack and hides it behind public normalization entries; callstack actions do not belong in the elaboration row
• Inference: dispatch in src/elaboration/elaborate.ts + src/elaboration/inference/* (per-construct handlers)
• Checking: src/elaboration/check.ts (dispatches on [term, type])

Lint contract

• pnpm lint stays green — pre-existing debt is baselined in eslint-suppressions.json; new violations fail. Fix suppressed ones opportunistically, then pnpm eslint . --prune-suppressions.
• _-prefix declares a binding intentionally unused (params, destructured elements, locals kept for documentation). Unprefixed unused bindings are errors — treat them as rot or bug symptoms.
• Sanctioned mutable cores — fresh-name supplies, effect interpreters that own handler state, the independent solver-v2 driver (verification/solver/v2/core.ts), and the NbE CEK driver (evaluation.v2.ts) are deliberately imperative and carry scoped lint carve-outs. The evaluator loop is intentional architecture; machine state belongs to the private callstack handler. Don't cite these cores as precedent for mutation elsewhere.

Comments

• Avoid unneeded comments — code should be self-documenting
• Use types to document intent
• Comments explain "why", not "what"
• Brief and to the point