Monday, October 24, 2022

How to correctly cache build-time dependencies using Nix


Professional Nix users often create a shared cache of Nix build products so that they can reuse build products created by continuous integration (CI). For example, CI might build Nix products for each main development branch of their project or even for every pull request and it would be nice if those build products could be shared with all developers via a cache.

However, uploading build products to a cache is a little non-trivial if you don’t already know the “best” solution, which is the subject of this post.

The solution described in this post is:

  • Simple

    It only takes a few lines of Bash code because we use the Nix command-line interface idiomatically

  • Efficient

    It is very cheap to compute which build products to upload and requires no additional builds nor an exorbitant amount of disk space

  • Accurate

    It uploads the build products that most people would intuitively want to upload

Note: Throughout this post I will be using the newer Nix command-line interface and flakes, which requires either adding this line to your nix.conf file:

extra-experimental-features = nix-command flakes

… and restarting your Nix daemon (if you have a multi-user Nix installation), or alternatively adding these flags to the beginning of all nix commands throughout this post:

$ nix --option extra-experimental-features 'nix-command flakes'

Wrong solution #0

As a running example, suppose that our CI builds a top-level build product using a command like this:

$ nix build .#example

The naïve way to upload that to the cache would be:

$ nix store sign --key-file "${KEY_FILE}" --recursive .#example

$ nix copy --to s3:// .#example

Note: You will need to generate a KEY_FILE using the nix-store --generate-binary-cache-key command if you haven’t already. For more details, see the following documentation from the manual:

Click to expand to see the documentation
Operation --generate-binary-cache-key
       nix-store --generate-binary-cache-key key-name secret-key-file

       This command generates an Ed25519 key pair (
       that can be used to create a signed binary cache. It takes three
       mandatory parameters:

       1.     A key name, such as, that is used to look up
              keys on the client when it verifies signatures. It can be
              anything, but it’s suggested to use the host name of your cache
              (e.g. with a suffix denoting the number of the
              key (to be incremented every time you need to revoke a key).

       2.     The file name where the secret key is to be stored.

       3.     The file name where the public key is to be stored.

That seems like a perfectly reasonable thing to do, right? However, the problem with that is that it is incomplete, meaning that the cache would still be missing several useful build products that developers would expect to be there.

Specifically, the above command only copies the “run-time” dependencies of our build product whereas most developers expect the cache to also include “build-time” dependencies, and I’ll explain the distinction between the two.

Run-time vs. Build-time

Many paths in the /nix/store are not “valid” in isolation. They typically depend on other paths within the /nix/store.

For example, suppose that I build the GNU hello package, like this:

$ nix build nixpkgs#hello

I can query all of the other paths within the /nix/store that the hello package transitively depends on at run-time using this command:

$ nix-store --query --requisites ./result

… or I can print the same information in tree form like this:

$ nix-store --query --tree ./result

On my macOS machine, it has two run-time dependencies (other than itself) within the /nix/store: libobjc and apple-framework-CoreFoundation-11.0.

Note: there might be other run-time dependencies, because I believe Nixpkgs support for macOS requires some impure system dependencies, but I’m not an expert on this so I could be wrong.

These are called “run-time” dependencies because we cannot run our hello executable without them.

Nix prevents us from getting into situations where a /nix/store path is missing its run-time dependencies. For example, if I were to nix copy the hello build product to any cache, then Nix would perform the following steps, in order:

  • Copy libobjc to the cache

    … since that has no dependencies

  • Copy apple-framework-CoreFoundation to the cache

    … since its libobjc dependency is now satisfied within the cache

  • Copy hello to the cache

    … since its apple-framework-CoreFoundation dependency is now satisfied within the cache

However, Nix also has a separate notion of “build-time” dependencies, which are dependencies that we need to in order to build the hello package.

Note: The reason we’re interested in build-time dependencies for our project is that we want developers to be able to rebuild the project if they make any changes to the source code. If we were to only cache the run-time dependencies of our project that wouldn’t cache the development environment that developers need.

In order to query these dependencies I need to first get the “derivation” (.drv file) for hello:

$ DERIVATION="$(nix path-info --derivation nixpkgs#hello)"

$ declare -p DERIVATION
typeset DERIVATION=/nix/store/4a78f0s4p5h2sbcrrzayl5xas2i7zq1m-hello-2.12.1.drv

You can think of a derivation file as a build recipe that contains instructions for how to build the corresponding build product (the hello package in this case).

I can query the direct dependencies of that derivation using this command:

$ nix-store --query --references "${DERIVATION}"

Many of these dependencies are themselves derivations (.drv files), meaning that they represent other packages that Nix might have to build or fetch from a cache.

Note: the .drv files are actually not the build-time dependencies, but rather the instructions for building them. You can convert any .drv file to the matching product it is supposed to build using the same nix build command, like this:

$ nix build /nix/store/labgzlb16svs1z7z9a6f49b5zi8hb11s-bash-5.1-p16.drv

Does that mean that these build-time dependencies are on our machine if we built nixpkgs#hello? Not necessarily. In fact, in all likelihood the nixpkgs#hello build was cached, meaning that nix build nixpkgs#hello only downloaded hello and its run-time dependencies and no build-time dependencies were required nor installed by Nix.

However, I could in principle force Nix to build the hello package instead of downloading it from a cache, like this:

$ nix build nixpkgs#hello --rebuild

… and that would download the direct build-time dependencies of the hello package in order to rebuild the package.

Wrong solution #1

By this point you might suppose that you have enough information to come up with a better set of /nix/store paths to cache. Your solution might look like this:

  • Get the derivation for the top-level build product

  • Get the direct build-time dependencies of that derivation

  • Build the top-level build product and its direct build-time dependencies

  • Cache the top-level build product and its direct build-time dependencies

In other words, something like this Nix code:

$ DERIVATION="$(nix path-info --derivation "${BUILD}")"

$ DEPENDENCIES=($(nix-store --query --references "${DERIVATION}"))

$ nix build "${BUILD}" "${DEPENDENCIES[@]}"

$ nix store sign --key-file "${KEY_FILE}" --recursive "${BUILD}" "${DEPENDENCIES[@]}"

$ nix copy --to "${CACHE}" "${BUILD}" "${DEPENDENCIES[@]}"

This is better, but still not good enough!

The problem with this solution is that it only works well if your dependencies never change and you only modify your top-level project. If you upgrade or patch any of your direct build-time dependencies then you need to have their build-time dependencies cached so that you can quickly rebuild them.

In fact, going two layers deep is still not enough; in practice you can’t easily anticipate in advance how deep in the build-time dependency tree you might need to patch or upgrade things. For example, you might need to patch or upgrade your compiler, which is really deep in your build-time dependency tree.

Wrong solution #2

Okay, so maybe we can try to build and cache all of our build-time dependencies?

Wrong again. There are way too many of them. You can query them by replacing --references with --requisites and you’ll a giant list of results, even for “small” packages. For example:

$ DERIVATION=$(nix path-info --derivation nixpkgs#hello)

$ nix-store --query --requisites "${DERIVATION}"
 🌺 500+ derivations later 🌺 …
Click to expand and see the full list of build-time dependencies

The above command not only lists the build-time dependencies for the hello package, but also their transitive build-time dependencies. In other words, these are all the derivations needed to build the hello package “from scratch” in the absence of any cache products. We can see the complete tree of build-time dependencies like this:

$ nix-store --query --tree "${DERIVATION}"
   │   ├───/nix/store/3glray2y14jpk1h6i599py7jdn3j2vns-mkdir.drv
   │   ├───/nix/store/50ql5q0raqkcydmpi6wqvnhs9hpdgg5f-cpio.drv
   │   ├───/nix/store/81xahsrhpn9mbaslgi5sz7gsqra747d4-unpack-bootstrap-tools->
   │   ├───/nix/store/>
   │   ├───/nix/store/gxzl4vmccqj89yh7kz62frkxzgdpkxmp-sh.drv
   │   └───/nix/store/pjbpvdy0gais8nc4sj3kwpniq8mgkb42-bzip2.drv
   │   ├───/nix/store/7kcayxwk8khycxw1agmcyfm9vpsqpw4s-bootstrap-tools.drv [..>
   │   ├───/nix/store/nbxwxwqwcr9rrmxb6gb532f18102815x-bootstrap-stage0-stdenv>
   │   │   ├───/nix/store/
   │   │   ├───/nix/store/
   │   │   ├───/nix/store/7kcayxwk8khycxw1agmcyfm9vpsqpw4s-bootstrap-tools.drv>
   │   │   ├───/nix/store/
   │   │   ├───/nix/store/cickvswrvann041nqxb0rxilc46svw1n-prune-libtool-files>
   │   │   ├───/nix/store/
   │   │   ├───/nix/store/
   │   │   ├───/nix/store/
   │   │   ├───/nix/store/
   │   │   ├───/nix/store/
   │   │   ├───/nix/store/kxw6q8v6isaqjm702d71n2421cxamq68-make-symlinks-relat>
   │   │   ├───/nix/store/m54bmrhj6fqz8nds5zcj97w9s9bckc9v-compress-man-pages.>
   │   │   ├───/nix/store/ngg1cv31c8c7bcm2n8ww4g06nq7s4zhm-set-source-date-epo>
   │   │   └───/nix/store/wlwcf1nw2b21m4gghj70hbg1v7x53ld8-reproducible-builds>
   │   ├───/nix/store/i65va14cylqc74y80ksgnrsaixk39mmh-mirrors-list.drv
   │   │   ├───/nix/store/7kcayxwk8khycxw1agmcyfm9vpsqpw4s-bootstrap-tools.drv>
   │   │   ├───/nix/store/nbxwxwqwcr9rrmxb6gb532f18102815x-bootstrap-stage0-st>
   │   │   └───/nix/store/
   │   └───/nix/store/

If we were to build and cache all of these build-time dependencies then our local /nix/store and cache would explode in size. Also, we do not need to do this because there is a better solution …

Correct solution

The solution that provides the best value is to cache all transitive build-time dependencies that are present within the current /nix/store after building the top-level build product. In other words, don’t bother to predict which build-time dependencies we need; instead, empirically infer which ones to cache based on which ones Nix installed and used along the way.

This is not only more accurate, but it’s also more efficient: we don’t need to build or download anything new because we’re only caching things we already locally installed.

As a matter of fact, the nix-store command already supports this use case quite well. If you consult the documentation for the --requisites flag, you’ll find this gem:

       • --requisites; -R
         Prints out the closure (../ of the store path paths.

         This query has one option:

         • --include-outputs Also include the existing output paths of store
           derivations, and their closures.

         This query can be used to implement various kinds of deployment. A
         source deployment is obtained by distributing the closure of a store
         derivation. A binary deployment is obtained by distributing the closure
         of an output path. A cache deployment (combined source/binary
         deployment, including binaries of build-time-only dependencies) is
         obtained by distributing the closure of a store derivation and
         specifying the option --include-outputs.

We’re specifically interested in a “cache deployment”, so we’re going to do exactly what the documentation says and use the --include-outputs flag in conjunction with the --requisites flag. In other words, the --include-outputs flag was expressly created for this use case!

So here is the simplest, but least robust, version of the script for computing the set of build-time dependencies to cache, as a Bash array:

$ # Continue reading before using this code; there's a more robust version later

$ # Optional: Perform the build if you haven't already
$ nix build "${BUILD}"

$ DERIVATION="$(nix path-info --derivation "${BUILD}")"

$ DEPENDENCIES=($(nix-store --query --requisites --include-outputs "${DERIVATION}"))

$ nix store sign --key-file "${KEY_FILE}" --recursive "${DEPENDENCIES[@]}"

$ nix copy --to "${CACHE}" "${DEPENDENCIES[@]}"

The above code is simple and clear enough to illustrate the idea, but we’re going to make a few adjustments to make this code more robust.

Specifically, we’re going to:

  • Change the code to support an array of build targets

    i.e. BUILDS instead of BUILD

  • Use mapfile instead of ($(…)) to create intermediate arrays

    See: SC2207

  • Use xargs to handle command line length limits

… which gives us:

$ # Optional: Perform the build if you haven't already
$ echo "${BUILDS[@]}" | xargs nix build

$ mapfile -t DERIVATIONS < <(echo "${BUILDS[@]}" | xargs nix path-info --derivation)

$ mapfile -t DEPENDENCIES < <(echo "${DERIVATIONS[@]}" | xargs nix-store --query --requisites --include-outputs)

$ echo "${DEPENDENCIES[@]}" | xargs nix store sign --key-file "${KEY_FILE}" --recursive

$ echo "${DEPENDENCIES[@]}" | xargs nix copy --to "${CACHE}"

… where you:

  • replace BUILDS with a Bash array containing what you want to build

    e.g. .#example or nixpkgs#hello

  • replace CACHE with whatever store you use as your cache

    e.g. s3://

  • replace KEY_FILE with the path to your cache signing key


That last script is the pedantically robust way to do this in Bash if you want to be super paranoid. The above script might not work in other shells, but hopefully this post was sufficiently clear that you can adapt the script to your needs.

If I made any mistakes in the above post, let me know and I can fix them.

Thursday, October 20, 2022

What does "isomorphic" mean (in Haskell)?

What does "isomorphic" mean (in Haskell)

Sometimes you’ll hear someone describe two things as being “isomorphic” to one another and I wanted to explain what that means.

You might have already guessed that “isomorphic” is a synonym for “equivalent”, and that would have been a pretty good guess. Really, the main difference between the two words is that “isomorphic” has a more precise and more general definition than “equivalent”.

In this post I will introduce a more precise definition of “isomorphic”, using Haskell code. This definition won’t be the fully general definition, but I still hope to give you some taste of how “isomorphic” can denote something more than just “equivalent”.

The simple version

The simplest and least general definition of “isomorphic” (in Haskell) is:

Two types, A, and B, are isomorphic if there exist two functions, forward and backward of the following types:

forward :: A -> B

backward :: B -> A

… such that the following two equations (which I will refer to as the “isomorphism laws”) are true:

forward . backward = id

backward . forward = id

id here is the identity function from Haskell’s Prelude, defined like this:

id :: a -> a
id x = x

… and (.) is the function composition operator (also from Haskell’s Prelude), defined like this:

(.) :: (b -> c) -> (a -> b) -> (a -> c)
(f . g) x = f (g x)

According to the above definition, the types Bool -> a and (a, a) are isomorphic, because we can define two functions:

forward :: (Bool -> a) -> (a, a)
forward function = (function False, function True)

backward :: (a, a) -> (Bool -> a)
backward (first, second) False = first
backward (first, second) True  = second

… and we can prove that those two functions satisfy the isomorphism laws using equational reasoning.

Proof of the isomorphism laws (click to expand)

Here’s the proof of the first isomorphism law:

forward . backward

-- (f . g) = \x -> f (g x)
-- … where:
-- f = forward
-- g = backward
= \x -> forward (backward x)

-- x = (first, second)
= \(first, second) -> forward (backward (first, second))

-- forward function = (function False, function True)
= \(first, second) ->
    (backward (first, second) False, backward (first, second) True)

-- backward (first, second) False = first
-- backward (first, second) True  = second
= \(first, second) -> (first, second)

-- x = (first, second)
-- … in reverse
= \x -> x

-- id x = x
-- … in reverse
= \x -> id x

-- η-reduction
= id

… and here is the proof of the second isomorphism law:

backward . forward

-- (f . g) = \x -> f (g x)
-- … where:
-- f = backward
-- g = forward
-- x = function
= \function -> backward (forward function)

-- forward function = (function False, function True)
= \function -> backward (function False, function True)

-- η-expand
= \function bool -> backward (function False, function True) bool

-- There are two possible cases:
-- Case #0: bool = False
-- Case #1: bool = True

-- Proof for case #0: bool = False
  = \function bool -> backward (function False, function True) False

  -- backward (first, second) False = first
  -- … where:
  -- first  = function False
  -- second = function True
  = \function bool -> function False

  -- bool = False
  -- … in reverse
  = \function bool -> function bool

  -- η-reduction
  = \function -> function

  -- id x = x
  -- … in reverse
  = \function -> id function

  -- η-reduction
  = id

-- Proof for case #1: bool = True
  = \function bool -> backward (function False, function True) True

  -- backward (first, second) True = second
  -- … where:
  -- first  = function False
  -- second = function True
  = \function bool -> function True

  -- b = True
  -- … in reverse
  = \function bool -> function bool

  -- η-reduction
  = \function -> function

  -- id x = x
  -- … in reverse
  = \function -> id function

  -- η-reduction
  = id

We’ll use the notation A ≅ B as a short-hand for “A is isomorphic to B”, so we can also write:

Bool -> a ≅ (a, a)

Whenever we declare that two types are isomorphic we need to actually specify what the forward and backward conversion functions are and prove that they satisfy isomorphism laws. The existence of forward and backward functions of the correct input and output types is not enough to establish that the two types are isomorphic.

For example, suppose we changed the definition of forward to:

forward :: (Bool -> a) -> (a, a)
forward function = (function True, function False)

Then forward . backward and backward . forward would still type-check and have the right type, but they would no longer be equal to id.

In other words, when discussing isomorphic types, it’s technically not enough that the two types are equivalent. The way in which they are equivalent matters, too, if we want to be pedantic. In practice, though, if there’s only one way to implement the two conversion functions then people won’t bother to explicitly specify them.

The reason why this is important is because an isomorphism also gives us an explicit way to convert between the two types. We're not just declaring that they're equivalent, but we're spelling out exactly how to transform each type into the other type, which is very useful!

More examples

Let’s speedrun through a few more examples of isomorphic types, which all parallel the rules of arithmetic:

-- 0 + a = a
Either Void a ≅ a

-- a + (b + c) = (a + b) + c
Either a (Either b c) = Either (Either a b) c

-- 1 × a = a
((), a) ≅ a

-- a × (b × c) = (a × b) × c
(a, (b, c)) ≅ ((a, b), c)

-- 0 × a = 0
(Void, a) ≅ Void

-- a × (b + c) = (a × b) + (a × c)
(a, Either b c) ≅ Either (a, b) (a, c)

-- a ^ 1 = a
() -> a ≅ a

-- a ^ 0 = 1
Void -> a ≅ ()

-- (c ^ b) ^ a = (c ^ a) ^ b
a -> b -> c ≅ b -> a -> c

-- (c ^ b) ^ a = c ^ (a × b)
a -> b -> c ≅ (a, b) -> c

Exercise: implement the forward and backward functions for some of the above types and prove the isomorphism laws for each pair of functions. It will probably be very tedious to prove all of the above examples, so pick the ones that interest you the most.

Intermediate tricks

This section will introduce some more advanced tricks for proving that two types are isomorphic.

First, let’s start with a few ground rules for working with all isomorphisms:

  • Reflexivity: a ≅ a

  • Symmetry: If a ≅ b then b ≅ a

  • Transitivity: If a ≅ b and b ≅ c then a ≅ c

Now let’s get into some Haskell-specific rules:

a newtype in Haskell is isomorphic to the underlying type if the newtype constructor is public.

For example, if we were to define:

newtype Name = Name { getName :: String }

… then Name and String would be isomorphic (Name ≅ String), where:

forward :: Name -> String
forward = getName

backward :: String -> Name
backward = Name

One such newtype that shows up pretty often when reasoning about isomorphic types is the Identity type constructor from Data.Functor.Identity:

newtype Identity a = Identity { runIdentity :: a }

… where Identity a ≅ a.

To see why Identity is useful, consider the following two types:

newtype State s a = State { runState :: s -> (a, s) }

newtype StateT s m a = StateT { runStateT :: s -> m (a, s) }

The latter newtype is from the transformers package, which is how we layer on the “state” effect within a monad transformer stack. If you don’t understand what that means, that’s okay; it’s not that relevant to the point.

However, the transformers package doesn’t define State as above. Instead, the transformers package defines State like this:

type State s = StateT s Identity

The latter type synonym definition for State is equivalent (“isomorphic”) to the newtype definition for State I provided above. In order to prove that though I’ll need to distinguish between the two State type constructors, so I’ll use a numeric subscript to distinguish them:

import Data.Functor.Identity (Identity)

newtype State₀ s a = State₀ { runState :: s -> (a, s) }

newtype StateT s m a = StateT { runStateT :: s -> m (a, s) }

type State₁ s = StateT s Identity

… and then we can prove that State₀ is isomorphic to State₁ like this:

  • State₀ s a ≅ s -> (a, s)

    … because the State₀ newtype is isomorphic to the underlying type

  • s -> (a, s) ≅ s -> Identity (a, s)

    … because the Identity newtype is isomorphic to the underlying type

  • s -> Identity (a, s) ≅ StateT s Identity a

    … because the StateT newtype is isomorphic to the underlying type

  • StateT s Identity a = State₁ s a

    … because of how the State₁ type synonym is defined.

Therefore, by transitivity, we can conclude:

  • State₀ s a ≅ State₁ s a

Okay, now let’s introduce an extremely useful rule related to isomorphic types:

If f is a Functor then forall r . (a -> r) -> f r is isomorphic to f a.

Or in other words:

Functor f => (forall r . (a -> r) -> f r) ≅ f a

… and here are the two conversion functions:

{-# LANGUAGE RankNTypes #-}

forward :: Functor f => (forall r . (a -> r) -> f r) -> f a
forward f = f id

backward :: Functor f => f a -> (forall r . (a -> r) -> f r)
backward fa k = fmap k fa

This is essentially the Yoneda lemma in Haskell form, which is actually a bit tricky to prove. If you don’t believe me, try proving the isomorphism laws for the above forward and backward functions and see how far you get. It’s much easier to rely on the fact that someone else already did the hard work of proving those isomorphism laws for us.

Here’s a concrete example of the Yoneda lemma in action. Suppose that I want to prove that there is only one implementation of the identity function, id. I can do so by proving that the type of the identity function (forall a . a -> a) is isomorphic to the () type (a type inhabited by exactly one value):

(forall a . a -> a) ≅ ()

Here’s how you prove that by chaining together several isomorphic types:

  (forall a . a -> a)
  -- a ≅ () -> a
≅ (forall a . (() -> a) -> a)
  -- a ≅ Identity a
≅ (forall a . (() -> a) -> Identity a)
  -- ✨ Yoneda lemma (where f = Identity) ✨
Identity ()
≅ ()

… so since the () type is inhabited by exactly one value (the () term) and the () type is isomorphic to the type of id, then there is exactly one way to implement id (which is id x = x).

Note: To be totally pedantic, there is exactly one way to implement id “up to isomorphism”. This is how we say that there might be several syntactically different ways of implementing id, such as:

id x = x

id y = y

id = \x -> x

id x = y
    y = x

… but all of those ways of implementing id are isomorphic to one another (in a slightly different sense that I have not covered), so there is essentially only one way of implementing id.

Similarly, we can prove that there are exactly two ways to implement a function of type forall a . a -> a -> a by showing that such a type is isomorphic to Bool (a type inhabited by exactly two values):

  (forall a . a -> a -> a)
  -- a -> b -> c ≅ (a, b) -> c
≅ (forall a . (a, a) -> a)
  -- (a, a) ≅ Bool -> a
≅ (forall a . (Bool -> a) -> a)
  -- a ≅ Identity a
≅ (forall a . (Bool -> a) -> Identity a)
  -- ✨ Yoneda lemma (where f = Identity) ✨
Identity Bool

… and in case you’re curious, here are the only two possible ways to implement that type (up to isomorphism):

{-# LANGUAGE ExplicitForAll #-}

false :: forall a . a -> a -> a
false f t = f

true :: forall a . a -> a -> a
true f t = t

Here’s one last example of using the Yoneda lemma to prove that:

(forall r . (a -> r) -> r) ≅ a

… which you can prove like this:

  (forall r . (a -> r) -> r)
  -- Identity r ≅ r
≅ (forall r . (a -> r) -> Identity r)
  -- ✨ Yoneda lemma (where f = Identity) ✨
Identity a
≅ a

Exercise: Prove that these two types are isomorphic:

(forall r . (b -> r) -> (a -> r)) ≅ a -> b
Solution (click to expand)
  (forall r . (b -> r) -> (a -> r))
  -- a -> b -> c ≅ b -> a -> c
≅ (forall r . a -> (b -> r) -> r)
  -- r ≅ Identity r
≅ (forall r . a -> (b -> r) -> Identity r)
  -- ✨ Yoneda lemma (where f = Identity) ✨
≅ a -> Identity b
  -- Identity b ≅ b
≅ a -> b


So far we’ve only used the word “isomorphic” but there is a related word we should cover: “isomorphism”.

In Haskell, if the types A and B are “isomorphic” then an “isomorphism” between them is the corresponding pair of functions converting between them (i.e. forward and backward).

The easiest way to explain this is to actually define an isomorphism type in Haskell:

data Isomorphism a b = Isomorphism
    { forward  :: a -> b
    , backward :: b -> a

For example:

exampleIsomorphism :: Isomorphism ((a, b) -> c) (a -> b -> c)
exampleIsomorphism = Isomorphism{ forward = curry, backward = uncurry }

However, this is not the only way we can encode an isomorphism in Haskell. For example, the lens package has an Iso type which can also represent an isomorphism:

import Control.Lens (Iso', iso)

exampleIso :: Iso' ((a, b) -> c) (a -> b -> c)
exampleIso = iso curry uncurry

These two types are equivalent. In fact, you might even say they are … isomorphic 👀.

{-# LANGUAGE NamedFieldPuns #-}

import Control.Lens (AnIso', Iso', cloneIso, iso, review, view)

data Isomorphism a b = Isomorphism
    { forward  :: a -> b
    , backward :: b -> a

-- | We have to use `AnIso'` here instead of `Iso'` for reasons I won't go into
isomorphismIsomorphism :: Isomorphism (Isomorphism a b) (AnIso' a b)
isomorphismIsomorphism = Isomorphism{ forward, backward }
    forward :: Isomorphism a b -> AnIso' a b
    forward (Isomorphism f b) = iso f b

    backward :: AnIso' a b -> Isomorphism a b
    backward iso =
            { forward  = view (cloneIso iso)
            , backward = review (cloneIso iso)

Generalized isomorphisms

I mentioned earlier that the isomorphism definition we began with was not the fully general definition. In this section we’ll slightly generalize the definition, while still sticking to something ergonomic to express within Haskell:

Two types, A, and B, are isomorphic if there exist two morphisms, forward and backward of the following types:

forward :: cat A B

backward :: cat B A

… such that cat is an instance of the Category type class and the following two equations (which I will refer to as the “isomorphism laws”) are true:

forward . backward = id

backward . forward = id

… where (.) and id are the methods of the Category type class and not necessarily the (.) and id from the Prelude.

This definition is based on the Category type class from the Control.Category module, which is defined like this:

class Category cat where
    -- | the identity morphism
    id :: cat a a

    -- | morphism composition
    (.) :: cat b c -> cat a b -> cat a c

… and all instance of the Category class must satisfy the following three “category laws”:

(f . g) . h = f . (g . h)

f . id = f

id . f = f

In other words, you can think of the Category class as generalizing our notion of functions to become “morphisms” so that we replace values of type a -> b (functions) with values of type cat a b (“morphisms”). When we generalize our notion of functions to morphisms then we can similarly generalize our notion of isomorphisms.

Of course, Haskell functions are one instance of this Category class:

instance Category (->) where
    id =

    (.) = (Prelude..)

… so if we take our more general definition of isomorphisms and replace cat with (->) then we get back the less general definition of isomorphisms that we started with.

However, things other than functions can be instances of this Category class, too. For example, “monadic” functions of type Monad m => a -> m b can implement Category, too, if we wrap them in a newtype:

import Control.Category (Category(..))
import Control.Monad ((<=<))

-- Note: This type and instance already exists in the `Control.Arrow` module
newtype Kleisli m a b = Kleisli{ runKleisli :: a -> m b }

instance Monad m => Category (Kleisli m) where
    id = Kleisli return

    Kleisli f . Kleisli g = Kleisli (f <=< g)

… and that satisfies the category laws because:

(f <=< g) <=< h = f <=< (g <=< h)

f <=< return = f

return <=< f = f

Fun fact: The above category laws for the Kleisli type constructor are isomorphic to the monad laws (in a different sense of the world "isomorphic" that I have not covered).

Once we begin to use Category instances other than functions we can begin to explore more interesting types of “morphisms” and “isomorphisms”. However, in order to do so we need to generalize our Isomorphism type like this:

data Isomorphism cat a b = Isomorphism
    { forward  :: cat a b
    , backward :: cat b a

… so that we can store morphisms that are not necessarily functions.

With that generalized Isomorphism type in hand we can now create a sample Isomorphism in a Kleisli Category:

import Data.Monoid (Sum(..))
import Control.Monad.Writer (Writer)

writerIsomorphism :: Isomorphism (Kleisli (Writer (Sum Integer))) () ()
writerIsomorphism = Isomorphism{ forward, backward }
    forward :: Kleisli (Writer (Sum Integer)) () ()
    forward = Kleisli (\_ -> tell (Sum 1))

    backward :: Kleisli (Writer (Sum Integer)) () ()
    backward = Kleisli (\_ -> tell (Sum (-1)))

Like before, we still require that:

forward . backward = id

backward . forward = id

… but in this case the (.) and id in these two isomorphism laws will be the ones for our Kleisli type instead of the ones for functions.

Proof of isomorphism laws (click to expand)

I’ll skip over several steps for this proof to highlight the relevant parts:

forward . backward

= Kleisli (\_ -> tell (Sum 1)) . Kleisli (\_ -> tell (Sum (-1)))

= Kleisli ((\_ -> tell (Sum 1)) <=< (\_ -> tell (Sum (-1))))

= Kleisli (\_ -> tell (Sum 0))

= Kleisli return

= id
The proof of backward . forward = id is essentially the same thing, except flipped.

Note our Isomorphism effectively says that the type () is isomorphic to the type () within this Kleisli (Writer (Sum Integer)) Category, which is not a very interesting conclusion. Rather, for this Isomorphism the (slightly more) interesting bit is in the “morphisms” (the forward and backward definitions), which are inverses of one another.

Here is one last example of a non-trivial Category instance with an example isomorphism:

import Prelude hiding ((.), id)

-- Note: This is not how the lens package works, but it's still a useful example
data Lens a b = Lens{ view :: a -> b, over :: (b -> b) -> (a -> a) }

instance Category Lens where
    id = Lens{ view = id, over = id }

    Lens{ view = viewL, over = overL } . Lens{ view = viewR, over = overR } =
        Lens{ view = viewL . viewR, over = overR . overL }

lensIsomorphism :: Isomorphism Lens Bool Bool
lensIsomorphism = Isomorphism{ forward, backward }
    forward :: Lens Bool Bool
    forward = Lens{ view = not, over = \f -> not . f . not }

    -- There is no rule that the two morphisms can't be the same
    backward :: Lens Bool Bool
    backward = forward

Again, it’s not very interesting to say that Bool is isomorphic to Bool, but it is more to note that the forward lens is essentially its own inverse.

There’s one last category I want to quickly mention, which is … Isomorphism!

Yes, the Isomorphism type we introduced is itself an instance of the Category class:

instance Category cat => Category (Isomorphism cat) where
    Isomorphism forwardL backwardL . Isomorphism forwardR backwardR =
        Isomorphism (forwardL . forwardR) (backwardR . backwardL)

    id = Isomorphism id id

You might even say that an “isomorphism” is a “morphism” in the above Category. An “iso”-“morphism”, if you will (where “iso” means “same”).

Furthermore, we can create an example Isomorphism in this Category of Isomorphisms:

nestedIsomorphism :: Isomorphism (Isomorphism (->)) Integer Integer
nestedIsomorphism =
        { forward  = Isomorphism{ forward = (+ 1), backward = subtract 1 }
        , backward = Isomorphism{ forward = subtract 1, backward = (+ 1) }

Okay, perhaps that’s going a bit too far, but I just wanted to end this post with a cute example of how you can keep chaining these ideas together in new ways.


In my experience, the more you train your ability to reason formally about isomorphisms the more you broaden your ability to recognize disparate things as equivalent and draw interesting connections between them.

For example, fluency with many common isomorphisms is a useful skill for API design because often there might be a way to take an API which is not very ergonomic and refactor it into an equivalent (isomorphic) API which is more ergonomic to use.