Introduction

This is my (draft) writing to try to formalize type convention and formals for the nix language.

To support the convention utilize doc-comments.

Example:

{
  /**
    # Type

    ```
    mapAttrs :: ( String -> a -> b ) -> { ${name} :: a; } -> { ${name} :: b; }
    ```
  */
  mapAttrs = ...
}

Motivation

By specifying the syntax of the type section within nix this opens a wide range of possibilities.

• consistent function / API documentation. (I.e. used by noogle.dev)
• Type checking - whether you call a function with the expected types.
• Language Server (LSP) support - display inline or hover type signatures.
• Encourage Modular architectures, with well-defined and documented interfaces.
• Static type / correctness checking

Detailed implementation

I propose to formulate a strict type syntax. Be it used for doc-comments or maybe even integrated into the language itself.

Syntax follows nix

The syntax is mainly inspired and as close as possible to the Nix language. Everyone who knows Nix can easily learn the type-language for it. There are only very few modifications that are self-explaining and intuitive. While we could imagine a way more complex language, that allows expressing every last detailed relationship. I think it is more important to provide a good abstraction and find the right compromise between simplicity and expressiveness.

Formals

As the annotation references to exactly one expression. There is only one type expression possible

All notations are PascalCase

PascalCase with a starting uppercase letter. This is also in other languages a known convention for types or classes

Types MUST be chosen from the existing list

see primitives

Operators MUST be chosen from the existing list

see operators

explicit AttrSet and List keywords are PROHIBITED

See the correct usage here

complex types MUST include their members explicitly

There is no AttrSet and no List keyword.

explicit Any is PROHIBITED

Correct usage with type variables see here

Allowing arbitrary values within complex-types

It is possible to allow arbitrary values within complex types, but it requires an explicit statement.

There is no implicit any.

Type variables must be written in LOWERCASE to prevent confusion

They are used instead of the Any Keyword.

For Type bindings it is PROHIBITED to choose names from the reserved list

This will help to keep the code clean. Reduces complexity, resolves for shadowing and namespace conflicts, with global names.

Tokens

The following tokens do exist

Tokens removed

In contrast to the default nix language, some tokens do not exist and may even result in an error.

The following keywords do exist

Only the let .. in keywords are supported.

Keywords removed

As complexity is already quite high. It is considered best to not support the following keywords in the type language.

Reserved Types

All types are written in Uppercase by convention to visually distinguish them from variables and actual values.

Some composed types are handled as native types as well. They are well-defined internally but can be used natively in the type language.

_Internal context

Syntax

-- under construction --

The syntax very closely follows the Nix syntax to make writing types intuitive for Nix users. Although the language is inspired by Haskell, not every Nix user may be familiar with Haskell.

Legacy let

Did you know the legacy let? Don't bother it is legacy ^^ ;-). Legacy let is not supported by the type language. In general, every type is defined in a type expression.

e.g.

Int | Bool

is a type expression; - but also

let
Foo :: Int;
in
Foo | Bool

Those two examples contain essentially almost every rule for writing type expressions.

As shown in general there are two levels of type expression.

• Type-expression
• Simple Type-expression

The everything is a Type Expression but in certain places you can only write simple type expression. This behavior is not invented with the type language; it is derived from nix. Where the same principles apply.

For example Simple type expressions do not ally writing let ... in.

[ let T :: Int in T ]

is just NOT allowed. There are certain places within the syntax where you can only write simple expressions such as:

[ {SIMPLE} ] -> [ Int | String ]

Root Ident

Currently, there are many so-called root ident nodes.

Example:

    mapAttrs :: (String -> Any -> Any) -> AttrSet -> AttrSet

Types

This chapter clarifies all types.

To Pickup the overview more quickly they can be viewed in the following list.

Every decision and further specification are explained in the corresponding sub-chapters respectively.

List of all Types

Primitives

The Any type (upper boundary)

The Any type is often used to explicitly allow arbitrary values. However, the Any type is complex and doesn't add much value to a type system. Instead, we should use type variables whenever possible.

Interestingly there are two different Any types:

e.g. If we look at CUE-lang (which is also inspired by nix)

CUE defines the values bottom, or error, (denoted |) that is an instance of all types and top, or any, (denoted _) of which all types are an instance.

