Type-systems in nix

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.

Type systems generally

In general nix has dynamic types, like python or javascript. This means the types are not written down and fixed like in other languages like in rust or c. The type will be determined at runtime and complex concerns like memory allocation are completely hidden from the developer.

Type systems can generally be classified into two subsections:

• Static Types
• Dynamic Types

Both type systems have different benefits and disadvantages.

But generally speaking people tend to build better software if they have access to static types. Or at least have the possibility to express types statically even in dynamic languages like with Type annotations in python or with Typescript in javascript.

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",
    ...
}

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