# Building Zen - an actor-based Nix module system - my tacosprint project, by [vic](https://github.com/vic) ([@oeiuwq](https://x.com/oeiuwq)) Zen is the project I've been working on during [tacosprint](https://tacosprint.org). It is an exploration built on my previous months work on Nix effectful libraries. Zen's goal is not to replace nixpkgs modules, but my way to explore other ways of expressing and resolving configurations using already proven functional idioms from languages like Scala/Haskell. > TL;DR — Zen modules are actors, they communicate via message exchange (built on an effectful-streams substrate) are stateful and can change their behaviour depending on messages, like exposing different set of configurable options or different strategies for merging values, error-handling or cross-actor discovery and communication. > > Benchmarks: `nix-shell --run 'just bench'` > Demos: `nix-shell --run 'just demo'` Zen is very opinionated about what a module system provides; For me, such a system must have: - A way to merge multiple sources value contributions for the same option. - A way to validate merged values (types). - A way for configuration values to depend on other values. In my opinion, other things like file-loading `imports = [ ... ]` are not a concern of a module system and should not be part it. Zen is my take at `nixpkgs`-alternative module systems, see also [`adios`](https://github.com/adisbladis/adios) and [`hola`](https://github.com/sini/hola) (WIP by [@sini](https://github.com/sini)) for other explorations. Zen is very lightweight, all of its power derives from the underlying composable libraries that make it possible to provide capabilities that `nixpkgs`'s `lib.evalModules` is **structurally incapable** of: - **Real Types**. In nixpkgs we have value-checks, not proper types. The underlying MLTT substrate features dependent/refined types, and can express types things that nixpkgs cannot, like `int -> string` where `lib.functionTo` cannot type its domain. The [`nix-effects`](https://github.com/kleisli-io/nix-effects) foundational library provides not only effectful monads, but also streams and type system. - **Resolve a conflict, then prove the result is valid.** Two modules both claim `port`. A condition handler negotiates a winner. Then a **dependent type** proves the negotiated configuration is internally consistent all in one evaluation. `nixpkgs` throws `conflicting definition values` and dies on the spot. > Demo: `just demo mesh` - **Modules that find each other without knowing each other.** A client asks a broker for "whoever provides capability X", gets wired to a provider, and neither module names the other. Flip a provider's priority and the client silently re-wires, zero edits to either side. Modules no longer query fixed-option-paths but they exchange messages. > Demo: `just demo discovery` - **Swap the failure policy by swapping one handler.** The same config runs fail-loud in CI (collect **every** error, located) and degrade-gracefully in dev (fall back, keep going). You change the **handler**, never the config. Better error reporting, each error is annotated and becomes a left (Either monad error) value. Other actors can provide strategies for solving errors, with Common-Lisp style restarts. > Demo: `just demo policy` - **Errors, cycles, and conflicts are inspectable data, not crashes.** A bad option becomes a located `{ path, why, got }` value, and the rest of the config still settles around it. A circular reference becomes a located `{ why = "cycle"; cycle = [...] }` report instead of `nixpkgs`'s unlocated `infinite recursion encountered`. > Demo: `just demo blame` / `partial` / `cycle` `zen` is a **~100-line kernel** over four small, independently useful libraries. `just demo` runs all **14** acts side-by-side — `nixpkgs ✗` next to `zen ✓` — and `just demo <name>` runs a single act. Everything below is one of those acts. --- ## The substrate: four github.com/denful libraries > TL;DR. **the four libraries are useful entirely on their own.** `bend` is a lens library, `ned` is a stream library, `fx` is an effects-and-types library, `dnzl` is an actor library — none of them knows what a "configuration" is. `zen` is the ~100-line lib that **composes** them yielding a module system. Even when benchmarks measure 20x speed of nixpkgs, the interesting object is not speed. It is the substrate underneath it and new configuration patterns that it makes possible. `zen` invents almost nothing. Each capability above is really a capability of one of four libraries; `zen` is the thin layer that wires them together. ### composable lenses ([denful/bend](https://github.com/denful/bend)) A `bend` lens has type `input → Either value error`: it transforms the data, or explains structurally why it couldn't. In `zen`, both **merge** (N module contributions: one value) and **validation** (that value against a type) are `Either`, returning `bend` lenses. A verification is not a `true`/`false` predicate it is a lens that returns `right typedValue` or `left { why, got, path }`. A validation failure is a located record you or other actors can read, not an exception that unwinds the stack. This is ["parse, don't validate"](https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/) principle taken all the way down. ### cyclic streams ([denful/ned](https://github.com/denful/ned)) `ned` is a Cycle.js inspired stream library: you describe a system as `(sources: attrsOf stream) -> (sinks: attrsOf stream)`, and `ned` ties the knot to find the fixpoint. That is exactly the shape a module system needs, modules **read** the merged config (`sources.config`) while **defining** it (their sinks). In `nixpkgs` the fixpoint is implicit, a property of the evaluation engine. In `zen` it is an explicit, inspectable `ned` cycle. `ned` also provides a relational primitive, `withPeers`, which groups a stream so each element can see its peers — the foundation for any settlement where elements must coordinate (leader election, port allocation, discovery). ### algebraic effects + dependent types ([kleisli-io/nix-effects](https://github.com/kleisli-io/nix-effects)) `nix-effects` brings three things to Nix that Nix has no business having. **Algebraic effect handlers**: evaluation runs **inside** an effect world, so what happens on an error is a handler decision, not a hard-coded `throw`. **Common-Lisp-style conditions and restarts**: a problem can be signalled, and a handler can pick a restart that resumes computation from the signal site. And **real Martin-Löf type theory**, dependent records, `Vector n` value-indexed types, dependent functions, and refined types. Because evaluation stays in the effect world, errors are data, **policies are handlers**, and **types are proofs** all at once. ### actors ([denful/dnzl](https://github.com/denful/dnzl)) `dnzl` is a small actor library: `send`, `become`, `reply`, with an per-actor inbox. An actor is stateful behaviour that evolves per message it can `become` a new handler in response to what it receives and references are passed in-band, not held as global pointers. This is what lets a `zen` module be more than a constant: a module can be an actor that accumulates state across the message stream it sees. `dnzl` has no `spawn` and no supervision tree it is the actor **calculus** (behaviour-over-messages), it has no Erlang-grade fault tolerance nor network access. (`dnzl` re-exports `ned`, `fx`, and `bend`, so depending on `zen` pulls the whole substrate.) --- ## How zen composes them Each library owns one axis of the design: - **`bend`** owns **N->1 contributions and types**: merge and validation are lenses, failures are located data. - **`ned`** owns **the fixpoint**: modules read the merged config because `ned` ties the cycle; an option's value is a stream, and `withPeers` lets streams settle relationally. - **`fx`** owns **the effect world**: keeping evaluation inside it is what makes errors data, handlers policy, and dependent types proofs rather than a separate verification pass. - **`dnzl`** owns **modules-as-actors**: a module's behaviour can evolve over the messages it sees. Every capability is one specific pair of libraries clicking together. ### Errors, cycles, and conflicts as data — *`bend` + `ned`* A failing option is a `bend` `left`: `{ path, why, got }`. Because failures are values, `zen.run` **accumulates** them and every bad option in the set, each located, instead of aborting on the first (`just demo blame`), and the **valid** options still settle around the broken one (`just demo partial`). Cycles are caught by a static **Kahn topological sort** a `ned` pre-pass over the dependency graph that runs **before any value is forced** so a genuine circular reference comes back as `{ why = "cycle"; cycle = [ "a" "b" ]; path = "a" }` instead of an unlocated engine death (`just demo cycle`). Contrast: `nixpkgs` surfaces fault #1 and never reaches fault #2, and a cycle is `infinite recursion encountered` with no path at all. ### Recover and re-policy *`nix-effects`' conditions/restarts* When two modules conflict, the merge step does not fail it **signals** a condition (a `"negotiating"` value), and `zen.run` invokes a handler that picks a **restart**, which resumes evaluation from the signal site (`just demo recover`). Because the per-option handler is a seam in the kernel, you keep the config fixed and **swap the handler** to change the whole system's failure posture: `zen.resolve.reject` to collect every conflict for CI, a fall-back resolver to degrade gracefully in dev (`just demo policy`). The policy lives outside the config, where it belongs. ### Dependent types, in your config *`fx` MLTT through `zen`'s whole-config `check`* `zen.run` takes an optional `check`: a `bend` lens applied to the **fully merged** config, and that lens can carry either normal nixpkgs' lib.types or `fx`'s real MLTT. So a field's **type can depend on another field's value**, a record whose `data` must be a `Vector` whose length is the value of its own `len` field (`just demo deptype`, `just demo deprecord`). You can declare an option as a domain-checked function whose return type is computed from the input value (`just demo pitype`). You can attach **refinement witnesses** that prove a value satisfies a predicate (`just demo refined`), and express **located cross-field invariants** that blame the exact field that broke the relationship (`just demo crossfield`). ### Discovery. *`dnzl` actors + `ned` `withPeers`* A broker is a `ned` `withPeers` settlement over a stream of capability **registrations**: providers announce "I offer X at priority P", the client requests "whoever offers X", and `withPeers` (the same relational-grouping primitive that does leader election) matches them. The modules are `dnzl` actors; neither holds a reference to the other. Re-prioritise a provider and the match flips with no edit to the client (`just demo discovery`). ### Mesh. *`nix-effects` restarts + dependent types, fused in one `zen.run`* the **restart** machinery negotiates the conflicting value, then the dependent-type `check` proves the negotiated configuration is internally consistent. negotiate, then prove, in one `zen.run` (`just demo mesh`). One pass produces both a resolution and a proof of its validity. `nixpkgs` produces neither; it throws producing a hard to read stack trace. --- ## Try it Clone the `https://github.com/denful/zen` and run: ```sh nix-shell # enters shell.nix env just bench # simplified benchmarks on nixpkgs just demo # all 14 demos just demo mesh # negotiate a conflict, then prove the result just demo discovery # modules that find each other by capability just demo policy # swap the failure policy by swapping a handler just bench ```