Module Structure

How fixed points, the nixpkgs module system, and dendrites fit together to structure this configuration.

fixed point combinator

lambda calculus

Lambda calculus is a field of mathematics that is used to express computation and formal logic through only using defining statements each relative to a variable and then binding values to those variables through substitution.

For illustration think of the statement λx. x + 1. What this statement says is given a lambda function that has a variable of x; take whatever value is supplied to x and add 1 to it yielding the result. While technically this is not valid lambda calculus because it utilizes mathematical concepts not native to that field such as addition and the idea of numbers it illustrates the concept on how to read a lambda calculus expression.

higher order functions

We can do more complex things than just apply numbers to statements to yield other numbers. Think of these two functions:

λa. λb. a
λa. λb. b

What these statements describe is a process where a value is bound to the parameter a. From there the bodies of the statements yield a new statement that has a value b that can be bound.

From there after binding the value b the method will then yield either the value bound to a or the value bound to b. If we chose the first method then the yielded value will be a, but if we chose the second method then the yielded value will be b.

If we want to give names to these functions we could call them something like first and second:

first → λa. λb. a
second → λa. λb. b

self referential values

This is all very useful for defining a process with a defined amount of steps, but sometimes we need something more complex than a nice list of actions to take.

For this we can create methods that provide something called a fixed point. A fixed point is a value that is defined in relation to itself instead of based on an external property.

Take the method Y

Y → λf. (λx. f(x x))(λx. f(x x))

Moving out of the realm of lambda calculus and into human readable labels we can do some substitution to figure out what this method does.

Y(g) = (λx. g(x x))(λx. g(x x))
    := g((λx. g(x x)) (λx. g(x x)))
    := g(Y(g))

Or in plain English it is a method that takes in another method and then runs it on its own result indefinitely. Because Y(g) and g(Y(g)) are equivalent, if g applied to some value x yields that same value x back then the method as a whole will resolve to x via simple substitution instead of running forever.

how it applies to our configuration

Because fixed point combinators are able to define something in relation to itself we can utilize them to define a configuration relative to other properties of that same configuration.

{ config }: {
	subject = "world";
	greeting = "Hello ${config.subject}!";
}

This function takes in a configuration value and then resolves a value that is equivalent to the original value supplied to the configuration. This means the result of greeting is Hello world!. If the value of subject was to be changed or somehow overwritten then the resulting greeting would also change to reflect that same value.

module/submodule structure

nixpkgs uses fixed points to create a module system for itself. The module system has 3 fundamental primitives that a method can yield: imports, options, and config.

imports are a list of other modules that will be resolved in concert with the module that is already being resolved.

options is a set of definitions on how values inside of the config primitive can be defined.

config is the values that the module itself will yield after everything is applied.

{ config, lib, ... }: {
	imports = [
		./hardware-config.nix
	];
	options = {
		username = lib.mkOption {
			type = lib.types.str;
			default = "user";
		};
	};
	config = {
		username = "admin";
	};
}

If you do not define any new options in a module then you can omit the config keyword and just define the configuration options at the top level.

{ config, lib, ... }: {
	username = "admin";
}

dendrite structure

While the module system is useful for defining things that have hard constraints to them sometimes we need a more free form way of defining things. For example when composing many modules it can be hard to keep track of a large import tree by file path. Instead of doing that we can instead automatically import all of the files that are defined as a part of a directory and then compose them together into a list of named modules.

# service-a.nix
{...}: {
	modules.nixos.service-a = { config, ... }: {
		# define service a here
	};
}
# service-b.nix
{...}: {
	modules.nixos.service-b = { config, ... }: {
		# define service b here
	};
}
# system.nix
{self, ...}: {
	modules.nixos.system = { config, ...}: {
		imports = [
			self.modules.nixos.service-a
			self.modules.nixos.service-b
		];

		# define system here
	};
}