Wednesday, September 7, 2022

nix-serve-ng: A faster, more reliable, drop-in replacement for nix-serve

nix-serve-ng

Our team at Arista Networks is happy to announce nix-serve-ng, a backwards-compatible Haskell rewrite of nix-serve (a service for hosting a /nix/store as a binary cache). It provides better reliability and performance than nix-serve (ranging from ≈ 1.5× to 32× faster). We wrote nix-serve-ng to fix scaling bottlenecks in our cache and we expect other large-scale deployments might be interested in this project, too.

This post will focus more on the background behind the development process and comparisons to other Nix cache implementations. If you don’t care about any of that then you can get started by following the instructions in the repository’s README.

Background

Before we began this project there were at least two other open source rewrites of nix-serve-ng that we could have adopted instead of nix-serve:

  • eris - A Perl rewrite of nix-serve

    Note: the original nix-serve is implemented in Perl, and eris is also implemented in Perl using a different framework.

  • harmonia - A Rust rewrite of nix-serve

The main reason we did not go with these two alternatives is because they are not drop-in replacements for the original nix-serve. We could have fixed that, but given how simple nix-serve is I figured that it would be simpler to just create our own. nix-serve-ng only took a couple of days for the initial version and maybe a week of follow-up fixes and performance tuning.

We did not evaluate the performance or reliability of eris or harmonia before embarking on our own nix-serve replacement. However, after nix-serve-ng was done we learned that it was significantly faster than the alternatives (see the Performance section below). Some of those performance differences are probably fixable, especially for harmonia. That said, we are very happy with the quality of our solution.

Backwards compatibility

One important design goal for this project is to be significantly backwards compatible with nix-serve. We went to great lengths to preserve compatibility, including:

  • Naming the built executable nix-serve

    Yes, even though the project name is nix-serve-ng, the executable built by the project is named nix-serve.

  • Preserving most of the original command-line options, including legacy options

    … even though some are unused.

In most cases you can literally replace pkgs.nix-serve with pkgs.nix-serve-ng and it will “just work”. You can even continue to use the existing services.nix-serve NixOS options.

The biggest compatibility regression is that nix-serve-ng cannot be built on MacOS. It is extremely close to supporting MacOS save for this one bug in Haskell’s hsc2hs tool: haskell/hsc2hs - #26. We left in all of the MacOS shims so that if that bug is ever fixed then we can get MacOS support easily.

For more details on the exact differences compared to nix-serve, see the Result / Backwards-compatibility section of the README.

Performance

nix-serve-ng is faster than all of the alternatives according to both our formal benchmarks and also informal testing. The “Benchmarks” section of our README has the complete breakdown but the relevant part is this table:

Speedups (compared to nix-serve):

Benchmark nix-serve eris harmonia nix-serve-ng
Fetch present NAR info ×10 1.0 0.05 1.33 1.58
Fetch absent NAR info ×1 1.0 0.06 1.53 1.84
Fetch empty NAR ×10 1.0 0.67 0.59 31.80
Fetch 10 MB NAR ×10 1.0 0.64 0.60 3.35

… which I can summarize like this:

  • nix-serve-ng is faster than all of the alternatives across all use cases
  • eris is slower than the original nix-serve across all use cases
  • harmonia is faster than the original nix-serve for NAR info lookups, but slower for fetching NARs

These performance results were surprising for a few reasons:

  • I was not expecting eris to be slower than the original nix-serve implementation

    … especially not NAR info lookups to be ≈ 20× slower. This is significant because NAR info lookups typically dominate a Nix cache’s performance. In my (informal) experience, the majority of a Nix cache’s time is spent addressing failed cache lookups.

  • I was not expecting harmonia (the Rust rewrite) to be slower than the original nix-serve for fetching NARs

    This seems like something that should be fixable. harmonia will probably eventually match our performance because Rust has a high performance ceiling.

  • I was not expecting a ≈ 30x speedup for nix-serve-ng fetching small NARs

    I had to triple-check that neither nix-serve-ng nor the benchmark were broken when I saw this speedup.

So I investigated these performance differences to help inform other implementations what to be mindful of.

Performance insights

We didn’t get these kinds of speed-ups by being completely oblivious to performance. Here are the things that we paid special attention to to keep things efficient, in order of lowest-hanging to highest-hanging fruit:

  • Don’t read the secret key file on every NAR fetch

    This is a silly thing that the original nix-serve does that is the easiest thing to fix.

    eris and harmonia also fix this, so this optimization is not unique to our rewrite.

  • We bind directly to the Nix C++ API for fetching NARs

    nix-serve, eris, and harmonia all shell out to a subprocess to fetch NARs, by invoking either nix dump-path or nix-store --dump to do the heavy lifting. In contrast, nix-serve-ng binds to the Nix C++ API for this purpose.

    This would definitely explain some of the performance difference when fetching NARs. Creating a subprocess has a fixed overhead regardless of the size of the NAR, which explains why we see the largest performance difference when fetching tiny NARs since the overhead of creating a subprocess would dominate the response time.

    This may also affect throughput for serving large NAR files, too, by adding unnecessary memory copies/buffering as part of streaming the subprocess output.

  • We minimize memory copies when fetching NARs

    We go to great lengths to minimize the number of intermediate buffers and copies when streaming the contents of a NAR to a client. To do this, we exploit the fact that Haskell’s foreign function interface works in both directions: Haskell code can call C++ code but also C++ code can call Haskell code. This means that we can create a Nix C++ streaming sink from a Haskell callback function and this eliminates the need for intermediate buffers.

    This likely also improves the throughput for serving NAR files. Only nix-serve-ng performs this optimization (since nix-serve-ng is the only one that uses the C++ API for streaming NAR contents).

  • Hand-write the API routing logic

    We hand-write all of the API routing logic to prioritize and optimize the hot path (fetching NAR info).

    For example, a really simple thing that the original nix-serve does inefficiently is to check if the path matches /nix-cache-info first, even though that is an extremely infrequently used path. In our API routing logic we move that check straight to the very end.

    These optimizations likely improve the performance of NAR info requests. As far as I can tell, only nix-serve-ng performs these optimizations.

I have not benchmarked the performance impact of each of these changes in isolation, though. These observations are purely based on my intuition.

Features

nix-serve-ng is not all upsides. In particular, nix-serve-ng is missing features that some of the other rewrites provide, such as:

  • Greater configurability
  • Improved authentication support
  • Monitoring/diagnostics/status APIs

Our focus was entirely on scalability, so the primary reason to use nix-serve-ng is if you prioritize performance and uptime.

Conclusion

We’ve been using nix-serve-ng long enough internally that we feel confident endorsing its use outside our company. We run a particularly large Nix deployment internally (which is why we needed this in the first place), so we have stress tested nix-serve-ng considerably under heavy and realistic usage patterns.

You can get started by following these these instructions and let us know if you run into any issues or difficulties.

Also, I want to thank Arista Networks for graciously sponsoring our team to work on and open source this project

Monday, August 29, 2022

Stop calling everything "Nix"

nix-terminology

One of my pet peeves is when people abuse the term “Nix” without qualification when trying to explain the various components of the Nix ecosystem.

As a concrete example, a person might say:

“I hate Nix’s syntax”

… and when you dig into this criticism you realize that they’re actually complaining about the Nixpkgs API, which is not the same thing as the syntax of the Nix expression language.

So one of the goals of this post is to introduce some unambiguous terminology that people can use to refer to the various abstraction layers of the Nix ecosystem in order to avoid confusion. I’ll introduce each abstraction layer from the lowest level abstractions to the highest level abstractions.

Another reason I explain “Nix” in terms of these abstraction layers is because this helps people consult the correct manual. The Nix ecosystem provides three manuals that you will commonly need to refer to in order to become more proficient:

… and I hope by the end of this post it will be clearer which manual interests you for any given question.

Edit: Domen Ko┼żar pointed out that there is an ongoing effort to standardize terminology here:

I’ll update the post to match the agreed-upon terminology when that is complete.

Layer #0: The Nix store

I use the term “Nix store” to mean essentially everything you can manage with the nix-store command-line tool.