• TOP any all types are an instance of that. You can imagine it as the TOP-most set, that includes every type. But no value has that type.

• Bottom any which is an instance of all types. This is kind of the imaginary value that has the any type. Still, doesn't contain any value. Which could also be denoted: Never or Empty Type it is a type that is the subtype of any type.

The following is a nice quote from the Typescript world

The any type is so dangerous because it exists outside of the type tree. It is both a top and bottom type. Everything can be assigned to it and it can be assigned to everything else. ...

I think it might make most sense to define Any as TOP in our type system. This means it is the upper boundary of our type system. All types within the system are a subtype of Any.

Never (lower boundary)

I think it makes most sense to have a distinct Bottom type. Other type systems call this: Bottom any or Empty Type. This is the lower boundary of our type system. All types are a supertype of Never and that is true for all types that may eventualy exist in this type system.

The easiest way of thinking about Never is this example:

let
 # a -> Never
 f = x: abort "now";
 # Never <- f 42
 result = f 42;
in
 # result :: Never
 result

A function f that takes Any argument and since it aborts the evaluation it returns Never.

Never might need its own chapter since it requires understanding lazyness in the language to determine which expression returns never during evaluation.

The Bool type

As the Bool type can only have two values (true/false)

The following is the definition of the Bool type

Bool :: true | false

Complex

T, U, ...; are placeholders for any types, those MUST be specifically declared on usage

More details how to use complex types in the corresponding chapters

Composed

used operators are defined in the operators chapter

Primitives

Overview

The following primitive types have been identified.

All other types can be composed from them by using those and the operators.

Primitives

The Any type (upper boundary)

The Any type is often used to explicitly allow arbitrary values. However, the Any type is complex and doesn't add much value to a type system. Instead, we should use type variables whenever possible.

Interestingly there are two different Any types:

e.g. If we look at CUE-lang (which is also inspired by nix)

CUE defines the values bottom, or error, (denoted |) that is an instance of all types and top, or any, (denoted _) of which all types are an instance.

• TOP any all types are an instance of that. You can imagine it as the TOP-most set, that includes every type. But no value has that type.

• Bottom any which is an instance of all types. This is kind of the imaginary value that has the any type. Still, doesn't contain any value. Which could also be denoted: Never or Empty Type it is a type that is the subtype of any type.

The following is a nice quote from the Typescript world

The any type is so dangerous because it exists outside of the type tree. It is both a top and bottom type. Everything can be assigned to it and it can be assigned to everything else. ...

I think it might make most sense to define Any as TOP in our type system. This means it is the upper boundary of our type system. All types within the system are a subtype of Any.

Never (lower boundary)

I think it makes most sense to have a distinct Bottom type. Other type systems call this: Bottom any or Empty Type. This is the lower boundary of our type system. All types are a supertype of Never and that is true for all types that may eventualy exist in this type system.

The easiest way of thinking about Never is this example:

let
 # a -> Never
 f = x: abort "now";
 # Never <- f 42
 result = f 42;
in
 # result :: Never
 result

A function f that takes Any argument and since it aborts the evaluation it returns Never.

Never might need its own chapter since it requires understanding lazyness in the language to determine which expression returns never during evaluation.

The Bool type

As the Bool type can only have two values (true/false)

The following is the definition of the Bool type

Bool :: true | false

Complex

Overview

The following complex types have been identified.

All complex types can be composed from Any other types even from themselves by using those and the operators.

Complex

T, U, ...; are placeholders for any types, those MUST be specifically declared on usage

More details how to use complex types in the corresponding chapters

List

Abstract definition

Let [ a ] be a list where the elements of that list do not have any type constraints.

Then a List of a specific Type [ T ] is a list where all elements a fullfil the type constraint T

A list [] can contain no, one or multiple elements. (0...n)

However the List-type can only contain one simple type expression.

See syntax rules to learn what a simple type expression is.

Examples

list of string

[ String ]

list of string or bool

[ Number | Bool ]

-> see the | {or} operator defined here

empty list

[ ]

list of any attrSet

[ { ... } ]

AttrSet

Abstract

An AttrSet type can be thought of as just a list of pair of name and value.

• fst on pair of name and value yields the name.
• snd on pair of name and value yields the value.

Then AttrSet can be written as:

[Pair(name,value)]

