Wednesday, January 26, 2022

Nixpkgs overlays are monoids

overlay-monoid

Nixpkgs supports overriding sets of packages using overlays and these overrides bear many similarities to object-oriented inheritance.

As a simple example, I can disable tests for the hello package in Nixpkgs using code that superficially resembles a subclass overriding a superclass method:

# ./example.nix

let
  overlay = self: super: {
    hello = super.hello.overrideAttrs (old: {
      doCheck = false;
    });
  };

  pkgs = import <nixpkgs> { overlays = [ overlay ]; };

in
  pkgs.hello

Here the super identifier plays a role similar to an object-oriented superclass: if you squint and view the package set preceding the override as the “superclass” then the above code defines the hello package for my “subclass” as being the same as the hello package from the “superclass” except without tests.

Also, just like in object-oriented programming, your “methods” (i.e. packages) can refer to other “methods” from within the same “class”, using self. For example, I can specify that I want the hello package to gratuitously run cowsay after the installation phase, like this:

# ./example.nix

let
  overlay = self: super: {
    hello = super.hello.overrideAttrs (old: {
      postInstall = "${self.cowsay}/bin/cowsay 'Installation complete'";
    });
  };

  pkgs = import <nixpkgs> { overlays = [ overlay ]; };

in
  pkgs.hello

… and if we build that we’ll see the output from cowsay in the build logs:

$ nix-build ./example.nix

 _______________________ 
< Installation complete >
 ----------------------- 
        \   ^__^
         \  (oo)\_______
            (__)\       )\/\
                ||----w |
                ||     ||
@nix { "action": "setPhase", "phase": "fixupPhase" }
post-installation fixup
gzipping man pages under /nix/store/xid1pxd0bccq8592pbjrb5b9k4qv3zzq-hello-2.10/
strip is /nix/store/hm2qzyqh6bh872rwlpjl4kw7a1nk173d-clang-wrapper-11.1.0/bin/st
stripping (with command strip and flags -S) in /nix/store/xid1pxd0bccq8592pbjrb5
patching script interpreter paths in /nix/store/xid1pxd0bccq8592pbjrb5b9k4qv3zzq
/nix/store/xid1pxd0bccq8592pbjrb5b9k4qv3zzq-hello-2.10

You can also combine multiple overlays, which lets you spread out these sorts of overrides into separate logical units. For example, we can create one overlay that disable tests for the hello package and a second overlay that adds the cowsay post-install step, like this:

let
  overlay0 = self: super: {
    hello = super.hello.overrideAttrs (old: {
      doCheck = false;
    });
  };

  overlay1 = self: super: {
    hello = super.hello.overrideAttrs (old: {
      postInstall = "${self.cowsay}/bin/cowsay 'Installation complete'";
    });
  };

  pkgs = import <nixpkgs> { overlays = [ overlay0 overlay1 ]; };

in
  pkgs.hello

Under the hood, when you specify multiple overlays they are combined using the pkgs.lib.composeExtensions function (which will be relevant in just a second).

Monoids

Overlays are not only practical, but also theoretically cool, because overlays are monoids!

To see why, we have to first establish the three things that constitute a monoid:

  • Every monoid has a corresponding type, which we’ll denote as M

  • Every monoid has an associative binary operator, which we’ll denote as ×

    This operator has type: M -> M -> M (using Haskell notation). In other words it is a function of two inputs of type M and returns an output, also of type M.

  • Every monoid has an “identity” of that operator, which we’ll denote as 1

    This “identity” is a value of type M.

When we say that × is associative, we mean that for any three values (e.g. a, b, and c) of type M, the following equation is true:

(a × b) × c = a × (b × c)

In other words, the way in which we group multiplication does not change the result. In fact, associativity means that we can elide the parentheses and the meaning of the expression is still unambiguous:

a × b × c

When we say that 1 is the “identity” of ×, we mean that for any value (e.g. a) of type M, the following equations are true:

1 × a = a

a × 1 = a

Other monoids

