nfx (GitHub - vic/nfx: Nix Algebraic Effects System with Handlers) is a port of my fx.rs effects system (rust) which in turn was an evolution of my first fx.go go implementation.
This port was vibecoded with my other repos as base just because I had to use some tokens.
This post made me revisit something I’d shelved. Last summer I built an algebraic effects system in Nix (free monad encoding, handler composition, dependent contracts, the works) but the handler loop was direct recursion. Anything beyond a few modules just blew the C++ stack. I figured stack depth was a death sentence for the whole approach and gave up on it.
Looking at it fresh, turns out builtins.genericClosure works as a trampoline. It’s the only iterative primitive Nix has, and if you force handler state through deepSeq in the key field it breaks thunk accumulation. O(1) stack depth at 1M+ operations. Wrote it up here: Trampolining Nix with genericClosure
I come from Common Lisp, so the conditions/restarts module stood out. Storing restart closures in the context and invoking by name is basically restart-case. I did something similar in nix-effects, different encoding but same idea. You can’t get the interactive restart menu without something like IFD, but for configuration where restarts are known ahead of time, that’s fine.
Anyway, have you run into stack depth on larger computations, or does the lazy context-passing just sidestep it?
@vic maybe a silly question given you stated your motivation, so i guess i’m open to responses from others as well, but are there any particular use-cases you had in mind for this?
have not tried it for anything large, not even small, :D. yeah having a production grade effects system requires not blowing up the recursion stack, I’ve had no time to explore nfx further since that weekend. But I do hope to find some time to read your linked resources, thanks for sharing.
Nothing useful yet, no silly questions. I’ve been using effect systems at work for like 7 years now (Scala ecosystem mainly). And I had those Go and Rust prototypes and was thinking about the big mess (for me) that is the overlays system, so I was curious thinking if it’d be possible to use something like a reader effect, that could say “I need a c compiler” and that c-compiler be provided by an effect handler. So basically my curiosity was about having dependency injection In nix via effect handlers (providing environment) instead of all derivations reading from a huge attrset (globally merged as overlays do) because we could have scoped overrides with effect handlers. Anyways, I have very limited time to explore things, but that was basically why I was trying to explore algebraic effects in nix.
I spent more time in the source. func + rw.local handles scoped overrides, and nesting works, that is to say, two nested rw.local calls compose the way you’d expect.
Perhaps not surprising to you, but conditions maps to the dependency injection case you described really well. To see why, consider that overlays can override a package, but they can’t express “I need a C compiler, and here’s what to do if there isn’t one.” However, conditions can:
# The derivation declares what it needs and names a fallback strategy
needsCC = conditions.withRestart "use-default" (cc: pure cc)
(mapM (env:
if env ? cc then pure env.cc
else conditions.signal { type = "missing-dep"; name = "cc"; }
) state.get);
# This environment has linker but no cc, so the signal fires.
# The handler invokes the "use-default" restart with gcc.
provide { linker = ld; } (
conditions.handle "missing-dep" (_:
conditions.invokeRestart "use-default" gcc
) needsCC
)
The derivation defines the restart: “I can accept a default compiler.” The handler picks which restart to invoke and with what value. So the derivation and the package set negotiate resolution, rather than the package silently receiving whatever the overlay provides. I tested both paths against the repo: provide { cc = clang; linker = ld; } reads clang directly, provide { linker = ld; } fires the signal and the handler supplies gcc. Composes with rw.local for scoped overrides too.
The limitation I see is callPackage. It injects from the global fixpoint, so a package can’t say “give me whatever cc is in scope.” Either callPackage wraps its result in an effect, or the package definition itself becomes effectful. Have you thought about where that boundary sits?
yes, even when Nix language is functional, I feel like most idoms we see on the wild it are not. I guess people using lisp on guix get more functional patterns that what nix community does. I believe there’s a lot of potential in using functional idoms like effects in a language like Nix, given it is lazy. If we did have effect-scoped packages that would be an alternative evaluation path (as you mention current callPackage uses the global fixpoint). Yes exactly that was I wanted this particular effect system to have conditions (my previous rust and go prototypes did not have condition system). Anyways, it is cool we have things to explore around Nix. Another idea I was having about using an effect system is that effects are basically program as data (again, just because we are not using lisp) and if you have that, you could describe the dependencies some code has, without executing it. I’ve seen some people explore this on other threads but I believe with a patched nix interpreter maybe.
Another thing nfx has is “logic programming”, basically branch exploration (it lacks a bit of code to have unification like you’d have on uKanren like logic languages). You could have logic-variable-holes on some derivations and have it filled by the unification system. Again, things to explore once having a job is not a concern.
Also effect handlers could help with “security” constraints, like I need not only a C compiler, but one that provides such and such features or has some others turned off, because of security constraints of my package. And we could describe these requirements via part of the effect row and satisfy them via handlers.
I tried the security constraints idea against the repo. A package signals what it needs, the signal carries the full constraint description, and the handler picks a compiler based on that:
# Compiler records with some kind of security feature metadata
gcc-hardened = {
name = "gcc-hardened";
features = { stackProtector = true; fortifySource = true; fips = false; };
};
gcc-fips = {
name = "gcc-fips";
features = { stackProtector = true; fortifySource = true; fips = true; };
};
# Does every required feature match what the compiler provides?
checkConstraints = required: provided:
builtins.all (name:
provided.${name} or false == required.${name}
) (builtins.attrNames required);
# The package declares its security requirements.
# If the compiler in scope satisfies them, use it.
# Otherwise, signal with the full constraint description.
requireCC = constraints:
conditions.withRestart "use-compiler" (cc: pure cc)
(mapM (env:
let cc = env.cc or null;
in if cc != null && checkConstraints constraints (cc.features or {})
then pure cc
else conditions.signal {
type = "security-constraint";
inherit constraints;
provided = if cc != null then cc.features or {} else {};
}
) state.get);
The handler reads the constraint from the signal and picks the right compiler:
# Handler inspects what was required and chooses accordingly
smartHandler = cond:
let needed = cond.constraints;
in conditions.invokeRestart "use-compiler"
(if needed.fips or false then gcc-fips else gcc-hardened);
# No compiler in scope. Signal fires, handler reads fips = true, provides gcc-fips.
runFx (provide {} (
conditions.handle "security-constraint" smartHandler
(requireCC { fips = true; })
))
# => gcc-fips
# Same handler, different requirement. Reads stackProtector + fortifySource, provides gcc-hardened.
runFx (provide {} (
conditions.handle "security-constraint" smartHandler
(requireCC { stackProtector = true; fortifySource = true; })
))
# => gcc-hardened
In my mind, the condition is the effect row here: it describes the security requirement as data, the handler satisfies it. Same negotiation as the DI case, but now the package and handler are negotiating security properties.
stream.flatMap already does constraint search over a compiler pool. Singleton streams per compiler, flatMap with a predicate to filter, done to drop non-matches. Stack two filters and the intersection falls out. observeAll enumerates solutions, observe takes the first. That seems to be the kind of “fill logic-variable-holes via search” you described, i.e., you say what you need and search the space rather than construct through it.
Then there’s the encoding question. In context-passing, requireCC is pending { ability = <lambda> }. You can run it, but you can’t see what constraints it will signal until you do. A freer encoding gives you Request "cc" { fips = true; } (cc -> ...), pattern-matchable without execution. The dependency description is the program, readable before any handler runs. Both encodings express the security constraints fine. The difference is whether you can audit statically (freer) or only dynamically (context-passing). If you want it to be able to show you every security requirement in this package set without building anything, then freer becomes a necessity.
I do keep coming back to CL the more I think about this. callPackage is basically dynamic binding without the language knowing about it. CL special variables have dynamic extent, closer to what rw.local does. Guix inherits that from Scheme. It seems to me that Nix reinvented the pattern without the tradition. We then have the same underyling question: how much does the language let you see about what a computation will do before you run it.
Lots of stuff to explore 