Introduction

This (Draft) targets the # Type field declared in RFC-145

Motivation

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

• consistent function / API documentation.
• 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 checking (Partial)

Detailed implementation

I propose to formulate a syntax for the # Type section.

No need to use code brackets

using single or triple ``` (backticks) is not necessary. The complete # Type section allows writing one single type expression. The syntax of that is specified in the following.

Builds on top of dynamic types

Type information from comments can; just like in the latest js-docs; be used as a source for checking the correctness of code. We could imagine static type checking to work in symbiotic ways with dynamic type checking, such as YANTS (by TVL).

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. We think it is more important to provide a good abstraction and find the right compromise between simplicity and expressiveness.

Comparison nixOS-modules system

In general, developers must break complex parts into modules. Allowing them to follow the SOLID principles. Where you could write the interface definition and then develop or refactor the module behind that interface. As long as the interface stays the same or is downwards compatible nothing in your software breaks. This property is a very essential feature for writing stable and extendable code.

Nix offers nixos-modules to write such modules and interface declarations. However, those declarations are boilerplate codes that may run during evaluation time. And also increases complexity as a lot is going on with merge behavior priority (e.g. mkForce) and so on. Also, it is not clear what is validated and how much it costs in terms of additional runtime overhead. With type annotations, this can be improved. It is not considered mutually exclusive but rather inclusive to use both worlds together. Validate at runtime what cannot be known statically (before runtime) and validate statically once you are sure about something in a static context. (This is essentially called a 'gradual' type system) A good type system would offer both and even detect automatically when to run the check.

Thanks to @roberth and @theophane to point me towards this.

Future Work

• In the Future, the syntax could be integrated into the Nix language. With optional typings; Just like in Python or Javascript.
• Interface documentation could then be generated from the nix language itself if types were specified.

Getting started

This repo will soon provide a syntax checker. Which will check the type syntax.

Type-checking itself will not happen yet.

TODO: Fill this section to embrace consistent documentation.

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.

[Optional] Spaces between Operators are recommended

This follows the nix syntax rules. The symbols and grammar rules of the nix language are adopted.

Spaces are required where they would be required in valid nix syntax. This will be quite intuitive

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

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. ...

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

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. ...

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.

If that name does not exist it is called non-existing member name.

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

() 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 syntax rule!

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

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
  # ....

... - 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 arguments of one 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

• 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

'.' - Attribute selection

Usage of the (.) operator:

L must be an AttrSet, and R must evaluate to type String

If R itself contains an expression this is parenthesized with the ${ } operator. This operator tells the parser to evaluate the expression in R before passing it to the (.) function.

 L(.)R = L.R 

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

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

 y = x - 1

(-) is a special case where the RHS is applied first to the function. So if the LHS was omitted it gets the value 0 as type Int.

 L(-)R :: R -> L -> T
 (-) :: ( Int | Float ) -> ( Int | Float | 0 ) -> (Int | Float)

The minus operator is a dependent type It depends on the received argument value

• If it receives two Int types it returns Int
• but if one or both of its arguments is of type Float it returns type Float
• The type signature is correct using the Number type, but it lacks the information about its value dependency.

'+' - plus operator

'?' - 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.