when you reference a specific name on an AttrSet; You basically implicitly apply a filter or find operation on that list where the fst of the mapped entry equals the referenced name

For simplicity this is called a member name from now on, if that name exists.

Redefining some operators

::-operator within AttrSet contexts

The ::-operator maps the Type of its RHS over the Type on its LHS. It can take an Iterable or a single element on its LHS.

Within Type-declarations for AttrSets it is possible to declare an explicit member name of an AttrSet like this.

  {
    N :: T
  }

Then N is of type String and N becomes a member name of that AttrSet. The snd operation on the entry of N would yield a value of type T.

Introducing: [ N :: T ]-operator, which can only be used within AttrSet in member name fields.

The [ N :: T ]-operator maps over all member names of an AttrSet [N] and applies the type T to each member name N if not already done by explicit member__ declaration (see above).

When there are AttrSets with dynamic members it is possible to declare all those members at once with the [ N :: T ] and :: operator.

Then an AttrSet with list of dynamic members where each member-name N references a value of type V can be written as.

  {
    [ N :: T ] :: V
  }

Examples

  # member '.foo' references a value of type string
  # all other members `*` are of type string and each member reference value of any variable Type.
  {
    [ name :: String ] :: a,
    foo :: String
  }

  { foo :: a }

   {}

where the member names `[ N :: T ] are an empty list.

useful ${} Shortcut

${N} = [ N :: String ]

If we take into account that in AttrSets names (N) are always of type String the user can omit the String Keyword completely, and instead give only the names. N

That rule allows for intuitive usage of names within type definitions of an AttrSet

/*
type:
  packageMap :: {
    ${pname} :: {
      ${version} :: Derivation
    }
  }
*/
packageMap = {
  "gcc-utils" = {
    "1.2.3" = builtins.Derivation {...};
    };
  # ...
  };

Lambda

Abstract definition

A lambda is a function that takes exactly one argument and returns exactly one result.

It is denoted as follows:

a -> b

Where a is the argument and b is the returned result.

Then a typed lambda notation:

T -> G

Denotes that T is the type of argument a and G is the type of result b.

In lambda notations arguments do not have names like in e.g. AttrSet because they are positional arguments.

Examples

Lambda that takes a String and returns String

String -> String

Function that takes String and Number and finally returns String

String -> Number -> String

As lambdas can take only one argument, the return type of the first lambda expression is a lambda that takes the second argument and returns the final type.

Function that takes a function

(String -> String) -> [String] -> [String]

Sometimes parenthesis is necessary to clarify order of evaluation

The () Parenthesis operator is defined here

Operators

All Operators SHOULD be used with surrounding whitespace.

:: declares the type

The variable name on the LHS is declared to have the type on the RHS

e.g. name :: String

In attribute set contexts :: defines both the type of a and b as illustrated below.

def pair=λa.λb.λf.((f a) b)
<=>
{ "foo" = 1; }

typeOf { "foo" = 1; }
=>
{ String :: Int; } # Example type conversion may not closely represent the type conversion done by a real type engine.

def first p​=λa.λb.a

first { String :: Int; }
=>
String

def second p=λa.λb.b

second { String :: Int; }
=>
Int

() Parenthesis

Parenthesis to clarify order of type evaluation

e.g. ( a -> b ) | Bool

Precedence: (Highest)

; Separator for subsequent entries (like in AttrSet)

e.g. { foo :: Number; bar :: String }

Important: This is a required syntax rule! It terminates the type expression.

Currently this is very inconsistent in nixpkgs.

| syntactic or

syntactic Or can be used for composition or enums

Let T and U be different Types. Then the | operator evaluates to either T or U.

Sometimes within this paper | is written as {or}

This is only due to readability and not allowed in the real language

Precedence: 2

Triviality / special Cases

Any | a

Is always Any; Because any other type a must already be a subtype of any, due to the definition of Any.

b | Never

Is always b; Due to the definition of Never; b must be a supertype of Never.

Examples

Float | Int

( Number | Bool ) | Int

{ opt :: Int | String }

# lets say we want to create a type which can represent the type of both 'foo' and 'bar'
let
  /*
    Type:
      FooBar = Int | String

      foo :: FooBar
  */
  foo = 1;
  /*
    Type:
      bar :: FooBar
  */
  bar = "baz";

in
  # ....

& conjunction operator

TODO

Triviality / special Cases

Any & a

Is always a

b & Never

Is always Never

... - arbitrary input values

can only be used within an AttrSet to allow Any more name-value pairs.

... = ${rest} :: a within an AttrSet context

e.g.

/*
  Type: foo :: { bar :: a, ...} -> a
*/
Foo = {bar, ...}@inp:
#...

Precedence: None

// merge operator

syntactically merges Types of AttrSets

{ foo :: String } // { bar :: Number } => { foo :: String; bar :: Number }

{ foo :: String } // { ${names} :: a } => { foo :: String; ${names} :: a }

Overwrites occur like in the nix language itself

{ foo :: String } // { foo :: Number } => { foo :: Number }

Precedence: 3

-> arrow operator

Allows for lambda types

Precedence: 1

? optional arguments in an AttrSet

--e.g. { opt :: Int ? }

Note: The very end of type side contains the ? operator.

The reason for this is extendability. Initially the ?-Operator is introduced as Unary-operator, marking the entry type as optional. In future it will be desirable to use the ? as binary-operator to add default values on optional entries.

e.g.

{
  foo :: Int ? 1;
}

Precedence: None

Precedence

Precedence is just taken from the official nix operators. To make usage as intuitive as possible. However the type language only uses a tight subset of the operator available in nix.

-> see grammar

Type Variables

Abstract

As the explicit Any keyword is prohibited. Even there is no such Any type.

It is of course possible to construct the Any type and use it properly but in good type systems there is no need for that type.

The Any type is covered from Polymorphism with the usage of type variables.

Type variables can have any name but it is usually considered best practice to choose either letters from the latin alphabet or use meaningful names.

Type variables must be written in LOWERCASE to prevent confusion.

Examples

The following function signatures from nix and nixpkgs are written most clearly with type variables

builtins.map

( a -> b ) -> [a] -> [b]

builtins.catAttrs

String -> [ { ${name} :: a } ] -> [a]

lib.attrsets.attrByPath

[ String ] -> a -> { ${path} :: b } -> (a | b)

builtins.mapAttrs

(String -> a -> b) -> { ${name} :: a } -> { ${name} :: b }

builtins.sort

(a -> a -> Bool) -> [a] -> [a]

Namespaces

Type variables are currently the best way to properly use polymorphism in type signatures. But using them requires the underlying parser and the user need to understand some concepts like namespaces and shadowing.

This section orients itself on the Haskell type variables. See here for their rules

In nix we don't have the same syntax as haskell has but the basic principles and core concept will be adopted from the parser.

Bigger sets with nested type variables

sometime it is possible to have expressions, that contain multiple levels of nestings, where also different hierarchies of type variables must interact with each other.

{ foo :: a } -> {
  nestedFunction :: a -> b,
  bar :: ( b -> c ) -> [c] -> [b]
}

This seem a little complex now, because the parent function returns an AttrSet that includes function signatures using the same type variables as the outermost function itself.

There is actually a very strict and proven ruleset for that exact problem out there.

The Haskell Ruleset for scoped type variables

(see also above).

Type Variables with constraints

Sometime we have variable types in signatures, but cannot allow any type for the variable. Then we could construct a type and assign it like this.

  Foo = ( String | Path )
  Foo -> Foo 

This is already allowed syntax in the proposed type system. There are no additional changes that need to be made.

Sometimes there might be more than one expression necessary to express the type of a function.

Also this means that the annotated function might take a String or a Path, and also returns them. If that function takes a String it will return the same String type. Once Foo evaluates to type String every occurrence of Foo is then of type String.

Nix

The language fundamentals

It is very desireable to build a solid set of type signatures for the most basic operators in nix.

Those are:

• language syntax
• Operations
• Builtins

If those basic functionality from a type perspective of the language itself is clarified.

this opens a whole new spectrum of possibilities like type inference or type checking.

Operations

The official documentation about the operators in nix can be found here

🚧🚧🚧 This site is WIP

Official List

Type signatures

From a type perspective those operators can be seen as lambda functions. Every operator takes (one or more) arguments of a type and returns a type. The following list was created to clarify the type signatures.

Some operators take one or two arguments, they can either take them from left or right hand side.

Some formals

for simplicity this document follows these conventions:

• R is used as Right hand side type.
• L is used as Left hand side type.
• When using the proposed lambda notation, the first argument is always LHS and the second the RHS of the discussed operator.
• T,U,W are used as generic Type variables mostly do denote the resulting type, or types of free variables.
• a,b,... can be of any type. They are type variables.
• x is a functions input value
• y is a functions return value
• f, g, h are used to give names to functions.

'.' - Attribute selection

Usage of the (.) operator:

L must be an AttrSet, and R must be of type String

 L(.)R = L.R

Since attribute sets are defined as lists of pairs. The . operation simply finds the matching first pair and returns the second pair (which is the value). If the value doesn't exist it raises an Error in the value world which means it returns type Never in the type world.

 L(.)R = L -> R -> T
 L(.)R :: { ${name} :: a } -> String -> a | Never

If R itself contains an expression this must be parenthesized with the ( ) operator. This operator tells us to evaluate the expression in R before passing it to the (.) operator.

Examples:

 { "car" :: String; "bus" :: Int }.("car" | "bus")
 # Evaluates to
 String | Int

Attribute selection in conjunction with or

The or operator simply narrows out the Never type and instead returns a fallback value with the type of b.

 L.R (`or`) b = L.R or b
 L.R (`or`) b :: { ${name} :: a } -> String -> a | b

Function application

Let f be a function; x its applied argument and y the applied function result.

 y = f x

For comprehensiveness let the type signature of the above function be L and the applied argument R.

blow the argument R is applied to a function of type L.

 L R = L -> R -> T
 L R :: (a -> b) -> a -> b

'-' - minus operator

(Number -> Number -> Number)

'+' - plus operator

let
Larg :: String | Path;
Rarg  :: String | Path;
in
(Larg -> Rarg -> Larg) | (Number -> Number -> Number)

'?' - Has attribute

'++' - List concatenation

'<' '>' - comparison

'==' - Equality

'!=' - Inequality

'*' - Multiplication

'!' - Negation

'//' - Update

'&&' '||' '->' - Logical

Builtins

This section contains the proof that all nix builtins can be meaningfully and correctly annotated with the proposed type system.

There are currently 89 builtin functions, that can be discovered with

run nix __dump-builtins

Every builtins signature can be found below (sorted alphabetically)

Following symbols are used below

• ✅ - Compliant
• ⚠️ - Under construction.

Builtins - TODO: The type signatures are not compliant yet

abort ⚠️

String -> Error

add ✅

Number -> Number -> Number

all ✅

(a -> Bool) -> [a] -> Bool

any ✅

(a -> Bool) -> [a] -> Bool

attrNames ✅

{ ${key} :: a } -> [String]

attrValues ✅

{ ${key} :: a } -> [a]

baseNameOf ✅

( String | Path ) -> String

bitAnd ✅

Int -> Int -> Int

bitOr ✅

Int -> Int -> Int

bitXor ✅

Int -> Int -> Int

break ✅

a -> a

catAttrs ✅

String -> [ { ${name} :: a } ] -> [a]

ceil ✅

Number -> Int

compareVersions ✅

String -> String -> (-1 | 0 | 1)

concatLists ✅

[ [ a ] ] -> [ a ]

concatMap ✅

( a -> [ b ] ) -> [ a ] -> [ b ]

concatStringsSep ✅

String -> [ ( String | Path ) ] -> String

deepSeq ✅

a -> b -> b

dirOf ✅

a = (Path | String)
a -> a

div ⚠️

Number -> Number -> Number

elem ⚠️

a -> [b] -> Bool

elemAt ⚠️

[a] -> Int -> b

fetchClosure ⚠️

AttrSet -> AttrSet

fetchGit ⚠️

AttrSet -> AttrSet

fetchTarball ⚠️

AttrSet -> AttrSet

fetchurl ⚠️

String -> AttrSet

filter ⚠️

(a -> Bool) -> [a] -> [b]

filterSource ⚠️

(Path -> String -> Bool) -> Path -> Path

floor ⚠️

Float -> Int

foldl' ⚠️

(a -> b -> c) -> a -> [b] -> c

fromJSON ⚠️

String -> a

functionArgs ⚠️

(a) -> AttrSet

genList ⚠️

(a -> b) -> a -> [b]

genericClosure ⚠️

AttrSet -> [AttrSet]

getAttr ⚠️

String -> AttrSet -> a

getEnv ⚠️

String -> String

getFlake ⚠️

AttrSet -> AttrSet

groupBy ⚠️

(a -> b) -> [a] -> AttrSet

hasAttr ⚠️

String -> AttrSet -> Bool

hashFile ⚠️

String -> Path -> String

hashString ⚠️

String -> String -> String

head ⚠️

[a] -> a

import ⚠️

Path -> a

intersectAttrs ⚠️

AttrSet -> AttrSet -> AttrSet

isAttrs ⚠️

a -> Bool

isBool ⚠️

a -> Bool

isFloat ⚠️

a -> Bool

isFunction ⚠️

a -> Bool

isInt ⚠️

a -> Bool

isList ⚠️

a -> Bool

isNull ⚠️

a -> Bool

isPath ⚠️

a -> Bool

isString ⚠️

a -> Bool

length ⚠️

[a] -> Int

lessThan ⚠️

Number -> Number -> Bool

listToAttrs ⚠️

[{name :: String, value :: a}] -> AttrSet

map ⚠️

(a -> b) -> [a] -> [b]

mapAttrs ⚠️

(a -> b -> c) -> AttrSet -> AttrSet

match ⚠️

String -> String -> ( Null | [ String ] )

mul ⚠️

Number -> Number -> Number

parseDrvName ⚠️

String -> AttrSet

partition ⚠️

(a -> Bool) -> [a] -> AttrSet

Path ⚠️

AttrSet -> StorePath

pathExists ⚠️

Path -> Bool

placeholder ⚠️

String -> String

readDir ⚠️

Path -> AttrSet

readFile ⚠️

Path -> String

removeAttrs ⚠️

AttrSet -> [a] -> AttrSet

replaceStrings ⚠️

[String] -> [String] -> String -> String

seq ✅

a -> b -> b

sort ✅

(a -> a -> Bool) -> [a] -> [a]

split ⚠️

String -> String -> [String]

splitVersion ⚠️

String -> [String]

StorePath ⚠️

StorePath -> StorePath

stringLength ⚠️

String -> Int

sub ⚠️

Number -> Number -> Number

substring ⚠️

Int -> Int -> String -> String

tail ⚠️

[a] -> a

throw ⚠️

String

toFile ⚠️

Path -> String -> StorePath 

toJSON ⚠️

a -> String

toPath ⚠️

String -> Path

toString ⚠️

a -> String

toXML ⚠️

a -> String

trace ⚠️

a -> b -> b

traceVerbose ⚠️

a -> b -> b

tryEval ⚠️

a -> a

typeOf ✅

a -> "bool" | "int" | "float" | "string" | "set" | "list" | "path" | "null" | "lambda" 

zipAttrsWith ⚠️

(String -> [a] ) -> [a] -> AttrSet

Usage

The goal was to create a system that can add type hints to every expression in nix.

A nix file can contain many possible things.

So what kind of expressions and formats does the RFC need to support?

• named function expression.
• anonymous functions.
• named variables.

In any possible way nix has only expressions thus if this project covers all kind of expressions, it covers the complete nix language.

The following can be imported as a function called foo as the parent folder is named foo and contains a default.nix

# /foo/default.nix

{lib, ...}:
let
    applyIt = fn: fn 10;
#....
in
    act: applyIt act

Use-cases

Standardized (parsable) format to communicate type

There are simple functions with only few and basic arguments.

Number -> Number -> Number

But there are also complex functions, that other functions or nested attrsets as arguments. Communicate the rules those structures may have to follow is crucial.

String -> [ { ${name} :: a } ] -> [a]

We think; Understanding those type signatures with automated tooling is significant. For that to work we need a syntax that follows strict rules.

Provide hover and autocomplete information's on expressions

As a developer i'd like to get suggestions like:

• How many arguments does a certain function take?
• Type of the arguments?
• In case of Attribute-set arguments:
  • Which attributes of the required attributes are still missing?
  • Which optional attributes can i specify additionally?
• In general describe the type of an expression

Provide static type checks at development time

A static tool could check the actual type of the documented expression against the specified type. It is unclear how this would work, but it could certainly be done.

We think an approach would also include pre-evaluation of certain points, that are very hard to analyze statically.

Contributors

Thanks to all people who contributed to this project. (if agreed) github handles will be published here.