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.

Nix-light

The language we came up (that we will call nix-light in lack of a better name for now) with is (modulo some modifications) a subset of nix. You can find its grammar here and its (not fully written yet) semantics here. 1

The main differences with plain nix are :

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

Some will be left behind...

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.

Merging of sub-records

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

{
  ${e1}.x = 1;
  ${e2}.y = 2;
}

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; }; };
}

or

{ e1 = { "x" = 1; "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".

Recursive records with dynamic fields

As I told, the rec { ... } construct can be expressed using a let construct.

rec {
  l1 = e1;
  
  ln = en;
}

is equivalent to

let
  l1 = e1;
  
  ln = en;
in
{
  l1 = l1;
  
  ln = ln;
}

Once again, the problem arises with dynamic field names:

rec {
  e1 = e'1;
  e2 = e'2;
}

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 should never ever do, regardless of typing constraints. 3

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

Some small extras

Semantics

The semantic given for nix-light can quite easily be extended to nix, and thus can serve as a starting point if someone ever wants to formalize the language 4

Lists

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.


1 The − probably more up-to-date − sources are available here
2 As recursive records don't exist anymore, one can write "x" = x" in a record definition without provocating infinite recursion
3 IMHO this also holds most of the time for any use of dynamic fields. It would probably have been better if nix din't allow them and had a proper map data structure for the (rare) cases where it is needed
4 note however that this semantic is limited to what interests us for the purpose of type-checking. In particular, the 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.

Commentaires