June 26, 2017

After some more engineering on the typer, I'll now start dealing with records

Summary of the week

This week has been mostly spent on engineering and preparing future work.

Improving the language coverage

The tool now parses and types some more languages constructs (like the assert or the include). I still have a little more work to do on this , like parsing the different flavours of strings/paths and the <foo> syntax, but this should be only some parsing work, and the typechecker itself should not be touched.

Warnings and errors

Before this week, the behaviour of the typechecker was to raise an exception whenever a type error occur, and return the type of the current expression otherwise. While this is sufficient for typechecking, it was not fully satisfactory, because in a near future I plan to also issue some − non fatal − warnings, which exceptions couldn't provide me.

So I refactored the typechecking engine to also return a list of warnings. A nice side-effect of this is that it was also trivial to make errors non-fatal − in case of a type-error, the typer just gives the type ? to the expression and adds the error to the list. This allows the typechecker to show more errors in one run.

Typer pragmas

In order to define locally which warnings are enabled, I also added some "pragmas" to the syntax (inside comments like for the type annotations in order to keep compatibility with standard Nix, of course). Those will be used to tell the typer to activate or deactivate certain warnings/errors for a given expression − or to switch between strict and permissive mode. Those modes will by the way most probably be defined as some presets of activated warnings and errors.

Records

Records are the next big step for this work.

I already briefly presented their typing in a previous post. The theory has globally stayed unchanged as this seems to be the better trade-off between usability and expressiveness. There will however be some differences between the strict and the permissive mode. Here are some notable cases that will covered by warnings.

Overlapping fields

If e is an arbitrary expression of type String, and e' of type τ then we know that we can type { e = e'; } with the type { _ = Undef ∧ τ; }, which means that each field of the record is either of type τ or undefined.

Now, let's assume that e1 and e2 both have type String (and e1' and e2' have type τ1 and τ2 respectively). We would like to type { e1 = e1'; e2 = e2'; } with { _ = Undef ∧ τ1 ∧ τ2 }, which would mean that each field of the record can have the type τ1 or τ2 or be undefined.

However, this isn't exactly true, because if both e1 and e2 evaluate to the same value, then the record is undefined. This can be ignored, of course, as if the record is undefined it can be given any type we want (and in particular { _ = Undef ∧ τ1 ∧ τ2 }), but there will probably be a warning for this, as it may lead to unpredictable failures.

Access to a maybe-undefined field

If e has type { _ = τ; }, then we can't ensure that accessing to any of its fields will succeed. Thus it will be forbidden in strict mode, unless guarded by an or clause. In a similar fashion, an expression such as e1.${e2} where we can't ensure that e2 evaluates to a label of e1 will be forbidden.

However, this a rather common pattern, so it will probably be allowed in permissive mode.

The with statement

The with construct is one of the worst evils in Nix. Records are a hard topic because they can have dynamic fields which are impossible to reason about in the general case. And with brings this difficulty to the top-level. This means that you can't even know which variables are in scope. And this is really bad. So it is possible that this construct will be simply forbidden in strict mode.

In permissive mode, a "best effort" typing will be done, depending on whether the imported record is statically known or not. It should also be possible (but probably later) to add some warnings about variable shadowing 1 .

Misc

I also finalized last week a blog post for Tweag I/O about this work. It turned out to be quite popular, making the first page on Hacker News (even being #1 for a few minutes!) and hopefully made some good advertising for Nix in general.


1 In case you don't know, with behaves quite weird when it comes to variable shadowing: If a variable is already in scope, it will not be redefined by the with statement. For example, let x = 1; in with { x = true; }; x evaluates to 1 and not true. This has been decided to prevent accidental variable capture, but it also causes accidental variable "non-capture" in the sense that you may be surprised if you didn't remember that the variable was already defined earlier.

Commentaires