Here we use × to denote the binary operator and 1 to denote the corresponding identity value because we want to reuse our intuition that multiplication is associative and the number 1 is the identity of multiplication. However, monoids are more general than numbers and multiplication; there might be other binary operators and identity elements that behave in the same way.

For example, Nix attribute sets are also monoids, if we replace × with // and replace 1 with { }:

# // is an associative binary operator
(a // b) // c = a // (b // c)

# … and { } is the identity of //
{ } // a = a

a // { } = a

Also, as the title suggests, overlays from Nixpkgs are yet another example of a monoid! We can illustrate this by defining the three components of the “overlay monoid”:

  • The type M (using Haskell notation) is:

    -- Nix derivations are not actually text, but this keeps the example simple
    type Derivation = Text
    
    type PackageSet = Map Text Derivation
    
    type M = PackageSet -> PackageSet -> PackageSet
    
    -- … which we can expand out to the following equivalent type if we prefer:
    type M = Map Text Derivation -> Map Text Derivation -> Map Text Derivation
  • The binary operator is pkgs.lib.composeExtensions (the same function I mentioned earlier which combines overlays)

    The composeExtensions function is defined like this in Nixpkgs (refactored to improve the clarity of upcoming examples):

    composeExtensions = f: g:
        self: super:
            f self super // g self (super // f self super);

    Using object-oriented terminology, you can read that as saying: “to combine the methods defined in both f and g, first extend g’s superclass with all of f’s methods, then combine both sets of methods, giving precedence to methods defined in g”.

    The equivalent Haskell type and implementation would be:

    composeExtensions :: M -> M -> M
    composeExtensions f g =
        \self super ->
            Map.union (g self (Map.union (f self super) super)) (f self super)

    Carefully note that in the above Haskell code:

    • f has type M
    • g has type M
    • Everything past the = sign (i.e. \self super -> …) has type M

    It might help to expand out the Haskell type since the M type synonym is hiding a lot of complexity:

    -- This larger type is equivalent to the previous type:
    composeExtensions
      :: (PackageSet -> PackageSet -> PackageSet)  -- ← M
      -> (PackageSet -> PackageSet -> PackageSet)  -- ← M
      -> (PackageSet -> PackageSet -> PackageSet)  -- ← M
    
    -- We can expand things out further to this even larger equivalent type:
    composeExtensions
      :: (Map Text Derivation -> Map Text Derivation -> Map Text Derivation)
      -> (Map Text Derivation -> Map Text Derivation -> Map Text Derivation)
      -> (Map Text Derivation -> Map Text Derivation -> Map Text Derivation)
  • The identity value is (self: super: { }) (the empty overlay)

    The equivalent Haskell type and implementation would be:

    identityExtension :: M
    identityExtension =
        \self super -> Map.empty
    
    -- The following types are also equivalent:
    identityExtension
        :: PackageSet -> PackageSet -> PackageSet
    
    identityExtension
        :: Map Text Derivation -> Map Text Derivation -> Map Text Derivation

All we’re missing to establish that this is a bona-fide monoid is to prove that composeExtensions is an associative function and that identityExtension is its identity. We’ll do so using equational reasoning, but in Nix rather than Haskell:

It’s easier to prove the identity laws, so we’ll start with those:

composeExtensions (self: super: { }) f

# Replace composeExtensions with its definition
=   self: super:
            (self: super: { }) self super
        //  f self (super // (self: super: { }) self super)

# (self: super: e) self super = e
=   self: super: { } // f self (super // { })

# { } // a = a
=   self: super: f self (super // { })

# a // { } = a
=   self: super: f self super

# η-reduction
=   f

The other identity law is equally simple to prove:

composeExtensions f (self: super: { })

# Replace composeExtensions with its definition
=   self: super: f self super // (self: super: { }) self (super // f self super)

# β-reduction
=   self: super: f self super // { }

# a // { } = a
=   self: super: f self super

# η-reduction
=   f

Now, let’s prove that composeExtensions is associative, which means proving that:

composeExtensions (composeExtensions f g) h =
  composeExtensions f (composeExtensions g h)

We’ll begin from the left-hand side of the equation and keep rewriting until we reach the right-hand side of the equation:

composeExtensions (composeExtensions f g) h

# Replace the inner composeExtensions with its definition
=   composeExtensions
        (self: super: f self super // g self (super // f self super))
        h

# Replace the outer composeExtensions with its definition
=   self: super:
            (self: super: f self super // g self (super // f self super))
                self
                super
        //  h self
                (   super
                //  (self: super:
                        f self super // g self (super // f self super)
                    )
                        self
                        super
                )

# (self: super: e) self super = e
=   self: super:
            f self super
        //  g self (super // f self super)
        //  h self (super // f self super // g self (super // f self super))

# Factor out the three occurrences of `super // f self super` using a lambda
=   self: super:
            f self super
        //  (super: g self super // h self (super // g self super))
                (super // f self super)

# e = (self: e) self
=   self: super:
            f self super
        //  (self: super: g self super // h self (super // g self super)) self
                (super // f self super)

# Definition of composeExtensions, but in reverse
=   composeExtensions
        f
        (self: super: g self super // h self (super // g self super))

# Definition of composeExtensions, but in reverse
=   composeExtensions f (composeExtensions g h)

Generalization

In fact, the above implementation and the proofs of associativity/identity still work if you:

  • replace // with any associative operator
  • replace { } with the corresponding identity of the associative operator

In other words, we can generalize our implementation by replace Nix attribute sets with any arbitrary monoid! We can codify this neat property with the following Haskell type and Monoid instance:

-- This generalizes our previous overlay type
newtype Overlay m = Overlay { runOverlay :: m -> m -> m }

-- The `(<>)` operator generalizes our previous `composeExtensions` function
instance Semigroup m => Semigroup (Overlay m) where
    Overlay f <> Overlay g =
        Overlay (\self super -> f self super <> g self (super <> f self super))

-- `mempty` generalizes our previous `identityExtension`
instance Monoid m => Monoid (Overlay m) where
    mempty = Overlay (\self super -> mempty)

We can prove that this code generalizes the previous code by showing how we can implement the old overlay type and functions in terms of the new ones. The old code becomes a special case of the new code when we replace the type parameter m with Dual (Map Text Derivation):

{-# LANGUAGE TypeApplications #-}

import Data.Coerce (coerce)
import Data.Map (Map)
import Data.Monoid (Dual(..))

import Data.Text (Text)

newtype Overlay m = Overlay { runOverlay :: m -> m -> m }

instance Semigroup m => Semigroup (Overlay m) where
    Overlay f <> Overlay g =
        Overlay (\self super -> f self super <> g self (super <> f self super))

instance Monoid m => Monoid (Overlay m) where
    mempty = Overlay (\self super -> mempty)

type Derivation = Text

type PackageSet = Map Text Derivation

type OldOverlay = PackageSet -> PackageSet -> PackageSet

type NewOverlay = Overlay (Dual PackageSet)

composeExtensions :: OldOverlay -> OldOverlay -> OldOverlay
composeExtensions =
    coerce @(NewOverlay -> NewOverlay -> NewOverlay)
           @(OldOverlay -> OldOverlay -> OldOverlay)
           (<>)

identityExtension :: OldOverlay
identityExtension = coerce @NewOverlay @OldOverlay mempty

Conclusion

I’m not sure if there would be any applications of this Overlay type within the Haskell ecosystem, so I didn’t bother packaging up the latter Overlay type and Monoid instance. However, if you think this might be useful in your code then just let me know and I can create a tiny package for this purpose.

Hopefully this post illustrates how Nixpkgs overlays are actually a pretty principled system for overrides. Also, you might be able to formulate object-oriented inheritance in the same way, too, due to the similarities between Nix’s overlay system and object-oriented programming. The main difference is that Nix’s overlay system is weakly-typed, so to really give this a proper OOP treatment, you’d probably have to:

  • replace Nix’s attribute sets with more strongly-typed records
  • replace the Monoid with a more strongly-typed Category

… but I haven’t taken the time to fully flesh out that idea. Also, I’m not sure if it could be implemented in Haskell, since Haskell does not support anonymous records, but it might work just fine in PureScript.