Defining the language

April 3, 2017

Before we can work on the type system, the first step is to define the language
in a way that will allow us to think about it. In particular, we wanted to
simplify it as much as possible by removing everything that could be considered
as syntactic sugar.
The main differences with plain nix are :

The various syntaxes (

`x.y`

,`x."foo"`

or`x.${e}`

) for accessing e recrord field are all reduced to the construct`x.e`

where`e`

is an expression. The same holds for the different ways of defining a record fieldThe definition of records is also simplified: the notation

`{e.e1 = y1; e.e2 = y2; …}`

is rewritten to its more explicit version`{ e = { e1 = y1; e2 = y2; …}; …}`

The

`rec { ... }`

construct is removed as well as it can be emulated by a let-binding (let-bindings being recursive).- The
`inherit`

keyword is also dropped in favour of explicit`"x" = x`

and`"x" = x.e`

fields declarations.^{2} Some builtins functions are replaced by operators − the difference being that those functions were first-class in nix, while the operators aren't.

This is due to the fact that those builtins (most probably) won't be typeable, but only their applications will. For example, the

`functionArgs`

builtin can't be given a type by itself, but given a function`f`

, an ad-hoc typing rule for`functionArgs`

will be able to give a type to`functionArgs f`

.The list of those operators isn't fixed and will depend on what the type-system can handle.

A constructor

`Cons`

and a constant`nil`

have been introduced to represent lists in a more conventional manner. This isn't strictly speaking a simplification of the language, but it will most probably be necessary in order to type polymorphic lists, and is far more pleasant to work with than the opaque (and imho unpractical) list definition in nix. Two new patterns have also been introduced to perform matching on lists.

Of course, this is still a work-in-progress, and all this is expected to change according to the evolutions of the work.

Some people may have noticed that the immediate translation from nix to nix-light is not complete in the sense that an arbitrary nix expression can't always be translated to an equivalent nix-light expression.

The first problem occurs when the `{ x.y = z }`

shortcut is used with dynamic fields names.

For example, if `e1`

and `e2`

are arbitrary expressions the record

can't be converted to an expression in nix-light syntax, because we can't statically know wether it would be

```
{
e1 = { "x" = 1; };
e2 = { "y" = 2; }; };
}
```

This case can be eluded by using a functions like the recursiveUpdate one defined in `nixpkgs/lib/attrsets.nix`

, but with the rather annoying consequence of transforming something already hard to type into something even harder − the gist of this being "don't use dynamic record field names if you can avoid it, or the type-checker will bite you".

As I told, the `rec { ... }`

construct can be expressed using a `let`

construct.

Once again, the problem arises with dynamic field names:

Can't be simply converted like the previous example because dynamic names aren't allowed in let-bindings.

My opinion on that problem is that this is something you shouldSo I won't really consider this a problem if the program fails on such cases. But of course, if someone finds a solution to encode this in nix-light, I'll gladly take it.

Toying with the nix language is also an excellent opportunity to try new stuff.

The introduction of list constructors and patterns is partially motivated by this (in fact, while the constructors will probably be very useful while typing, the patterns are just here because we find it far more consistent and logical). The goal is to see wether this raise any problem and wether it would be a good addition.

`"x" = x"`

in a record definition without provocating infinite recursion
`derivation`

keyword is just considered as a function taking as argument a certain type of record and returning another type of record. The whole "writing to the store" stuff is ignored as it has no incidence on typing.