Technology

02 Type-systems in nix

Author Photo

Johannes Kirschbauer

· 5 min read
Thumbnail

About the existing type system

Generally there are different systems on types in nix.

The nix language is dynamically typed and only has internal types, which are present on the underlying language interpreter written in c++. A complete list of these types can be found here.

Like in many other languages there are Primitives like Integer or String, but also complex datatypes like List, Attrset or Derivation.

Those complex datatypes are related to each other, many of them can be thought of as special sub-types of attrset. One problem is, that no type rules or conventions about that relations exists.

Exploring Type Systems and Their Integration into the Nix Language

When diving into the world of programming languages, one of the foundational aspects to consider is the type system. The type system of a language determines how variables, function arguments, and return values are handled. As with most things in the tech world, there’s no one-size-fits-all solution, and the choice of type system often boils down to the problem domain and developer preference.

A Quick Look at Nix’s Type System

The Nix language, which forms the backbone of the Nix/NixOS ecosystem, uses a dynamic type system. If you’re familiar with languages like Python or JavaScript, you’d recognize this approach. In dynamic type systems, variable types aren’t predefined or fixed, as is the case in statically-typed languages like Rust or C. Instead, the types of variables are determined at runtime. This offers flexibility but may come with its own set of challenges.

Classifying Type Systems

Broadly speaking, type systems can be bucketed into two categories:

  • Static Types: In statically-typed languages, every variable’s type is defined at compile time. This allows for early error detection, making it easier to catch type-related issues before the code is executed.

  • Dynamic Types: In dynamically-typed languages, variable types are inferred at runtime. This provides flexibility in coding but can lead to runtime errors if there are mismatches in expected types.

Static vs. Dynamic: The Perpetual Debate

Both type systems come with their own sets of advantages and disadvantages. However, there’s an emerging consensus in the developer community. Many believe that access to static types—or at least the ability to express static types in inherently dynamic languages—leads to more robust software. This belief is supported by the rising popularity of tools like Type annotations in Python and TypeScript for JavaScript. These tools allow developers to harness the power of static types in languages that are traditionally dynamically typed.

nixos modules

It is possible to use nixos modules which are of the following format:

{
  # declaration of the 'interface'
  options = {
    # declarations, with dynamic type checking
  };

  # content of the module 'implementation'
  imports = [
    # paths to other modules
  ];
  config = {
    # option definitions
  };
}

With that format it is possible to specify (dynamic) types on the contents of a module. With types from this file

A simple interface declaration then looks like this:


options = {
  hardware.pulseaudio = {
    enable = mkOption {
      type = types.bool;
    };
  };
}

This is essentially a shortcut for common dynamic type checking. It also allows for automatic documentation generation, as the type attribute can be used to generate descriptions for the documentation.

Static typing in nix

There is no static typing in nix.

As nix is a dynamic language there are no static types in nix. If you’d like to add static types to nix, you have two options:

  1. Change the language paradigms to use static types.
  2. Add type annotations.

As it is very hard to re-implement the nix language a fast yet effective solution to the existing language would be to add type annotations.

doc-string type hints

Also nix has documentation strings that do document Example: and Type: within the source code of nixpkgs.

If you’d like to add Type annotations (like in python) you could start from that convention.

However it could also be possible to create a completely new type annotation system.

Annotation Systems

Some basic principles:

  • Type annotations start with the :: (double-colon)
  • Type annotations end with:
    • end-of-string on primitive types. Bool
    • enclosing parenthesis on complex types. ([{ -> }])
  • Type annotations are optional
  • Type annotations can appear everywhere in the code to increase readability.
  • Parsing and checking on Annotations can be done
    • from external tools
    • additional builtin functionality, such as e.g. nix check --types.

In the language itself

Within the nix language there could be special places for annotations carved out. Those type annotations can be safely ignored from the nix parser and don’t affect the execution of nix expressions. They are generally handled like comments but with special purposes.

Pro

  • Cleanest way
  • Doesn’t drift like comments would

Con

  • Requires changes in the nix parser

Example code

# typed primitive variables
 foo :: String = "bar";
 foo :: Bool = true;
 foo :: Int = 1;
 foo :: Number = 1.2 + 1;
 foo :: Path = ./path/to/file; 
 foo :: Derivation = mkDerivation {...};


# typed AttrSets 1
set :: { ${key} :: String } = {
  foo = "value must";
  bar = "always be";
  baz = "type string";
}

# typed AttrSets 2
set :: { package :: Derivation, ${key} :: String, internal :: "copy" } = {
  # 'package' is explizitly typed
  package = builtins.derivation {...}; 
  # all other entries are strings
  foo = "value sometimes";
  baz = "type string";
  # 'internal' is always that fixed string
  internal = "copy";
}

# typed lists

languages :: [String] = [
  "nix"
  "rust"
  "python"
];

Those types and rules how to use them must be invented and i have created a repository for that, where i collect those rules:

github:hsjobeki/nix-types

List of Types

Types are alway written in PascalCase, to visually separate them from variables.

Primitives

  • Any
  • Int
  • Float
  • Number
  • String
  • Bool
  • Path
  • Null

Complex

  • AttrSet {}
  • List []
  • Function ->

Built on top of that

  • Derivation
  • StorePath
  • Function

Any - type

The Any type is the union set of all types.

Containing all characteristics and allowing every operation on them.

Derivation - type

The Derivation type is a subset of the AttrSet type.

It could be an AttrSet that has very specific entries.

e.g.


Derivation :: {
    outPath :: StorePath,
    type :: "derivation",
    ...
}

See my other blogpost for the typeof derivation

StorePath - type

The StorePath type is just a subset of the Path type.

The StorePath from a type perspective is just an alias for Path there are really no assumptions, that would make it any different.

It may start with /nix/store/sha256-pname-version but the allowed Operations are all the same as on Path.

Thanks for reading so far.

More ideas are on my github repo here

#nix#type#noogle
← View all posts