That is the simplest definition, but to expand upon that, I mean the following files:

  • Derivations: /nix/store/*.drv
  • Build products: /nix/store/* without a .drv extension
  • Log files: /nix/var/log/nix/drvs/**
  • Garbage collection roots: /nix/var/nix/gcroots/**

… and the following operations:

  • Realizing a derivation

    i.e. converting a .drv file to the corresponding build products using nix-store --realise

  • Adding static files to the /nix/store

    i.e. nix-store --add

  • Creating GC roots for build products

    i.e. the --add-root option to nix-store

  • Garbage collecting derivations not protected by a GC root

    i.e. nix-store --gc

There are other things the Nix store supports (like profile management), but these are the most important operations.

CAREFULLY NOTE: the “Nix store” is independent of the “Nix language” (which we’ll define below). In other words, you could replace the front-end Nix programming language with another language (e.g. Guile scheme, as Guix does). This is because the Nix derivation format (the .drv files) and the nix-store command-line interface are both agnostic of the Nix expression language. I have a talk which delves a bit more into this subject:

Layer #1: The Nix language

I use the term “Nix language” to encompass three things:

  • The programming language: source code we typically store in .nix files
  • Instantiation: the interpretation of Nix code to generate .drv files
  • Flakes: pure evaluation and instantiation caching

To connect this with the previous section, the typical pipeline for converting Nix source code to a build product is:

Nix source code (*.nix)            │ Nix language
      ↓ Instantiation              ├─────────────
Nix derivation (/nix/store/*.drv)  │
      ↓ Realization                │ Nix store
Nix build product (/nix/store/*)   │

In isolation, the Nix language is “just” a purely functional programming language with simple language constructs. For example, here is a sample Nix REPL session:

nix-repl> 2 + 2
4

nix-repl> x = "world"   

nix-repl> "Hello, " + x  
"Hello, world"

nix-repl> r = { a = 1; b = true; }

nix-repl> if r.b then r.a else 0
1

However, as we go up the abstraction ladder the idiomatic Nix code we’ll encounter will begin to stray from that simple functional core.

NOTE: Some people will disagree with my choice to include flakes at this abstraction layer since flakes are sometimes marketed as a dependency manager (similar to niv). I don’t view them in this way and I treat flakes as primarily as mechanism for purifying evaluation and caching instantiation, as outlined in this post:

… and if you view flakes in that capacity then they are a feature of the Nix language since evaluation/instantiation are the primary purpose of the programming language.

Layer #2: The Nix build tool

This layer encompasses the command-line interface to both the “Nix store” and the “Nix language”.

This includes (but is not limited to):

  • nix-store (the command, not the underlying store)
  • nix-instantiate
  • nix-build
  • nix-shell
  • nix subcommands, including:
    • nix build
    • nix run
    • nix develop
    • nix log
    • nix flake

I make this distinction because the command-line interface enables some additional niceties that are not inherent to the underlying layers. For example, the nix build command has some flake integration so that you can say nix build someFlake#somePackage and this command-line API nicety is not necessarily inherent to flakes (in my view).

Also, many of these commands operate at both Layer 0 and Layer 1, which can blur the distinction between the two. For example the nix-build command can accept a layer 1 Nix program (i.e. a .nix file) or a layer 0 derivation (i.e. a .drv file).

Another thing that blurs the distinction is that the Nix manual covers all three of the layers introduced so far, ranging from the Nix store to the command-line interface. However, if you want to better understand these three layers then that is correct place to begin:

Layer #3: Nixpkgs

Nixpkgs is a software distribution (a.k.a. “distro”) for Nix. Specifically, all of the packaging logic for Nixpkgs is hosted on GitHub here:

This repository contains a large number of Nix expressions for building packages across several platforms. If the “Nix language” is a programming language then “Nixpkgs” is a gigantic “library” authored within that language. There are other Nix “libraries” outside of Nixpkgs but Nixpkgs is the one you will interact with the most.

The Nixpkgs repository establishes several widespread idioms and conventions, including:

  • The standard environment (a.k.a. stdenv) for authoring a package
    • There are also language-specific standard-environments, too
  • A domain-specific language for overriding individual packages or sets of packages

When people complain about “Nix’s syntax”, most of the time they’re actually complaining about Nixpkgs and more specifically complaining about the Nixpkgs system for overriding packages. However, I can see how people might mistake the two.

The reason for the confusion is that the Nixpkgs support for overrides is essentially an embedded domain-specific language, meaning that you still express everything in the Nix language (layer 1), but the ways in which you express things is fundamentally different than if you were simply using low-level Nix language features.

As a contrived example, this “layer 1” Nix code:

let
  x = 1;

  y = x + 2;

… would roughly correspond to the following “layer 3” Nixpkgs overlay:

self: super: {
  x = 1;

  y = self.x + 2;
}

The reason why Nixpkgs doesn’t do the simpler “layer 1” thing is because Nixpkgs is designed to support “late binding” of expressions, meaning that everything can be overridden, even dependencies deep within the dependency tree. Moreover, this overriding is done in such a way that everything “downstream” of the overrride (i.e. all reverse dependencies) pick up the change correctly.

As a more realistic example, the following program:

let
  pkgs = import <nixpkgs> { };

  fast-tags =
    pkgs.haskell.lib.justStaticExecutables pkgs.haskellPackages.fast-tags;

  fast-tags-no-tests =
    pkgs.haskell.lib.dontCheck fast-tags;

in
  fast-tags-no-tests

… is simpler, but is not an idiomatic use of Nixpkgs because it is not using the overlay system and therefore does not support late binding. The more idiomatic analog would be:

let
  overlay = self: super: {
    fast-tags =
      self.haskell.lib.justStaticExecutables self.haskellPackages.fast-tags;

    fast-tags-no-tests =
      self.haskell.lib.dontCheck self.fast-tags;
  };

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

in
  pkgs.fast-tags-no-tests

You can learn more about this abstraction layer by consulting the Nixpkgs manual:

Layer #4: NixOS

NixOS is an operating system that is (literally) built on Nixpkgs. Specifically, there is a ./nixos/ subdirectory of the Nixpkgs repository for all of the NixOS-related logic.

NixOS is based on the NixOS module system, which is yet another embedded domain-specific language. In other words, you configure NixOS with Nix code, but the idioms of that Nix code depart even more wildly from straightforward “layer 1” Nix code.

NixOS modules were designed to look more like Terraform modules than Nix code, but they are still technically Nix code. For example, this is what the NixOS module for the lorri service looks like at the time of this writing:

{ config, lib, pkgs, ... }:

let
  cfg = config.services.lorri;
  socketPath = "lorri/daemon.socket";
in {
  options = {
    services.lorri = {
      enable = lib.mkOption {
        default = false;
        type = lib.types.bool;
        description = lib.mdDoc ''
          Enables the daemon for `lorri`, a nix-shell replacement for project
          development. The socket-activated daemon starts on the first request
          issued by the `lorri` command.
        '';
      };
      package = lib.mkOption {
        default = pkgs.lorri;
        type = lib.types.package;
        description = lib.mdDoc ''
          The lorri package to use.
        '';
        defaultText = lib.literalExpression "pkgs.lorri";
      };
    };
  };

  config = lib.mkIf cfg.enable {
    systemd.user.sockets.lorri = {
      description = "Socket for Lorri Daemon";
      wantedBy = [ "sockets.target" ];
      socketConfig = {
        ListenStream = "%t/${socketPath}";
        RuntimeDirectory = "lorri";
      };
    };

    systemd.user.services.lorri = {
      description = "Lorri Daemon";
      requires = [ "lorri.socket" ];
      after = [ "lorri.socket" ];
      path = with pkgs; [ config.nix.package git gnutar gzip ];
      serviceConfig = {
        ExecStart = "${cfg.package}/bin/lorri daemon";
        PrivateTmp = true;
        ProtectSystem = "strict";
        ProtectHome = "read-only";
        Restart = "on-failure";
      };
    };

    environment.systemPackages = [ cfg.package ];
  };
}

You might wonder how NixOS relates to the underlying layers. For example, if Nix is a build system, then how do you “build” NixOS? I have another post which elaborates on that subject here:

Also, you can learn more about this abstraction layer by consulting the NixOS manual:

Nix ecosystem

I use the term “Nix ecosystem” to describe all of the preceding layers and other stuff not mentioned so far (like hydra, the continuous integration service).

This is not a layer of its own, but I mention this because I prefer to use “Nix ecosystem” instead of “Nix” to avoid ambiguity, since the latter can easily be mistaken for an individual abstraction layer (especially the Nix language or the Nix build tool).

However, when I do hear people say “Nix”, then I generally understand it to mean the “Nix ecosystem” unless they clarify otherwise.

Conclusion

Hopefully this passive aggressive post helps people express themselves a little more precisely when discussing the Nix ecosystem.

If you enjoy this post, you will probably also like this other post of mine:

… since that touches on the Nixpkgs and NixOS embedded domain-specific languages and how they confound the user experience.

I’ll conclude this post with the following obligatory joke:

I’d just like to interject for a moment. What you’re refering to as Nix, is in fact, NixOS, or as I’ve recently taken to calling it, Nix plus OS. Nix is not an operating system unto itself, but rather another free component of a fully functioning ecosystem made useful by the Nix store, Nix language, and Nix build tool comprising a full OS as defined by POSIX.

Many Guix users run a modified version of the Nix ecosystem every day, without realizing it. Through a peculiar turn of events, the operating system based on Nix which is widely used today is often called Nix, and many of its users are not aware that it is basically the Nix ecosystem, developed by the NixOS foundation.

There really is a Nix, and these people are using it, but it is just a part of the system they use. Nix is the expression language: the program in the system that specifies the services and programs that you want to build and run. The language is an essential part of the operating system, but useless by itself; it can only function in the context of a complete operating system. Nix is normally used in combination with an operating system: the whole system is basically an operating system with Nix added, or NixOS. All the so-called Nix distributions are really distributions of NixOS!

Sunday, August 28, 2022

Incrementally package a Haskell program using Nix

incremental-nix

This post walks through how to take a standalone Haskell file and progressively package the file using Nix. In other words, we will tour a spectrum of packaging options ranging from simple to fancy.

The running example will be the following standalone single-file Haskell program:

I won’t go into detail about what that program does, although you can study the program if you are curious. Essentially, I’m planning to deliver a talk based on that program at this year’s MuniHac and I wanted to package it up so that other people could collaborate on the program with me during the hackathon.

When I began writing this post, there was no packaging logic for this program; it’s a standalone Haskell file. However, this file has several dependencies outside of Haskell’s standard library, so up until now I needed some way to obtain those dependencies for development.

Stage 0: ghc.withPackages

The most low-tech way that you can hack on a Haskell program using Nix is to use nix-shell to obtain a transient development environment (this is what I had done up until now).

Specifically, you can do something like this:

$ nix-shell --packages 'ghc.withPackages (pkgs: [ pkgs.mtl pkgs.MemoTrie pkgs.containers pkgs.pretty-show ])'

… where pkgs.mtl and pkgs.MemoTrie indicate that I want to include the mtl and MemoTrie packages in my Haskell development environment.

Inside of that development environment I can build and run the file using ghc. For example, I can use ghc -O to build an executable to run:

[nix-shell]$ ghc -O Spire.hs
[nix-shell]$ ./Spire

… or if I don’t care about optimizations I can interpret the file using runghc:

$ runghc Spire.hs

Stage 1: IDE support

Once I’m inside a Nix shell I can begin to take advantage of integrated development environment (IDE) support.

The two most common tools Haskell developers use for rapid feedback are ghcid and haskell-language-server:

  • ghcid provides a command-line interface for fast type-checking feedback but doesn’t provide other IDE-like features

  • haskell-language-server is more of a proper IDE that you use in conjunction with some editor

I can obtain either tool by exiting from the shell and creating a new shell that includes the desired tool.

For example, if I want to use ghcid then I recreate the nix-shell using the following command:

$ nix-shell --packages ghcid 'ghc.withPackages (pkgs: [ pkgs.mtl pkgs.MemoTrie pkgs.containers pkgs.pretty-show ])'

… and then I can tell ghcid to continuously type-check my file using:

[nix-shell]$ ghcid Spire.hs

If I want to use haskell-language-server, then I recreate the nix-shell using this command:

$ nix-shell --packages haskell-language-server 'ghc.withPackages (pkgs: [ pkgs.mtl pkgs.MemoTrie pkgs.containers pkgs.pretty-show ])'

… and then I can explore the code in any editor that supports the language server protocol.

Note that if you use VSCode as your editor then you may need to install some additional plugins:

… and the next section will show how to install VSCode and those plugins using Nix.

However, once you do install those plugins then you can open the file in VSCode from within the nix-shell using:

[nix-shell]$ code Spire.hs

… and once you trust the file the IDE features will kick in.

Stage 2: Global development environment

Sometimes I like to globally install development tools that are commonly shared between projects. For example, if I use ghcid or haskell-language-server across all my projects then I don’t want to have to explicitly enumerate that tool in each project’s Nix shell.

Moreover, my tool preferences might not be shared by other developers. If I share my nix-shell with other developers for a project then I probably don’t want to add editors/IDEs or other command-line tools to that environment because then they have to download those tools regardless of whether they plan to use them.

However, I don’t want to globally install development tools like this:

$ nix-env --install --file '<nixpkgs>' --attr ghcid
$ nix-env --install --file '<nixpkgs>' --attr haskell-language-server

Part of the reason I use Nix is to avoid imperatively managing my development environment. Fortunately, though, nix-env supports a more declarative way of managing dependencies.

What you can do instead is save a file like this to ~/default.nix:

let
  # For VSCode
  config = { allowUnfree = true; };

  overlay = pkgsNew: pkgsOld: {
    # Here's an example of how to use Nix to install VSCode with plugins managed
    # by Nix, too
    vscode-with-extensions = pkgsOld.vscode-with-extensions.override {
      vscodeExtensions = [
        pkgsNew.vscode-extensions.haskell.haskell
        pkgsNew.vscode-extensions.justusadam.language-haskell
      ]; 
    };
  };

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

in      
  { inherit (pkgs)
      # I included some sample useful development tools for Haskell.  Feel free
      # to customize.
      cabal-install
      ghcid
      haskell-language-server
      stylish-haskell
      vscode-with-extensions 
    ; 
  }     

… and once you create that file you have two options.

The first option is that you can set your global development environment to match the file by running:

$ nix-env --remove-all --install --file ~/default.nix

NOTE: At the time of this writing you may also need to add --system x86_64-darwin if you are trying out these examples on an M1 Macbook. For more details, see:

Carefully note the --remove-all, which resets your development environment to match the file, so that nothing from your old development environment is accidentally carried over into your new development environment. This makes our use of the nix-env command truly declarative.

The second option is that you can change the file to create a valid shell, like this:

let
  config = { allowUnfree = true; };

  overlay = pkgsNew: pkgsOld: {
    vscode-with-extensions = pkgsOld.vscode-with-extensions.override {
      vscodeExtensions = [
        pkgsNew.vscode-extensions.haskell.haskell
        pkgsNew.vscode-extensions.justusadam.language-haskell
      ];
    };
  };

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

in
  pkgs.mkShell {
    packages = [
      pkgs.ghcid
      pkgs.haskell-language-server
      pkgs.stylish-haskell
      pkgs.vscode-with-extensions
      pkgs.cabal-install
    ];
  }

… and then run:

$ nix-shell ~/default.nix

Or, even better, you can rename the file to ~/shell.nix and then if you’re already in your home directory (e.g. you just logged into your system), then you can run:

$ nix-shell

… which will select ~/shell.nix by default. This lets you get a completely transient development environment so that you never have to install anything development tools globally.

These nix-shell commands stack, so you can first run nix-shell to obtain your global development environment and then use nix-shell a second time to obtain project-specific dependencies.

My personal preference is to use the declarative nix-env trick for installing global development tools. In my opinion it’s just as elegant as nix-shell and slightly less hassle.

Stage 3: Cabal

Anyway, enough about global development tools. Back to our Haskell project!

So ghc.withPackages is a great way to just start hacking on a standalone Haskell program when you don’t want to worry about packaging up the program. However, at some point you might want to share the program with the others or do a proper job of packaging if you’re trying to productionize the code.

That brings us to the next step, which is packaging our Haskell program with a Cabal file (a Haskell package manifest). We’ll need the cabal-install command-line tool before we proceed further, so you’ll want to add that tool to your global development environment (see the previous section).

To create our .cabal file we can run the following command from the top-level directory of our Haskell project:

$ cabal init --interactive
Should I generate a simple project with sensible defaults? [default: y] n

… and follow the prompts to create a starting point for our .cabal file.

After completing those choices and trimming down the .cabal file (to keep the example simple), I get a file that looks like this:

cabal-version:      2.4
name:               spire
version:            1.0.0
license:            BSD-3-Clause
license-file:       LICENSE

executable spire
    main-is:          Spire.hs
    build-depends:    base ^>=4.14.3.0
    default-language: Haskell2010

The only thing I’m going change for now is to add dependencies to the build-depends section and increase the upper bound on base::

cabal-version:      2.4
name:               spire
version:            1.0.0
license:            BSD-3-Clause
license-file:       LICENSE

executable spire
    main-is:          Spire.hs
    build-depends:    base >=4.14.3.0 && < 5
                    , MemoTrie
                    , containers
                    , mtl
                    , pretty-show
                    , transformers
    default-language: Haskell2010

Stage 4: cabal2nix --shell

Adding a .cabal file suffices to share our Haskell package with other Haskell developers if they’re not using Nix. However, if we want to Nix-enable package our package then we have a few options.

The simplest option is to run the following command from the top-level of the Haskell project:

$ cabal2nix --shell . > shell.nix

That will create something similar to the following shell.nix file:

{ nixpkgs ? import <nixpkgs> {}, compiler ? "default", doBenchmark ? false }:

let

  inherit (nixpkgs) pkgs;

  f = { mkDerivation, base, containers, lib, MemoTrie, mtl
      , pretty-show, transformers
      }:
      mkDerivation {
        pname = "spire";
        version = "1.0.0";
        src = ./.;
        isLibrary = false;
        isExecutable = true;
        executableHaskellDepends = [
          base containers MemoTrie mtl pretty-show transformers
        ];
        license = lib.licenses.bsd3;
      };

  haskellPackages = if compiler == "default"
                       then pkgs.haskellPackages
                       else pkgs.haskell.packages.${compiler};

  variant = if doBenchmark then pkgs.haskell.lib.doBenchmark else pkgs.lib.id;

  drv = variant (haskellPackages.callPackage f {});

in

  if pkgs.lib.inNixShell then drv.env else drv

… and if you run nix-shell within the same directory the shell environment will have the Haskell dependencies you need to build and run project using cabal:

$ nix-shell
[nix-shell]$ cabal run

… and tools like ghcid and haskell-language-server will also work within this shell, too. The only difference is that ghcid now takes no arguments, since it will auto-detect the cabal project in the current directory:

[nix-shell]$ ghcid

Note that this nix-shell will NOT include cabal by default. You will need to globally install cabal (see the prior section on “Global development environment”).

This cabal2nix --shell workflow is sufficiently lightweight that you can Nixify other people’s projects on the fly when hacking on them locally. A common thing I do if I need to make a change to a person’s project is to clone their repository, run:

$ cabal2nix --shell . > shell.nix
$ nix-shell

… and start hacking away. I don’t even need to upstream the shell.nix file I created in this way; I just keep it around locally for my own hacking.

In fact, I typically don’t want to upstream such a shell.nix file (even if the upstream author were receptive to Nix), because there are more robust Nix expressions we can upstream instead.

Stage 5: Custom shell.nix file

One disadvantage of cabal2nix --shell is that you have to re-run the command any time your dependencies change. However, if you’re willing to hand-write your own shell.nix file then you can create something more stable:

let
  overlay = pkgsNew: pkgsOld: {
    haskellPackages = pkgsOld.haskellPackages.override (old: {
      overrides = pkgsNew.haskell.lib.packageSourceOverrides {
        spire = ./.;
      };
    });
  };

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

in
  pkgs.haskellPackages.spire.env

The packageSourceOverrides is the key bit. Under the hood, that essentially runs cabal2nix for you any time your project changes and then generates your development environment from the result. You can also use packageSourceOverrides to specify non-default versions of dependencies, too:

let
  overlay = pkgsNew: pkgsOld: {
    haskellPackages = pkgsOld.haskellPackages.override (old: {
      overrides = pkgsNew.haskell.lib.packageSourceOverrides {
        spire = ./.;

        # Example of how to pin a dependency to a non-defaul version
        pretty-show = "1.9.5";
      };
    });
  };

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

in
  pkgs.haskellPackages.spire.env

… although that will only work for packages that have been released prior to the version of Nixpkgs that you’re depending on.

If you want something a bit more robust, you can do something like this:

let
  overlay = pkgsNew: pkgsOld: {
    haskellPackages = pkgsOld.haskellPackages.override (old: {
      overrides =
        pkgsNew.lib.fold
          pkgsNew.lib.composeExtensions
          (old.overrides or (_: _: { }))
          [ (pkgsNew.haskell.lib.packageSourceOverrides {
              spire = ./.;
            })
            (pkgsNew.haskell.lib.packagesFromDirectory {
              directory = ./packages;
            })
          ];
    });
  };

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

in
  pkgs.haskellPackages.spire.env

… and then you have the option to also depend on any dependency that cabal2nix knows how to generate:

$ mkdir packages

$ # Add the following file to version control to preserve the directory
$ touch packages/.gitkeep

$ cabal update

$ cabal2nix cabal://${PACKAGE_NAME}-${VERSION} > ./packages/${PACKAGE_NAME}.nix

… and that works even on bleeding-edge Haskell packages that Nixpkgs hasn’t picked up, yet.

Stage 6: Pinning Nixpkgs

All of the prior examples are “impure”, meaning that they depend on the ambient nixpkgs channel installed on the developer’s system. This nixpkgs channel might vary from system to system, meaning that each system might have different versions of nixpkgs installed, and then you run into issues reproducing each other’s builds.

For example, if you have a newer version of nixpkgs installed your Nix build for the above Haskell project might succeed, but then another developer might attempt to build your project with an older version of nixpkgs, which might select an older incompatible version of one of your Haskell dependencies.

Or, vice versa, the examples in this blog post might succeed at the time of this writing for the current version of nixpkgs but then as time goes on the examples might begin to fail for future versions of nixpkgs.

You can fix that by pinning Nixpkgs, which this post covers:

For example, we could pin nixpkgs for our global ~/default.nix like this:

let
  nixpkgs = builtins.fetchTarball {
    url    = "https://github.com/NixOS/nixpkgs/archive/0ba2543f8c855d7be8e90ef6c8dc89c1617e8a08.tar.gz";
    sha256 = "14ann7vz7qgfrw39ji1s19n1p0likyf2ag8h7rh8iwp3iv5lmprl";
  };

  config = { allowUnfree = true; };

  overlay = pkgsNew: pkgsOld: {
    vscode-with-extensions = pkgsOld.vscode-with-extensions.override {
      vscodeExtensions = [
        pkgsNew.vscode-extensions.haskell.haskell
        pkgsNew.vscode-extensions.justusadam.language-haskell
      ];
    };
  };

  pkgs = import nixpkgs { inherit config; overlays = [ overlay ]; };

in
  { inherit (pkgs)
      cabal-install
      ghcid
      haskell-language-server
      stylish-haskell
      vscode-with-extensions
    ;
  }

… which pins us to the tip of the release-22.05 branch at the time of this writing.

We can likewise pin nixpkgs for our project-local shell.nix like this:

let
  nixpkgs = builtins.fetchTarball {
    url    = "https://github.com/NixOS/nixpkgs/archive/0ba2543f8c855d7be8e90ef6c8dc89c1617e8a08.tar.gz";
    sha256 = "14ann7vz7qgfrw39ji1s19n1p0likyf2ag8h7rh8iwp3iv5lmprl";
  };

  overlay = pkgsNew: pkgsOld: {
    haskellPackages = pkgsOld.haskellPackages.override (old: {
      overrides = pkgsNew.haskell.lib.packageSourceOverrides {
        spire = ./.;
      };
    });
  };

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

in
  pkgs.haskellPackages.spire.env

Flakes

The final improvement we can make is the most important one of all: we can convert our project into a Nix flake:

There are two main motivations for flake-enabling our project:

  • To simplify managing inputs that we need to lock (e.g. nixpkgs)
  • To speed up our shell

To flake-enable our project, we’ll save the following code to flake.nix:

{ inputs = {
    nixpkgs.url = github:NixOS/nixpkgs/release-22.05;

    utils.url = github:numtide/flake-utils;
  };

  outputs = { nixpkgs, utils, ... }:
    utils.lib.eachDefaultSystem (system:
      let
        config = { };

        overlay = pkgsNew: pkgsOld: {
          spire =
            pkgsNew.haskell.lib.justStaticExecutables
              pkgsNew.haskellPackages.spire;

          haskellPackages = pkgsOld.haskellPackages.override (old: {
            overrides = pkgsNew.haskell.lib.packageSourceOverrides {
              spire = ./.;
            };
          });
        };

        pkgs =
          import nixpkgs { inherit config system; overlays = [ overlay ]; };

      in
        rec {
          packages.default = pkgs.haskellPackages.spire;

          apps.default = {
            type = "app";

            program = "${pkgs.spire}/bin/spire";
          };

          devShells.default = pkgs.haskellPackages.spire.env;
        }
    );
}

… and then we can delete our old shell.nix because we don’t need it anymore.

Now we can obtain a development environment by running:

$ nix develop

… and the above flake also makes it possible to easily build and run the program, too:

$ nix run    # Run the program
$ nix build  # Build the project

In fact, you can even run a flake without having to clone a repository. For example, you can run the example code from this blog post by typing:

$ nix run github:Gabriella439/spire

Moreover, we no longer have to take care of managing hashes for, say, Nixpkgs. The flake machinery takes care of that automatically for you and generates a flake.lock file which you can then add to version control. For example, the lock file I got was:

{
  "nodes": {
    "nixpkgs": {
      "locked": {
        "lastModified": 1661617163,
        "narHash": "sha256-NN9Ky47j8ohgPhA9JZyfkYIbbAo6RJkGz+7h8/exVpE=",
        "owner": "NixOS",
        "repo": "nixpkgs",
        "rev": "0ba2543f8c855d7be8e90ef6c8dc89c1617e8a08",
        "type": "github"
      },
      "original": {
        "owner": "NixOS",
        "ref": "release-22.05",
        "repo": "nixpkgs",
        "type": "github"
      }
    },
    "root": {
      "inputs": {
        "nixpkgs": "nixpkgs",
        "utils": "utils"
      }
    },
    "utils": {
      "locked": {
        "lastModified": 1659877975,
        "narHash": "sha256-zllb8aq3YO3h8B/U0/J1WBgAL8EX5yWf5pMj3G0NAmc=",
        "owner": "numtide",
        "repo": "flake-utils",
        "rev": "c0e246b9b83f637f4681389ecabcb2681b4f3af0",
        "type": "github"
      },
      "original": {
        "owner": "numtide",
        "repo": "flake-utils",
        "type": "github"
      }
    }
  },
  "root": "root",
  "version": 7
}

… and you can easily upgrade to, say, a newer revision of Nixpkgs if you need to.

Additionally, all of the Nix commands are now faster. Specifically, the first time you run a command Nix still needs to download and/or build dependencies, but subsequent runs are faster because Nix can skip the instantiation phase. For more details, see:

Conclusion

Flakes are our final destination, so that’s as far as this post will go. There are technically some more ways that we can overengineer things, but in my experience the idioms highlighted in this post are the ones that provide the highest power-to-weight ratio.

The key thing to take away is that the Nixpkgs Haskell infrastructure lets you smoothly transition from simpler approaches to more powerful approaches, and even the final flake-enabled approach is actually not that complicated.

Sunday, June 26, 2022

defaultable-map: An Applicative wrapper for Maps

defaultable-map: An Applicative wrapper for Maps

I’m announcing a small utility Haskell package I created that can wrap arbitrary Map-like types to provide Applicative and Alternative instances. You can find this package on Hackage here:

I can motivate why the Applicative and Alternative instances matter with a small example. Suppose that I define the following three Maps which are sort of like database tables:

import Defaultable.Map 

firstNames :: Defaultable (Map Int) String
firstNames = fromList [(0, "Gabriella"), (1, "Oscar"), (2, "Edgar")]

lastNames :: Defaultable (Map Int) String
lastNames = fromList [(0, "Gonzalez"), (2, "Codd"), (3, "Bryant")]

handles :: Defaultable (Map Int) String
handles = fromList [(0, "GabriellaG439"), (1, "posco"), (3, "avibryant")]

If you squint, you can think of these as analogous to database tables, where the primary key is an Int index:

> CREATE TABLE firstNames (id integer, firstName text);
> INSERT INTO firstNames (id, firstName) VALUES (0, 'Gabriella');
> INSERT INTO firstNames (id, firstName) VALUES (1, 'Oscar');
> INSERT INTO firstNames (id, firstName) VALUES (2, 'Edgar');
> SELECT * FROM firstNames;
id | firstName
---+----------
0  | Gabriella
1  | Oscar
2  | Edgar

> CREATE TABLE lastNames (id integer, lastName text);
> INSERT INTO lastNames (id, lastName) VALUES (0, 'Gonzalez');
> INSERT INTO lastNames (id, lastName) VALUES (2, 'Codd');
> INSERT INTO lastNames (id, lastName) VALUES (3, 'Bryant');
> SELECT * FROM lastNames;
id | lastName
---+---------
0  | Gonzalez
2  | Codd
3  | Bryant

> CREATE TABLE handles (id integer, handle text);
> INSERT INTO handles (id, handle) VALUES (0, 'GabriellaG439');
> INSERT INTO handles (id, handle) VALUES (1, 'posco');
> INSERT INTO handles (id, handle) VALUES (3, 'avibryant');
> SELECT * FROM handles;
id | handle
---+--------------
0  | GabriellaG439
1  | posco
3  | avibryant

The Defaultable (Map Int) type has a law-abiding Applicative instance, so we can safely “join” these “tables” using Applicative operations. For example, if we enable Haskell’s ApplicativeDo language extension then we can compute an “inner join” on tables like this:

{-# LANGUAGE ApplicativeDo #-}

innerJoin :: Defaultable (Map Int) (String, String)
innerJoin = do
    firstName <- firstNames
    lastName  <- lastNames
    return (firstName, lastName)

… and that evaluates to the following result:

Defaultable
    (fromList
        [ (0, ("Gabriella","Gonzalez"))
        , (2, ("Edgar"    ,"Codd"    ))
        ]
    )
    Nothing

… which is the same result we would have gotten from doing an inner join in SQL:

> SELECT firstNames.id, firstName, lastName
>     FROM firstNames INNER JOIN lastNames on firstNames.id = lastNames.id;
id | firstName | lastName
---+-----------+---------
0  | Gabriella | Gonzalez
2  | Edgar     | Codd

The Defaultable (Map Int) type also has a law-abiding Alternative instance, which we can combine with the Applicative instance to compute “left/right/outer joins”. For example, this “left join”:

leftJoin :: Defaultable (Map Int) (String, Maybe String)
leftJoin = do
    firstName <- firstNames
    lastName  <- optional lastNames
    return (firstName, lastName)

… evaluates to:

Defaultable
    (fromList
        [ (0, ("Gabriella",Just "Gonzalez"))
        , (1, ("Oscar"    ,Nothing        ))
        , (2, ("Edgar"    ,Just "Codd"    ))
        ]
    )
    Nothing

… which is analogous to this SQL left join:

> SELECT firstNames.id, firstName, lastName
>     FROM firstNames LEFT JOIN lastNames on firstNames.id = lastNames.id;
id | firstName | lastName
---+-----------+---------
0  | Gabriella | Gonzalez
1  | Oscar     |
2  | Edgar     | Codd

Since Haskell is a more fully-featured language than SQL, we can do more sophisticated things more easily than in SQL. For example, the following three-way join with some post-processing logic is much easier to express in Haskell than SQL:

display :: String -> Maybe String -> String -> String
display firstName Nothing handle =
    firstName <> ": @" <> handle
display firstName (Just lastName) handle =
    firstName <> " " <> lastName <> ": @" <> handle

interestingJoin :: Defaultable (Map Int) String
interestingJoin = do
    firstName <- firstNames
    lastName  <- optional lastNames
    handle    <- handles
    return (display firstName lastName handle)

… which evaluates to:

Defaultable
    (fromList
        [ (0, "Gabriella Gonzalez: @GabriellaG439")
        , (1, "Oscar: @posco"                     )
        ]
    )
    Nothing

The Defaultable type constructor

The central data type exported by the package is the Defaultable type constructor, which has the following simple definition:

data Defaultable map value = Defaultable (map value) (Maybe value)

Here the map type parameter can be any Map-like type that includes the type of the key. For example, a typical instantiation of the Defaultable type constructor might be Defaultable (Map key) value or Defaultable IntMap value.

The first field of the type is the actual map that you want to wrap in order to get an Applicative and Alternative instance. The second field is an optional default value stored alongside the map that can be returned if a lookup does not find a matching key.

The default value is not required (it can be Nothing), but that default value is what makes the Applicative instance work. Specifically, without the ability to specify a default value there would be no way to implement pure for a Map-like type.

In case you’re curious, here is what the Applicative instance looks like:

instance (Apply map, forall a . Monoid (map a)) => Applicative (Defaultable map)
  where
    pure v = Defaultable mempty (pure v)

    Defaultable fMap fDefault <*> Defaultable xMap xDefault =
        Defaultable fxMap fxDefault
      where
        fxMap = (fMap <.> xMap) <> fFallback <> xFallback
          where
            fFallback =
                case fDefault of
                    Nothing -> mempty
                    Just f  -> fmap f xMap

            xFallback =
                case xDefault of
                    Nothing -> mempty
                    Just x  -> fmap ($ x) fMap

        fxDefault = fDefault <*> xDefault

The neat part of the above instance is the class constraint:

          ↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓
instance (Apply map, forall a . Monoid (map a)) => Applicative (Defaultable map)

The Defaultable type is set up in such a way that you can wrap any Map-like type that satisfies that constraint (which is basically all of them) and get a law-abiding Applicative instance (See the Appendix for a proof of the Applicative laws).

In particular, this constraint makes use of the QuantifiedConstraints language extension introduced in GHC 8.6. Without that instance then we wouldn’t be able to generalize this type to wrap arbitrary Maps and we’d have to hard-code the package to work with a specific Map like Data.Map.Map.

The Defaultable type also implements Alternative, too, although that instance is much simpler:

instance (Apply map, forall a . Monoid (map a)) => Alternative (Defaultable map) where
    empty = Defaultable mempty empty

    Defaultable lMap lDefault <|> Defaultable rMap rDefault =
        Defaultable (lMap <> rMap) (lDefault <|> rDefault)

This instance is only possible because the Defaultable type constructor doesn’t require the default value to be present. If the default value were required then we could not sensibly define empty.

Prior art

I was surprised that something like this didn’t already exist on Hackage. The closest package I could find was this one:

However, that wasn’t exactly what I wanted, because it requires the default value to be present. That means that you can’t implement an Alternative instance for the TMap type from that package and you therefore can’t do things like left/right/outer joins as I mentioned above.

Also, more generally, sometimes you want a Map to have an Applicative instance without having to specify a default value. Requiring the default to always be present is not necessary to implement Applicative.

The other issue I had with that package is that it’s hard-coded to use Data.Map.Map under the hood, whereas I wanted an API that could be used in conjunction with any Map-like type.

Conclusion

The idea for this package originated from a LambdaConf presentation I gave a while ago where I brainstormed what a good “data science” ecosystem for Haskell might look like:

I sat on this idea for years without publishing anything to Hackage because my original vision was a bit too ambitious and included much more than just an Applicative Map type. However, recently I needed this Applicative Map type, so I settled for publishing a narrower and more focused package to Hackage.

The personal use case I have in mind for this package is no longer data science, but I hope that people interested in building a data science ecosystem for Haskell consider using this package as a building block since I believe it is well-suited for that purpose.

Appendix - Proof of the Applicative laws

These proofs require a few additional assumptions about the interaction between the Apply and Monoid constraint on the map type parameter to Defaultable. These assumptions hold for Map-like types.

The first assumption is that fmap is a Monoid homomorphism:

fmap f mempty = mempty

fmap f (x <> y) = fmap f x <> fmap f y

The second assumption is that f <.> is a Monoid homorphism:

f <.> mempty = mempty

f <.> (x <> y) = (f <.> x) <> (f <.> y)

The final assumption is specific to maps, which is:

-- Given:
mf :: map (a -> b)
mx :: map a
kf :: (a -> b) -> c
kx :: a -> c

  (mf <.> mx) <> fmap kf mf <> fmap kx mx
= (mf <.> mx) <> fmap kx mx <> fmap kf mf

The intuition here is if that map is a Map-like type constructor then we can think of those three expressions as having a set of keys associated with them, such that:

-- Given:
keys :: map a -> Set key

keys (mf <.> mx) = keys (fmap kf mf) `intersection` keys (fmap kx mx)

So normally the following equality would not be true:

  fmap kf mf <> fmap kx mx
= fmap kx mx <> fmap kf mf

… because the result would change if there was a key collision. Then the order in which we union (<>) the two maps would change the result.

However, if you union yet another map (mf <.> mx) that shadows the colliding keys then result remains the same.

The proof below uses that assumption a bit less formally by just noting that we can commute a union operation if there is a downstream union operation that would shadow any colliding keys that might differ.

Proof of identity law
pure id <*> v

-- pure v = Defaultable mempty (pure v)
= Defaultable mempty (pure id) <*> v

-- Expand: v = Defaultable xMap xDefault
= Defaultable mempty (pure id) <*> Defaultable xMap xDefault

-- Definition of (<*>)
= Defaultable fxMap fxDefault
  where
    fxMap = (mempty <.> xMap) <> fFallback <> xFallback
      where
        fFallback =
            case pure id of
                Nothing -> mempty
                Just f  -> fmap f xMap

        xFallback =
            case xDefault of
                Nothing -> mempty
                Just x  -> fmap ($ x) mempty

    fxDefault = pure id <*> xDefault

-- mempty <.> xMap = mempty
= Defaultable fxMap fxDefault
  where
    fxMap = mempty <> fFallback <> xFallback
      where
        fFallback =
            case pure id of
                Nothing -> mempty
                Just f  -> fmap f xMap

        xFallback =
            case xDefault of
                Nothing -> mempty
                Just x  -> fmap ($ x) mempty

    fxDefault = pure id <*> xDefault

-- Simplify `case pure id of …`
= Defaultable fxMap fxDefault
  where
    fxMap = mempty <> fFallback <> xFallback
      where
        fFallback = fmap id xMap

        xFallback =
            case xDefault of
                Nothing -> mempty
                Just x  -> fmap ($ x) mempty

    fxDefault = pure id <*> xDefault

-- fmap id x = x
= Defaultable fxMap fxDefault
  where
    fxMap = mempty <> fFallback <> xFallback
      where
        fFallback = xMap

        xFallback =
            case xDefault of
                Nothing -> mempty
                Just x  -> fmap ($ x) mempty

    fxDefault = pure id <*> xDefault

-- fmap f mempty = mempty
= Defaultable fxMap fxDefault
  where
    fxMap = mempty < >fFallback <> xFallback
      where
        fFallback = xMap

        xFallback =
            case xDefault of
                Nothing -> mempty
                Just x  -> mempty

    fxDefault = pure id <*> xDefault

-- pure id <*> v = v
= Defaultable fxMap fxDefault
  where
    fxMap = mempty <> fFallback <> xFallback
      where
        fFallback = xMap

        xFallback =
            case xDefault of
                Nothing -> mempty
                Just x  -> mempty

    fxDefault = xDefault

-- Simplify
= Defaultable fxMap fxDefault
  where
    fxMap = mempty <> xMap <> mempty

    fxDefault = xDefault

-- x <> mempty = x
-- mempty <> x = x
= Defaultable fxMap fxDefault
  where
    fxMap = xMap

    fxDefault = xDefault

-- Simplify
= Defaultable xMap xDefault

-- Contract: v = Defaultable xMap xDefault
= v
Proof of the composition law
pure (.) <*> u <*> v <*> w

-- Expand:
-- u = Defaultable uMap uDefault
-- v = Defaultable vMap vDefault
-- w = Defaultable wMap wDefault
=       pure (.)
    <*> Defaultable uMap uDefault
    <*> Defaultable vMap vDefault
    <*> Defaultable wMap wDefault

-- pure v = Defaultable mempty (pure v)
=       Defaultable mempty (pure (.))
    <*> Defaultable uMap uDefault
    <*> Defaultable vMap vDefault
    <*> Defaultable wMap wDefault

… before continuing, it’s easiest to prove all eight possible combinations of:

  • uDefault is pure u or empty
  • vDefault is pure v or empty
  • wDefault is pure w or empty

To avoid lots of repetition, I’ll only prove the most difficult case (where all defaults are present), since the other proofs are essentially subsets of that proof where some subterms disappear because they become mempty.

Case:

  • uDefault = pure u
  • vDefault = pure v
  • wDefault = pure w
=       Defaultable mempty (pure (.))
    <*> Defaultable uMap (pure u)
    <*> Defaultable vMap (pure v)
    <*> Defaultable wMap (pure w)

-- Definition of (<*>)
=       (Defaultable cuMap cuDefault
          where
            cuMap = (mempty <.> uMap) <> fmap (.) uMap <> fmap ($ u) mempty

            cuDefault = pure (.) <*> pure u
        )
    <*> Defaultable vMap (pure v)
    <*> Defaultable wMap (pure w)

-- mempty <.> x = mempty
=       (Defaultable cuMap cuDefault
          where
            cuMap = mempty <> fmap (.) uMap <> fmap ($ u) mempty

            cuDefault = pure (.) <*> pure u
        )
    <*> Defaultable vMap (pure v)
    <*> Defaultable wMap (pure w)

-- fmap f mempty = mempty
=       (Defaultable cuMap cuDefault
          where
            cuMap = mempty <> fmap (.) uMap <> mempty

            cuDefault = pure (.) <*> pure u
        )
    <*> Defaultable vMap (pure v)
    <*> Defaultable wMap (pure w)

-- pure f <*> pure x = pure (f x)
=       (Defaultable cuMap cuDefault
          where
            cuMap = mempty <> fmap (.) uMap <> mempty

            cuDefault = pure ((.) u)
        )
    <*> Defaultable vMap (pure v)
    <*> Defaultable wMap (pure w)

-- x <> mempty = x
-- mempty <> x = x
=       (Defaultable cuMap cuDefault
          where
            cuMap = fmap (.) uMap

            cuDefault = pure ((.) u)
        )
    <*> Defaultable vMap (pure v)
    <*> Defaultable wMap (pure w)

-- Simplify
=       (Defaultable (fmap (.) uMap) (pure (u .)))
    <*> Defaultable vMap (pure v)
    <*> Defaultable wMap (pure w)

-- Definition of (<*>)
=       (Defaultable cuvMap cuvDefault
          where
            cuvMap =
                    (fmap (.) uMap <.> vMap)
                <>  fmap (u .) vMap
                <>  fmap ($ v) (fmap (.) uMap)

            cuvDefault = pure (u .) <*> pure v
        )
    <*> Defaultable wMap (pure w)

-- fmap f (fmap g x) = fmap (f . g) x
=       (Defaultable cuvMap cuvDefault
          where
            cuvMap =
                    (fmap (.) uMap <.> vMap)
                <>  fmap (u .) vMap
                <>  fmap (. v) uMap

            cuvDefault = pure (u .) <*> pure v
        )
    <*> Defaultable wMap (pure w)

-- ((.) u) = \v -> u . v
=       (Defaultable cuvMap cuvDefault
          where
            cuvMap =
                    (fmap (.) uMap <.> vMap)
                <>  fmap (u .) vMap
                <>  fmap (. v) uMap

            cuvDefault = pure (u .) <*> pure v
        )
    <*> Defaultable wMap (pure w)

-- pure f <*> pure x = pure (f x)
=       (Defaultable cuvMap cuvDefault
          where
            cuvMap =
                    (fmap (.) uMap <.> vMap)
                <>  fmap (u .) vMap
                <>  fmap (. v) uMap

            cuvDefault = pure (u . v)
        )
    <*> Defaultable wMap (pure w)

-- Definition of (<*>)
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap = (cuvMap <.> wMap) <> fmap (u . v) wMap <> fmap ($ w) cuvMap 
      where
        cuvMap =
                (fmap (.) uMap <.> vMap)
            <>  fmap (u .) vMap
            <>  fmap (. v) uMap

    cuvwDefault = pure (u . v) <*> pure v

-- (f <> g) <.> x = (f <.> x) <> (g <.> x)
-- fmap f (x <> y) = fmap f x <> fmap f y
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (fmap (.) uMap <.> vMap <.> wMap)
        <>  (fmap (u .) vMap <.> wMap)
        <>  (fmap (. v) uMap <.> wMap)
        <>  fmap (u . v) wMap
        <>  fmap ($ w) (fmap (.) uMap <.> vMap)
        <>  fmap ($ w) (fmap (u .) vMap)
        <>  fmap ($ w) (fmap (. v) uMap)

    cuvwDefault = pure (u . v) <*> pure w

-- pure f <*> pure x = pure (f x)
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (fmap (.) uMap <.> vMap <.> wMap)
        <>  (fmap (u .) vMap <.> wMap)
        <>  (fmap (. v) uMap <.> wMap)
        <>  fmap (u . v) wMap
        <>  fmap ($ w) (fmap (.) uMap <.> vMap)
        <>  fmap ($ w) (fmap (u .) vMap)
        <>  fmap ($ w) (fmap (. v) uMap)

    cuvwDefault = pure (u (v w))

-- fmap (.) u <.> v <.> w = u <.> (v <.> w)
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  (fmap (u .) vMap <.> wMap)
        <>  (fmap (. v) uMap <.> wMap)
        <>  fmap (u . v) wMap
        <>  fmap ($ w) (fmap (.) uMap <.> vMap)
        <>  fmap ($ w) (fmap (u .) vMap)
        <>  fmap ($ w) (fmap (. v) uMap)

    cuvwDefault = pure (u (v w))

-- fmap f (x <.> y) = fmap (f .) x <.> y
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  fmap u (vMap <.> wMap)
        <>  (fmap (. v) uMap <.> wMap)
        <>  fmap (u . v) wMap
        <>  fmap ($ w) (fmap (.) uMap <.> vMap)
        <>  fmap ($ w) (fmap (u .) vMap)
        <>  fmap ($ w) (fmap (. v) uMap)

    cuvwDefault = pure (u (v w))

-- x <.> fmap f y = fmap (. f) x <.> y
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  fmap u (vMap <.> wMap)
        <>  (uMap <.> fmap v wMap)
        <>  fmap (u . v) wMap
        <>  fmap ($ w) (fmap (.) uMap <.> vMap)
        <>  fmap ($ w) (fmap (u .) vMap)
        <>  fmap ($ w) (fmap (. v) uMap)

    cuvwDefault = pure (u (v w))

-- fmap f (x <.> y) = fmap (f .) x <.> y
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  fmap u (vMap <.> wMap)
        <>  (uMap <.> fmap v wMap)
        <>  fmap (u . v) wMap
        <>  (fmap (($ w) .) (fmap (.) uMap) <.> vMap)
        <>  fmap ($ w) (fmap (u .) vMap)
        <>  fmap ($ w) (fmap (. v) uMap)

    cuvwDefault = pure (u (v w))

-- fmap f (fmap g x) = fmap (f . g) x
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  fmap u (vMap <.> wMap)
        <>  (uMap <.> fmap v wMap)
        <>  fmap (u . v) wMap
        <>  (fmap ((($ w) .) . (.)) uMap <.> vMap)
        <>  fmap ($ w) (fmap (u .) vMap)
        <>  fmap ($ w) (fmap (. v) uMap)

    cuvwDefault = pure (u (v w))

-- ((($ w) .) . (.))
-- = \u -> (($ w) .) ((.) u)
-- = \u -> (($ w) .) (u .)
-- = \u -> ($ w) . (u .)
-- = \u v -> ($ w) ((u .) v)
-- = \u v -> ($ w) (u . v)
-- = \u v -> (u . v) w
-- = \u v -> u (v w)
-- = \u v -> u (($ w) v)
-- = \u -> u . ($ w)
-- = (. ($ w))
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  fmap u (vMap <.> wMap)
        <>  (uMap <.> fmap v wMap)
        <>  fmap (u . v) wMap
        <>  (fmap (. ($ w)) uMap <.> vMap)
        <>  fmap ($ w) (fmap (u .) vMap)
        <>  fmap ($ w) (fmap (. v) uMap)

    cuvwDefault = pure (u (v w))

-- x <.> (f <$> y) = (. f) <$> x <.> y
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  fmap u (vMap <.> wMap)
        <>  (uMap <.> fmap v wMap)
        <>  fmap (u . v) wMap
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap ($ w) (fmap (u .) vMap)
        <>  fmap ($ w) (fmap (. v) uMap)

    cuvwDefault = pure (u (v w))

-- fmap f (fmap g x) = fmap (f . g) w
-- (f . g) = \x -> f (g x)
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  fmap u (vMap <.> wMap)
        <>  (uMap <.> fmap v wMap)
        <>  fmap (\w -> u (v w)) wMap
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap (\v -> u (v w)) vMap
        <>  fmap (\u -> u (v w)) uMap

    cuvwDefault = pure (u (v w))

-- `fmap (\w -> u (v w)) wMap <> (uMap <.> fmap ($ w) vMap)` commutes because
-- the colliding keys are shadowed by `(uMap <.> (vMap <.> wMap))`
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  fmap u (vMap <.> wMap)
        <>  (uMap <.> fmap v wMap)
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap (\w -> u (v w)) wMap
        <>  fmap (\v -> u (v w)) vMap
        <>  fmap (\u -> u (v w)) uMap

    cuvwDefault = pure (u (v w))

-- `fmap u (vMap <.> wMap) <> (uMap <.> fmap v wMap)` commutes because the
-- colliding keys are sahdowed by `(uMap <.> (vMap <.> wMap))`
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  (uMap <.> fmap v wMap)
        <>  fmap u (vMap <.> wMap)
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap (\w -> u (v w)) wMap
        <>  fmap (\v -> u (v w)) vMap
        <>  fmap (\u -> u (v w)) uMap

    cuvwDefault = pure (u (v w))

-- `fmap u (vMap <.> wMap) <> (uMap <.> fmap ($ w) vMap)` commutes because the
-- colliding keys are sahdowed by `(uMap <.> (vMap <.> wMap))`
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  (uMap <.> fmap v wMap)
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap u (vMap <.> wMap)
        <>  fmap (\w -> u (v w)) wMap
        <>  fmap (\v -> u (v w)) vMap
        <>  fmap (\u -> u (v w)) uMap

    cuvwDefault = pure (u (v w))

-- \w -> u (v w) = u . v
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  (uMap <.> (fmap v wMap)
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap u (vMap <.> wMap)
        <>  fmap (u . v) wMap)
        <>  fmap (\v -> u (v w)) vMap
        <>  fmap (\u -> u (v w)) uMap

    cuvwDefault = pure (u (v w))

-- fmap f (fmap g x) = fmap (f . g) x, in reverse
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  (uMap <.> (fmap v wMap)
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap u (vMap <.> wMap)
        <>  fmap u (fmap v wMap)
        <>  fmap (\v -> u (v w)) vMap
        <>  fmap (\u -> u (v w)) uMap

    cuvwDefault = pure (u (v w))

-- \v -> u (v w)
-- = \v -> u (($ w) v)
-- = u . ($ w)
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  (uMap <.> (fmap v wMap)
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap u (vMap <.> wMap)
        <>  fmap u (fmap v wMap)
        <>  fmap (u . ($ w)) vMap
        <>  fmap (\u -> u (v w)) uMap

    cuvwDefault = pure (u (v w))

-- fmap f (fmap g x) = fmap (f . g) x, in reverse
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  (uMap <.> (fmap v wMap)
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap u (vMap <.> wMap)
        <>  fmap u (fmap v wMap)
        <>  fmap u (fmap ($ w) vMap)
        <>  fmap (\u -> u (v w)) uMap

    cuvwDefault = pure (u (v w))

-- \f -> f x = ($ x)
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  (uMap <.> (fmap v wMap)
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap u (vMap <.> wMap)
        <>  fmap u (fmap v wMap)
        <>  fmap u (fmap ($ w) vMap)
        <>  fmap ($ (v w)) uMap

    cuvwDefault = pure (u (v w))

-- f <.> (x <> y) = (f <.> x) <> (f <.> y), in reverse
-- fmap f (x <> y) = fmap f x <> fmap f y, in reverse
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap = (uMap <.> vwMap) <> fmap u vwMap <> fmap ($ (v w)) uMap
      where
        vwMap = (vMap <.> wMap) <> fmap v wMap <> fmap ($ w) vMap

    cuvwDefault = pure (u (v w))

-- pure f <*> pure x = pure (f x), in reverse
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap = (uMap <.> vwMap) <> fmap u vwMap <> fmap ($ (v w)) uMap
      where
        vwMap = (vMap <.> wMap) <> fmap v wMap <> fmap ($ w) vMap

    cuvwDefault = pure u <*> pure (v w)

-- Definition of (<*>), in reverse
=   (   Defaultable uMap (pure u)
    <*> (Defaultable vwMap vwDefault
          where
            vwMap = (vMap <.> wMap) <> fmap v wMap <> fmap ($ w) vMap

            vwDefault = pure (v w)
        )
    )

-- pure f <*> pure x = pure (f x), in reverse
=   (   Defaultable uMap (pure u)
    <*> (Defaultable vwMap vwDefault
          where
            vwMap = (vMap <.> wMap) <> fmap v wMap <> fmap ($ w) vMap 

            vwDefault = pure v <*> pure w
        )
    )

-- Definition of (<*>), in reverse
=   (   Defaultable uMap (pure u)
    <*> (   Defaultable vMap (pure v)
        <*> Defaultable wMap (pure w)
        )
    )

-- Contract:
-- u = Defaultable uMap uDefault
-- v = Defaultable vMap vDefault
-- w = Defaultable wMap wDefault
= u <*> (v <*> w)
Proof of homomorphism law
pure f <*> pure x

-- pure v = Defaultable mempty (pure v)
= Defaultable mempty (pure f) <*> Defaultable mempty (pure x)

-- Definition of (<*>)
= Defaultable fxMap fxDefault
  where
    fxMap =  (mempty <.> mempty) <> fmap f mempty <> fmap ($ x) mempty

    fxDefault = pure f <*> pure x

-- fmap f mempty = mempty
= Defaultable fxMap fxDefault
  where
    fxMap = (mempty <.> mempty) <> mempty <> mempty

    fxDefault = pure f <*> pure x

-- mempty <.> x = mempty
= Defaultable fxMap fxDefault
  where
    fxMap = mempty <> mempty <> mempty

    fxDefault = pure f <*> pure x

-- mempty <> x = x
= Defaultable fxMap fxDefault
  where
    fxMap = mempty

    fxDefault = pure f <*> pure x

-- pure f <*> pure x = pure (f x)
= Defaultable fxMap fxDefault
  where
    fxMap = mempty

    fxDefault = pure (f x)

-- Simplify
= Defaultable mempty (pure (f x))

-- pure v = Defaultable mempty (pure v), in reverse
= pure (f x)
Proof of interchange law
u <*> pure y

-- pure v = Defaultable mempty (pure v)
= u <*> Defaultable mempty (pure y)

-- Expand: u = Defaultable uMap uDefault
= Defaultable uMap uDefault <*> Defaultable mempty (pure y)

-- Definition of (<*>)
= Defaultable uyMap uyDefault
  where
    uyMap = (uMap <.> mempty) <> uFallback <> fmap ($ y) uMap
      where
        uFallback =
            case uDefault of
                Nothing -> mempty
                Just u  -> fmap y mempty

    uyDefault = uDefault <*> pure y

-- fmap f mempty = mempty
= Defaultable uyMap uyDefault
  where
    uyMap = (uMap <.> mempty) <> uFallback <> fmap ($ y) uMap
      where
        uFallback =
            case uDefault of
                Nothing -> mempty
                Just u  -> mempty

    uyDefault = uDefault <*> pure y

-- Simplify `case uDefault of …`
= Defaultable uyMap uyDefault
  where
    uyMap = (uMap <.> mempty) <> uFallback <> fmap ($ y) uMap
      where
        uFallback = mempty

    uyDefault = uDefault <*> pure y

-- f <.> mempty = mempty
= Defaultable uyMap uyDefault
  where
    uyMap = mempty <> uFallback <> fmap ($ y) uMap
      where
        uFallback = mempty

    uyDefault = uDefault <*> pure y

-- mempty <> x = x
= Defaultable uyMap uyDefault
  where
    uyMap = fmap ($ y) uMap

    uyDefault = uDefault <*> pure y

-- u <*> pure y = pure ($ y) <*> u
= Defaultable uyMap uyDefault
  where
    uyMap = fmap ($ y) uMap

    uyDefault = pure ($ y) <*> uDefault

-- pure f <*> x = fmap f x
= Defaultable uyMap uyDefault
  where
    uyMap = fmap ($ y) uMap

    uyDefault = fmap ($ y) uDefault

-- Definition of `fmap`, in reverse
= fmap ($ y) (Defaultable uMap uDefault)

-- Contract: u = Defaultable uMap uDefault
= fmap ($ y) u

-- pure f <*> x = fmap f x, in reverse
= pure ($ y) <*> u