July 3, 2017

This week has been dedicated to records: parsing, simplification and (a bit of) typing.

Summary of the week

Parsing of records

Nothing really fancy here: I've extended the parser to support records, record patterns and record type annotations.

The record and record patterns are exactly the same as in plain Nix − except that they may contain type annotations. The record type annotations looks similar to records: { field_1; ...; field_n; } or { field_1; ...; field_n; ... }. The fields may have the form field_name = type or field_name =? type. The first one means that the field named field_name has type type and the second one that the field named field_name is optional and has type type if present.

Note that contrary to records, the field names can't be dynamic (this wouldn't really make sense), and the syntactic sugar x.y.z = type isn't available. The trailing semicolon is also optional.

For example, the record

{
  x = 1;
  y = {
    z = true;
    k = x: x + 1;
  };
}

has the type

{
  x = Int;
  y = {
    z = Bool;
    k = Int → Int;
  }
}

and the function

{ x /*: Int */, y /*: Bool */ ? true, ... }: if y then x else x+1

has the type

{ x = Int; y =? Bool; ... } → Int

Simplification

Nix has a special syntax for defining nested records:

{
  x.y = 1;
  x.z = 2;
}

Although this syntax is really practical, we can't directly work on such a representation, and we must transform a record such as the previous one into something of the form { x = { y = 1; z = 2; }; }.

This is a rather simple task in the general case, but happends to be impossible as soon as some field names are dynamic: How may one know whether { ${e1}.x = 1; ${e2}.y = 2; } is a record of the form { foo = { x = 1; y = 2; }; } or of the form { foo = { x = 1; }; bar = { y = 2; }; }?

So we have to be careful while treating them. Currently, I simply assume for the sake of simplicity that no conflict will occur (i.e. that the previous example will correspond to { foo = { x = 1; }; bar = { y = 2; }; }, but this is obviously wrong in the general case, so I'll have to add more subtlety in the future.

Typing of record patterns

The two previous points took me quite a long time (worse that what I expected to be honest), so I just began the actual typing work. I however got enough time to type the record patterns (which isn't really useful while I can't type record literals, but still).

More on this next week, because it makes more sense to present the whole record typing at once.

Next steps

Time flies, and I already have only two months left (minus some holidays that I'll have to take for my own sanity) until the end of my internship (my defense is planned on September, 1st). I plan to continue my work on this − and hope other people will join me once it reaches an advanced enough state − but I won't be able to be full-time on it, so it will likely advance much slower (hence I want to do as much as possible while I can spend all my days on it).

So here's a quick plan of what remains to do:


Commentaires