Fixpoint in NixOS
It took me a while to finally get how fixpoint works in NixOS1. I’ve worked in a couple functional languages before Nix (Elixir, some Erlang), but the concept of fixpoint has never come up. Maybe it’s more common in Haskell-land? Not sure.
In any case, in NixOS the concept comes up with regards to the module system, and it can be a bit inscrutable. You can totally /use/ the modulue system without ever fully understanding what a fixpoint is, and how it applies to the module system specifically – in fact, that’s exactly what I did.. until now!
A fixpoint is a value x that satisfies this self-referential equation: x = f(x).
For example, given this function:
f = self: {
a = 1;
b = self.a + 1;
c = self.b + 10;
}
the fixpoint for f is the attrset { a = 1; b = 2; c = 12; }, because it’s the only value that, when passed to f, sastisfies x = f(x). So far so good. But how is this practically useful, with regards to the module system?
As you might know, one of the observable properties of the module system is that it merges all of the different option definitions into one final configuration.
If modules were static attributes sets, we could obtain the resulting system config by simply merging them:
m1 = {
services.nginx.enable = true;
networking.firewall.allowedTCPPorts = [ 80 ];
}
m2 = {
services.prometheus.exporters.nginx.enable = true;
networking.firewall.allowedTCPPorts = [ 22 ];
}
which would evaluate to something like:
config = {
services.nginx.enable = true;
services.prometheus.exporters.nginx.enable = true;
networking.firewall.allowedTCPPorts = [ 22 80 ];
}
This process could simply be expressed as y = f(x), with f being some appropriate but dumb merge function, x the list of plain-attrset modules, and y the resulting config. So why do we need the fixpoint specifically?
The reason is that typically, modules are not attrsets, but functions that depend on the final config:
m1 = { ... }: {
services.nginx.enable = true;
networking.firewall.allowedTCPPorts = [ 80 ];
}
m2 = { config, ... }: {
services.prometheus.exporters.nginx.enable = lib.mkIf config.services.nginx.enable;
networking.firewall.allowedTCPPorts = [ 22 ];
}
Here, m2 depends on the result of the merge (config), which m2 is itself helping to produce. So our naive y = f(x) could be rewritten as y = f(x(y))2.
If we rename F = f ∘ x3, we get y = F(y) – that’s our fixpoint.
How this works in a lazy langauge like Nix is that the evaluation procedes by-dependency: each value of the final configuration is evaluated only when something depends on it.
In our example, services.prometheus.exporters.nginx.enable depends on config.services.nginx.enable, which depends on nothing else. The configuration is evaluated piece-meal, following the chain of dependencies, all the way to the end.
This allows cutting the gordian knot that calculating the fixpoint would apparently be: each option is resolved directly from the option it depends on. The only cases when this doesn’t work is when there’s an actual infinite recursion, eg if an option depends on itself. For example, foo.val = config.foo.val + 1 would infinitely recurse.
The fact that some modules depends on the result of the final merge, of which they’re also a part, is what makes this problem amenable to be expressed with the concept of a fixpoint.