Technology

03 typeof Derivation

Author Photo

Johannes Kirschbauer

· 10 min read
Thumbnail

Derivation

Seeking the Ideal Type Abstraction for the Derivation Type in Nix

In the vast realm of Nix, understanding the intricacies of the Derivation type is paramount. Not only does it unlock insights into the workings of the build system, but it also provides clarity on how such a system can be expressed through a type lens. The journey of encapsulating the essence of the Derivation type is akin to a quest – seeking the right type abstraction.

Why is Type Abstraction Critical?

Abstraction, in the context of type systems, is a potent mechanism. It allows us to distill the essence of a construct, presenting only its most vital attributes and behaviors. By omitting extraneous details, we’re able to focus on what truly matters. And when it comes to type abstraction, this act of condensation and simplification isn’t just a matter of convenience—it’s a necessity.

In my perspective, type abstraction isn’t merely about making things simpler. It’s about capturing the heart and soul of a concept, bringing forward its most salient features, and presenting them in a manner that is both comprehensible and actionable.

The Challenge with Derivation

The Derivation type in Nix is no straightforward entity. It’s woven with nuances and intricacies that make it both intriguing and challenging. Finding the right abstraction for it is not about trimming down its complexities, but rather, understanding these complexities and determining the best way to represent them.

In subsequent sections, I plan to dive deeper into the attributes of the Derivation type, exploring potential abstractions, and assessing their suitability.

Alright, let’s delve deeper into this intricacy within Nix.

The Hidden Layers of Abstraction: Understanding builtins.derivation in Nix

For those deeply immersed in Nix, the name builtins.derivation might ring familiar. However, there’s a nuanced detail to be observed – builtins.derivation isn’t actually a primary operation (primop). Instead, it’s a mere shadow, a wrapper around the foundational builtins.derivationStrict.

Why Don’t We See derivationStrict at all?

A valid question arises: If builtins.derivationStrict is the core function, why is it that we seldom see it being called directly?

Within the vast ecosystem of nixpkgs and many other Nix frameworks, what is predominantly used is mkDerivation. Think of mkDerivation as an opinionated façade. It provides an interface that’s more tailored, streamlined, and imbued with conventions that make it the de facto choice for most use cases.

In fact derivationStrict doesn’t return something that could be passed to the build plane in nix.

Something like the following is not ‘buildable’ by nix.

nix-build

let
  pkgs = import <nixpkgs> {};
in
  builtins.derivationStrict {
    name = "Simple-package";
    system = "x86_64-linux";
    builder = "${pkgs.bash}/bin/bash";
    outputs = ["out"];
    args = ["-c" "echo pkg > $out"];
  }

The secret lies in the returned type of derivationStrict which is not something detected buildableby nix. Where the return type of derivation will be detected as something that can be built.

So where and what is the difference?

Peeling Back the Layers: From derivationStrict to derivation

Let’s dive deep on an exploration, starting with the most fundamental layer of abstraction.

  1. The Foundation - derivationStrict: It’s the raw core function of any nix build; It writes the drv file and pre-calculates the store path of all ouputs; A drv-build plan is an exact build plan, which will reproduce exact same results if given the same inputs. However it lacks the ability to execute the build.

  2. The Middle Layer - derivation: Recognizing the intricacies of derivationStrict, Nix introduced derivation as a needed wrapper around derivation strict. It encapsulates derivationStrict and enhances it to make it ‘buildable’ by the nix build plane.

  3. The User-Friendly Facade - mkDerivation: Climbing one layer up, we encounter mkDerivation. Infused with conventions and designed for broader appeal, it offers a balance between power and usability. It’s no wonder that this becomes the go-to choice for many in the Nix world.

As we continue this exploration, it becomes evident how the multi-layered architecture in Nix, as epitomized by the journey from derivationStrict to mkDerivation, offers both flexibility and usability. Each layer serves a distinct purpose and together, they enrich the Nix ecosystem.

Dive deep

The following code block is the actual implementation of builtins.derivation by the time of this writing. And can be found here: https://github.com/NixOS/nix/blob/master/src/libexpr/primops/derivation.nix

/* This is the implementation of the ‘derivation’ builtin function.
   It's actually a wrapper around the ‘derivationStrict’ primop. */

drvAttrs @ { outputs ? [ "out" ], ... }:

let

  strict = derivationStrict drvAttrs;

  outputsList = map outputToAttrListElement outputs;

  commonAttrs = drvAttrs // (builtins.listToAttrs outputsList) //
    { all = map (x: x.value) outputsList;
      inherit drvAttrs;
    };

  outputToAttrListElement = outputName:
    { name = outputName;
      value = commonAttrs // {
        outPath = builtins.getAttr outputName strict;
        drvPath = strict.drvPath;
        type = "derivation";
        inherit outputName;
      };
    };


in (builtins.head outputsList).value

Decoding the ‘Derivation’ in Nixpkgs

In the Nix universe, the term “Derivation” pops up frequently, almost ubiquitously. At the heart of Nix’s functionality, a derivation represents a build action. But when we examine the ecosystem, it seems like multiple entities use the name “Derivation” to refer to different functions or types. Let’s delve into this and uncover the mystery behind “Derivation.”

Different Flavors of “Derivation”

toDerivation :: Path -> Derivation

This suggests a function that transforms a path into a derivation. It operates at a more foundational level, working directly with paths, which are core to Nix’s store mechanism.

builtins.derivation :: { ... } -> Derivation

This is a builtin Nix function that produces a derivation from a set of attributes. While it’s a powerful and essential operation, it isn’t always used directly, primarily because of its raw nature.

stdenv.mkDerivation :: { ... } -> Derivation

Part of the standard environment (stdenv) toolkit in Nix, mkDerivation is an abstraction over the builtins version, tailored for general usage. It incorporates various conventions and patterns, making it the popular choice when defining packages in nixpkgs.

So, Are They All the Same?

In essence, all the above return a “Derivation.” However, the process of creating that derivation, the level of abstraction, and the inputs differ. At a high level, they all encapsulate a build action in Nix, but the nuances lie in their implementation and use cases.

Expressing the Type of “Derivation”

Here lies the crux. How do we define the type of a Derivation? Given Nix’s dynamic nature, strict type definitions like in Haskell or TypeScript aren’t readily apparent. However, conceptually, a Derivation in Nix can be thought of as:

  • A promise or blueprint of a build action.
  • A record of dependencies, sources, and build instructions.
  • An entity that, when realized, produces a concrete build output in the Nix store.

However, pinning down a strict type definition in the same vein as traditional statically typed languages might be challenging due to Nix’s dynamic nature. It’s more about understanding the conceptual role of a Derivation and how different functions and methods in Nix contribute to creating and using them.

In summary, while different functions in Nix might produce “Derivations,” understanding the nuances and levels of abstraction can help you effectively harness the power of Nix’s core concepts.

Typeof Derivation

To express the type of Derivation we first need a way to express types in this post i will use the syntax of type system that i introduced here in a proposal for unifying the comment syntax for types.

Lets have a look at the type of the primop derivationStrict

This type signature will be the core of the next abstraction layer.

derivationStrict :: {
    name :: String;
    outputs :: String;
    builder :: String;
    system :: String;
} -> {
    drvPath :: String;
    ${output} :: String;
}

derivationStrict returns at least the drvPath which is set to a nix/store/<path>.drv where the drv file is located at. Also it holds one attribute for every space seperated output.

Like

outputs = "out doc lib"

would return

{
    drvPath="nix/store/<hash>.drv";
    out="nix/store/<hash>";
    doc="nix/store/<hash>";
    lib="nix/store/<hash>";
}

Lets have a look at the type of the builtins.Derivation now:

We do this by adding type annotations to every expression during construction of the internal builtins.derivation function

I soon found out that Derivation is a recursive, dependent type.

It is recursive, as it has itself in the all attribute and every entry declared in outputs is a Derivation itself.

And it is dependent because its final type depends on the value of input attributes.

If the following is to much information overload for you, go right to the end of this post, where you can find the final type.

/* This is the implementation of the ‘derivation’ builtin function.
   It's actually a wrapper around the ‘derivationStrict’ primop. */


/*
    Type:
        {
            outputs :: ? [ String ];
            ${additionalArg} :: a;
        }
*/
drvAttrs @ { outputs ? [ "out" ], ... }:

let

  /*
    Type:
        {
            name :: String;
            outputs :: ? String;
            builder :: String;
            system :: String;
            ${additionalArg} :: a;
        } -> {
            drvPath :: String;
            ${output} :: String;
        }
  */
  strict = derivationStrict drvAttrs;
  
    /*
        outputs :: [String] is transformed using the outputToAttrListElement
        Type:
        [ 
            {
                name :: String;
                value :: {
                    outPath :: String;
                    drvPath :: String;
                    type :: "derivation";
                    ${outputName} :: String;
                    ${commonAttrs} :: Any;
                }
            } 
        ] 
    */
  outputsList = map outputToAttrListElement outputs;
  

  /*
    {
        name :: String;
        outputs :: ? String;
        builder :: String;
        system :: String;
        ${additionalArg} :: String;
    } // {
        ${name} :: Derivation
    } // {
        all :: [ Derivation ]
        drvAttrs :: {
            outputs :: [ String ];
            ${additionalArg} :: a;
        }
    }
  */
  commonAttrs = drvAttrs // (builtins.listToAttrs outputsList) //
    { all = map (x: x.value) outputsList;
      inherit drvAttrs;
    };

    /*
        String -> {
            name :: String
            value :: {
                outPath :: String;
                drvPath :: String;
                type :: "derivation";
                outputName :: String;
                ${commonAttrs} :: Any;
            }
        }
    */
  outputToAttrListElement = outputName:
    { name = outputName;
      value = commonAttrs // {
        outPath = builtins.getAttr outputName strict;
        drvPath = strict.drvPath;
        type = "derivation";
        inherit outputName;
      };
    };

/*
 This returns the value attribute o the first element 
 in the outputsList 
 which I found to be a recursive expression:

 commonAttrs = 
    drvAttrs // 
    outputsList.asAttrSet // 
    {all= valuesOf outputsList; drvAttrs=drvAttrs;}

 outputsList = 
    map outputs over -> outputName: 
        [
            { name=outputName; value=commonAttrs//{...}; }
        ]

*/
in (builtins.head outputsList).value

So i find the type of builtins.derivation:

# As returned by builtins.derivation
Derivation :: {
  all :: [ Derivation ];
  builder :: String;
  drvAttrs :: {
      builder :: String; 
      name :: String;
      outputs :: [ output :: String ]; 
      system :: String;
      ${additionalArg} :: a;
  }
  drvPath :: String;
  name :: String;
  outPath :: String;
  outputName :: String;
  outputs :: [ output :: String];
  system :: String;
  type :: "derivation";
  ${output} :: Derivation;
  ${additionalArg} :: a;
};

This type cannot be seen as a standalone type because it is a dependent type. It depends on the input attributes and of the input values of builtins.derivation

Final Type

To get the final type we also need to resolve the type constraints for the type variable a that was introduced here.

a :: String

actually derivation accepts more types here: -> everything that can be coerced into string

I also added the special args keyword which is one of the possible additionalArg but it is passed as cli argument to the builder.

Every other additionalArg is passed as env variable instead.

With the type syntax proposed here

it is possible to write the following expression for the type of derivation

using the let in syntax that we all know and love. 😁

let 
    Derivation :: {
        all :: [ Derivation ];
        builder :: String;
        drvAttrs :: {
            builder :: String; 
            name :: String;
            outputs :: [ output@String ]; 
            system :: String;
            args :: [ String ]?;
            ${additionalArg} :: String;
        }
        drvPath :: String;
        name :: String;
        outPath :: String;
        outputName :: String;
        outputs :: [ output@String ];
        system :: String;
        type :: "derivation";
        args :: [ String ]?;
        ${output} :: Derivation;
        ${additionalArg} :: String?;
    };
in
    {
        name :: String;
        outputs :: [ output@String ]?;
        builder :: String;
        system :: String;
        args :: [ String ] ?;
        ${additionalArg} :: String?;
    } -> Derivation
#builtins.derivation

Adding more attributes to the builtins.derivation call adds those as environment variables.

The logic can be seen below:

# additionalArg
# e.g. derivation {... more="foo"; } 
export more='foo'
# common PATHs
export HOME='/homeless-shelter'
export NIX_BUILD_CORES='0'
export NIX_BUILD_TOP='/build'
export NIX_LOG_FD='2'
export NIX_STORE='/nix/store'
export PATH='/path-not-set'
export PWD='/build'
export SHLVL='1'
export TEMP='/build'
export TEMPDIR='/build'
export TERM='xterm-256color'
export TMP='/build'
export TMPDIR='/build'
export builder='/nix/store/a600x16bxc1qks8rbgalj5vaixgbxdhj-builder.sh'
export name='simple'
export out='/nix/store/y5n7k4hachqzih2i9pwi4wkkd9i97swl-simple'
export system='x86_64-linux'

Thanks for reading and have good time. I hope this was helpful and interesting

Edit: refactor the type expression to be conform to the proposed type language

#nix#derivation#type