Munich NixOS Meetup

NixOS 17.09 "Hummingbird" will be the next release scheduled to be released on September 28, 2017. Time to party!

Meet other fellow Nix/NixOS users & developers and the 17.09 release managers for some drinks.

More information will follow.

München - Germany

Friday, September 29 at 7:00 PM

13

https://www.meetup.com/Munich-NixOS-Meetup/events/243579914/

Composing Nix packages in PHP

namespace Pkgs;
use PNDP\AST\NixFunInvocation;
use PNDP\AST\NixExpression;

class Stdenv
{
    public function mkDerivation($args)
    {
        return new NixFunInvocation(new NixExpression("pkgs.stdenv.mkDerivation"), $args);
    }
}

namespace Pkgs;
use PNDP\AST\NixURL;

class Hello
{
    public static function composePackage($args)
    {
        return $args->stdenv->mkDerivation(array(
            "name" => "hello-2.10",

            "src" => $args->fetchurl(array(
                "url" => new NixURL("mirror://gnu/hello/hello-2.10.tar.gz"),
                "sha256" => "0ssi1wpaf7plaswqqjwigppsg5fyh99vdlb9kzl7c9lng89ndq1i"
            )),

            "doCheck" => true,

            "meta" => array(
                "description" => "A program that produces a familiar, friendly greeting",
                "homepage" => new NixURL("http://www.gnu.org/software/hello/manual"),
                "license" => "GPLv3+"
            )
        ));
    }
}

class Pkgs
{
    public $stdenv;

    public function __construct()
    {
        $this->stdenv = new Pkgs\Stdenv();
    }

    public function fetchurl($args)
    {
        return Pkgs\Fetchurl::composePackage($this, $args);
    }

    public function hello()
    {
        return Pkgs\Hello::composePackage($this);
    }
}

public function __call($name, $arguments)
{
    // Compose the classname from the function name
    $className = ucfirst($name);
    // Compose the name of the method to compose the package
    $methodName = 'Pkgs\\'.$className.'::composePackage';
    // Prepend $this so that it becomes the first function parameter
    array_unshift($arguments, $this);
    // Dynamically the invoke the class' composition method with $this as first parameter and the remaining parameters
    return call_user_func_array($methodName, $arguments);
}

Converting PHP language constructs into Nix language constructs

• A variable of type boolean, integer or double are converted verbatim.
• A string will be converted into a string in the Nix expression language, and conflicting characters, such as the backslash and double quote, will be escaped.
• In PHP, arrays can be sequential (when all elements have numeric keys that appear in numeric order) or associative in the remainder of the cases. The generator tries to detect what kind of array we have. It recursively converts sequential arrays into Nix lists of Nix language elements, and associative arrays into Nix attribute sets.
• An object that is an instance of a class, will be converted into a Nix attribute set exposing its public properties.
• A NULL reference gets converted into a Nix null value.
• Variables that have an unknown type or are a resource will throw an exception.

Building packages programmatically

/* Evaluate the package */
$expr = PNDPBuild::evaluatePackage("Pkgs.php", "hello", false);

/* Call nix-build */
PNDPBuild::callNixBuild($expr, array());

Building packages from the command-line

$ pndp-build -f Pkgs.php -A hello

$ pndp-build -f Pkgs.js -A hello --eval-only

$ pndp-build -f Pkgs.js -A hello --eval-only --format

Discussion

Availability

I was recently working on a small little project - a client API for the ListenBrainz project. Most of the details aren’t particularly interesting - it’s just a HTTP client library to a REST-like API with JSON. For the implementation, I let Servant and aeson do most of the heavy lifting, but I got stuck when considering what final API to give to my users.

Obviously, interacting with ListenBrainz requires some sort of IO so whatever API I will be offering has to live within some sort of monad. Currently, there are three major options:

1. Supply an API targetting a concrete monad stack.

   Under this option, our API would have types such as

   submitListens :: ... -> M ()
   getListens :: ... -> M Listens

   where M is some particular monad (or monad transformer).

2. Supply an API using type classes

   This is the mtl approach. Rather than choosing which monad my users have to work in, my API can be polymorphic over monads that support accessing the ListenBrainz API. This means my API is more like:

   submitListens :: MonadListenBrainz m => ... -> m ()
   getListens :: MonadListenBrainz m => ... -> m Listens

3. Use an extensible effects framework.

   Extensible effects are a fairly new entry, that are something of a mix of the above options. We target a family of concrete monads - Eff - but the extensible effects framework lets our effect (querying ListenBrainz) seamlessly compose with other effects. Using freer-effects, our API would be:

   submitListens :: Member ListenBrainzAPICall effects => ... -> Eff effects ()
   getListens :: Member ListenBrainzAPICall effects => ... -> Eff effects Listens

So, which do we choose? Evaluating the options, I have some concerns.

For option one, we impose pain on all our users who want to use a different monad stack. It’s unlikely that you’re application is going to be written soley to query ListenBrainz, which means client code becomes littered with lift. You may write that off as syntatic, but there is another problem - we have committed to an interpretation strategy. Rather than describing API calls, my library now skips directly to prescribing how to run API calls. However, it’s entirely possible that you want to intercept these calls - maybe introducing a caching layer or additional logging. Your only option is to duplicate my API into your own project and wrap each function call and then change your program to use your API rather than mine. Essentially, the program itself is no longer a first class value that you can transform.

Extensible effects gives us a solution to both of the above. The use of the Member type class automatically reshuffles effects so that multiple effects can be combined without syntatic overhead, and we only commit to an interpretation strategy when we actually run the program. Eff is essentially a free monad, which captures the syntax tree of effects, rather than the result of their execution.

Sounds good, but extensible effects come with (at least) two problems that make me hesistant: they are experimental and esoteric, and it’s unclear that they are performant. By using only extensible effects, I am forcing an extensible effects framework on my users, and I’d rather not dictate that. Of course, extensible effects can be composed with traditional monad transformers, but I’ve still imposed an unnecessary burden on my users.

So, what do we do? Well, as Old El Paso has taught us: why don’t we have both?

It’s trivial to actually support both a monad transformer stack and extensible effects by using an mtl type class. As I argue in Monad transformers, free monads, mtl, laws and a new approach, I think the best pattern for an mtl class is to be a monad homomorphism from a program description, and often a free monad is a fine choice to lift:

class Monad m => MonadListenBrainz m where
  liftListenBrainz :: Free f a -> m a

But what about f? As observed earlier, extensible effects are basically free monads, so we can actually share the same implementation. For freer-effects, we might describe the ListenBrainz API with a GADT such as:

data ListenBrainzAPICall returns where
  GetListens :: ... -> ListenBrainzAPICall Listens
  SubmitListens :: ... -> ListenBrainzAPICall ()

However, this isn’t a functor - it’s just a normal data type. In order for Free f a to actually be a monad, we need f to be a functor. We could rewrite ListenBrainzAPICall into a functor, but it’s even easier to just fabricate a functor for free - and that’s exactly what Coyoneda will do. Thus our mtl type class becomes:

class Monad m => MonadListenBrainz m where
  liftListenBrainz :: Free (Coyoneda ListenBrainzAPICall) a -> m a 

We can now provide an implementation in terms of a monad transformer:

instance Monad m => MonadListenBrainz (ListenBrainzT m)
  liftListenBrainz f =
    iterM (join . lowerCoyoneda . hoistCoyoneda go)

    where
      go :: ListenBrainzAPICall a -> ListenBrainzT m a

or extensible effects:

instance Member ListenBrainzAPICall effs => MonadListenBrainz (Eff effs) where
  liftListenBrainz f = iterM (join . lowerCoyoneda . hoistCoyoneda send) f 

or maybe directly to a free monad for later inspection:

instance MonadListenBrainz (Free (Coyoneda ListenBrainzAPICall)) where
  liftListenBrainz = id

For the actual implementation of performing the API call, I work with a concrete monad transformer stack:

performAPICall :: Manager -> ListenBrainzAPICall a -> IO (Either ServantError a)

which both my extensible effects “run” function calls, or the go function in the iterM call for ListenBrainzT’s MonadListenBrainz instance.

In conclusion, I’m able to offer my users a choice of either:

• a traditional monad transformer approach, which doesn’t commit to a particular intepretation strategy by using an mtl type class
• extensible effects

All without extra syntatic burden, a complicated type class, or duplicating the implementation.

You can see the final implemantion of listenbrainz-client here.

Bonus - what about the ReaderT pattern?

The ReaderT design pattern has been mentioned recently, so where does this fit in? There are two options if we wanted to follow this pattern:

• We require a HTTP Manager in our environment, and commit to using this. This has all the problems of providing a concrete monad transformer stack - we are committing to an interpretation.
• We require a family of functions that explain how to perform each API call. This kind of like a van Laarhoven free monad, or really just explicit dictionary passing. I don’t see this really gaining much on abstracting with type classes.

I don’t feel like the ReaderT design pattern offers anything that isn’t already dealt with above.

Munich NixOS Meetup

With the NixOS community of practice (CoP) we want to establish a regular get-together with people who are passionate about any Nix / NixOS related topic. There will be no talks and there is no agenda, instead we discuss, learn or work in pairs or groups on specific topics.

There will be food and drinks sponsored by HolidayCheck.

Munich - Germany

Thursday, August 3 at 5:00 PM

8

https://www.meetup.com/Munich-NixOS-Meetup/events/242120700/

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:

• On the typing side of things:

  • Finish the typing of records

  • Write a default typing environment with all the built-in values.

    Some of them (like functionArgs for example) will be available as operators with custom typing rules because it isn't really possible to give them a meaningful type.

  • Get a real gradual type

    There's currently a type that is called "gradual" in the tool, but it is in fact nothing but a new type constant (akin to Int or Bool) without any special behaviour.

  • Fix the subtyping

    The subtyping relation that is used isn't exactly the one one would expect (because it has been designed for a strict language and Nix is lazy, and this introduces some differences in the subtyping).

    Unless some clever hack is found to reuse the existing algorithm this is gonna be really tricky and I may not be able to do it before September.

  • Rewrite the pretty-printing of types

    The pretty-printing of the types is currently handled by CDuce (the language whose type-system I based this one on), but as its types are slightly different from ours, the pretty-printing isn't always exactly accurate. So if it isn't too hard, I'll rewrite a custom pretty-printer.

• On a more practical side:

  • Document everything

    Although all the documentation should be present in my work notes, this blog or my future thesis, a proper manual and tutorial has to be written for this to be usable by someone else than me.

  • Run more extensive tests on the parser to ensure its compatibility with plain Nix

  • Enhance the interface

    Apart from an OCaml library, the interface for the typechecker is a quickly written executable which I use for testing and which will require some work in order to be usable

  • Choose the default warnings and errors

    The errors reported by the tool are configurable, but a couple of defaults sets (the "strict" and the "permissive" modes) will cover 99% of the usages and avoids the need for the user to understand every detail of the type system.

  • Enhance the error reporting

    The error messages are rather rough and need to be polished

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

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.

I couldn't find the time last week to make something presentable out of the typechecker as I promised, but almost all the features are already here − except records which I'll probably start implementing in a few weeks.

Implementation

State of the typechecker

I finished most of the engine for the language without records, so I'll now work on adding everything that is needed around, and handling some constructs that could be ignored from a theoretical point of view − mostly because it could be considered as just some syntactic sugar.

Here are the constructs that need to be considered:

Assert

The assert construct should be typed in a rather simple way, as assert e1; e2 is equivalent to if e1 then e2 else raise "Assertion failed" Well, it is not strictly equivalent because the exceptions raised by assert and the one raised by raise aren't exactly the same − see this comment −, but four our purposes, it is the same. .

Import

The simplest way to handle the import statement is to simply replace it by a dump of the imported file. This is probably what I will do in a first time. In a second time, it may be useful for performance reasons to type the imported file separately and memoïze the result (this is what nix does with the evaluation iirc).

Different modes of check

During the design of the type-system, there has been a constant tension between having a safe type-system and being able to typecheck as much existing code as possible.

Eventually, it became clear that both weren't compatible, and that in order to keep the best of both worlds, we needed to have (at least) two different versions (a "permissive" one and a "strict" one) of the type-system. So that's what we decided to do, with an annotation to switch from one to the other. Nothing has been implemented in this direction, and the boundary between strict and permissive hasn't been decided yet − especially, it will mostly concern records. But an important point is that the gradual type will be considered differently.

On the theoretical side

There hasn't been much improvement here, as I am still stuck with the proof of correctness, which is definitely harder than expected (but I must admit, I didn't work a lot on it). A PhD student of my advisor is also working on a really similar proof, and hopefully he will find a solution − as I don't really have much more time for this because I need to work on the implementation.

Next week

I'll start drafting headlines for my dissertation; this will allow me to see which points need some more work.

In parallel, I plan to make the type annotations for lists − this will probably deserve its own post as there is some really elegant stuff that I borrow from CDuce and that are worth presenting, as well as to treat the assert and import keywords.

I'm also rewriting the parser − this is already almost over, but there is still a few polishing work ongoing, as the old one was a quick and dirty crafted one, that I wrote in order to be quickly able to work on the typechecker itself, but which behaves quite badly − in particular regarding error messages.

This week has been shared between a lot of easy fun putting together all the pieces that I worked on during the last weeks, and a lot of frustration trying to prove the soundness of the system.

Implementation

After several weeks spent trying to understand the API of CDuce − the language our type-system takes it inspiration from and whose code we planned to reuse as much as possible to ease the Implementation −, I eventually understood it enough to start using it for writing the inference engine.

This has been really enjoyable, as all I had to do was plugging together a few functions that where already dealing with all the boring low-level stuff, and everything has been almost instantly working. I could quickly write a prototype of typer for the core lambda-calculus of the language. It is still a little bit too rough on the edges to be presented, but I should (hopefully) be able to present some nice examples for next week.

On the theoretical side

I talked last week about some difficulties with the proof of the soundness of the type-system.

Those difficulties still hold, although some progress has been done. There are a couple of paths that we are currently exploring for a this:

• We may change a bit the semantic of the language we work on (which is currently an approximation of the lazyness of nix) with something closer actual lazyness. This should probably solve our problems, but at the cost of redefining the language with a heavier and less practical formalism.

• We may use a non-syntactic proof using something like what is described in this paper which a colleague from tweag suggested to me. While mathematically-heavy, this kind of proof has the advantage of being able to operate on our simplified semantic, which means we can keep our simple formalism everywhere else. It also is more modular than syntactic proofs, which means that we may prove some extensions of the core system without needing to rewrite the full proof.

Next week

Next week will be more or less like this one: I'll continue the implementation using all the nice features offered by CDuce. In the same time, I'll keep on working on the proof − I hope that this will be solved before next Friday.

Provided I find the time − which is rather unlikely, but who knows? − I'll also try to make an online demonstration of the engine to show the progress of the implementation.

It's been a month (already !) since my last update on this work. In the meantime, we've begun to prove a subset of the type-system, and (slowly) started the implementation.

Bidirectional typing

One nice feature that we added in order to make our system more powerful is a little touch of bidirectional typing, which allows us to type some expressions that the old type-system wasn't powerful enough to type.

Here is an example (and in fact the example that motivated this addition in the first place):

let f :: (true → Int → Int) ∧ (false → Bool → Bool) =
  cond: x: if cond then x+1 else not x in f

Although the type annotation corresponds to a type that's perfectly reasonable − f applied to a value of type true and a value of type Int returns an Int, and applied to a value of type false and a value of type Bool returns a Bool −, the type-system isn't able to infer it. It doesn't matter how we annotate the expression, it can't, because we would have to annotate x as either Int or Bool depending on the value of cond, and our system can't express this.

Without diving into the details, this is now possible to do. Of course this exact case isn't really exciting as it is easily possible to rewrite is as something with roughly the same semantics and that already was possible to type. But the really nice thing is that most of the times you now only have to annotate the top-level functions, and not every single lambda in the code.

Proving the type-system

The main work of those last weeks has been on establishing a proof of the soundness of (the core of) the type-system.

Saying that a type-system is "sound" intuitively means that it respects the adage that "well-typed programs cannot go wrong". The exact definition depends on what it is intended for, but in our case we can define it as "A well-typed expression will either loop indefinitely, raise an exception, or reduce to a value" (where a value is a constant, a list, a record, a function…).

We've been working on this the last few weeks, and this is somehow harder than expected. The classical way of proving soundness is to prove two lemmas known as "subject reduction" and "progress". The first one states that if a well-typed expression e reduces ("evaluates") to another expression e', then e' is also a well-typed expression, which has the same type as e (or a more precise type). The second one states that if e is a well-typed expression, then it reduces to some e'. The combination of those two lemmas give us our soundness theorem.

The fact is that the subject-reduction lemma doesn't hold for our system − for a couple of reasons that I won't detail here to keep things simple, but that I would gladly explain if anyone is interested. We see some possible workarounds for this, but we still have to investigate a little more to ensure that they are viable.

Implementation

We also started the implementation. For this, we will reuse a lot of code from the implementation of the type system of the CDuce language because ours shares a lot with it. In particular, a really big part − maybe the biggest part − of the implementation is the subtyping relation, which is the same in CDuce and in Nix.

Unfortunately the code of CDuce, although really well-written, lacks of documentation and is hardly commented, so it took me some time to get into it.

Plans for the future

Apart from trying to keep this weekly newsletter weekly − and I apologize for the whole month of silence, I'll try next week to come up with a clear idea of how to prove the soundness (not a fully redacted proof, but at least the main arguments), and advance on the implementation − ideally, I'd like to have a working prototype of a simplified type-checker (without bidirectional typing) for the core lambda-calculus − no lists and no records − within three weeks (but I'm not very good at estimates, so this doesn't mean much).

Munich NixOS Meetup

Talk by Johannes Bornhold

NixOPS is the cloud deployment tool out of the NixOS ecosystem. It is based on Nix and NixOS and allows to describe a network of machines and additional resources. Based on this description the network can be deployed.

The container backend is based on NixOS' built-in container support. The talk will give a short introduction into the usage of NixOPS and the container backend. This will be based on my experiences trying to use the container backend to quickly throw a few containers into a virtual machine and later deploy these container on a regular server.

The second part will give an introduction into NixOPS internals with a focus on its container backend. This part will cover the internal structure of the NixOPS codebase as well as the way how declarative and imperative NixOS containers do currently work, looking from the NixOPS angle.

If some people are interested we can do a little hackathon afterwards. Proposed topic by Johannes:

• Unify declarative / imperative NixOS containers to extend it's usability from the NixOPS perspective. This is the bit I ended up working on, instead of throwing containers out into my virtual machine.
    Some background food on this topic:
    • Some notes on this PR
    • Early code fragments      

My goal would be to look at some small steps to further explore this approach.

Munich - Germany

Friday, May 26 at 6:00 PM

26

https://www.meetup.com/Munich-NixOS-Meetup/events/239835348/

This week's post will be about adding gradual types and type annotatinos to the system.

Last week, we took advantage of the fact that Jeremy Siek, the inventor of gradual typing was in Paris to work on adding gradual types to the system.

This has also been the occasion to explicit where type annotations would be needed.

About gradual types

(note that this is just a very quick introduction. If you want something more detailed, I enjoin you to read the original blogpost about it).

The jungle of programming languages is roughly split into two universes: the typed world and the untyped one. The goal of gradual typing is to bridge the gap in between. For this purpose, we add a new type (the "gradual type", often written ?), which is the type of expressions that we do not want (or can't) type.

The type ? can replace every type (for example, if a function expects an argument of type Int, I can pass in a value of type ? instead), and every type can replace the type ? (so if a function expects an argument of type ?, I can pass an Int or a Bool or a function String → (? → Bool) instead).

This tool is used in various languages such as Hack, Flow or Typescript.

Back to nix

So how can this be useful for nix?

First, let's see where we need to help the (classical) type checker in order to see where and why those types can help.

Type annotations

While a type-checker can be really smart, the mind of a programmer is often way too weird for him it may only infer a limited amount of stuff, and often needs some hints to understand what is going on.

In the case of nix, there are two places where you probably will need to annotate stuff: lambdas and (recursive) let-bindings. Those are the places where it would otherwise have to guess the type of variables, In some type-systems such as the Hindley-Milner type system used in the ML languages, there is no need for such annotations because the type-system is simple enough to allow working around that impossible guess. Unfortunately, those workarounds do not scale with more complicated type systems − in particular with intersection types. which is out of his reach. This doesn't mean that the type-checker won't be able to say anything about those, just that most of the time, the types it would infer would be too imprecise.

Lambdas

In order to type a function λx.e, the type-checker will have to type the body e without knowing anything about x, and by the way deduce the possible types for x. This is possible in ML thanks to unification, but unfortunately wouldn't work in our case.

As a consequence, the programmer will have to explicitly annotate the type of the argument, so that the type-checker can do its job. In fact, the programmer may even write several types for the argument, because function types aren't only arrows τ → σ, but also intersections of arrows ⋀_i(τ_i → σ_i). So for each type τ_i of the argument, the type-checker will run to deduce a return type σ_i. Functions will then have a form like λx:(τ1;...;τn).e

Recursive let-bindings

Recursive declarations are similar to lambdas in the sense that we use a variable before it is fully defined − hence before it is typed. So for the very same reason, we must annotate the variables that we define recursively.

Including gradual types into this

Those annotations seem like a reasonable trade-off, but it breaks compatibility with existing untyped code. The obvious solution is to add a default type annotation if none is given by the programmer, which must be the gradual type if we want the body to type and still stay sound.

So an unannotated function λx.e is just syntactic sugar for λx:?.e.

That's nice, but what do we do with it?

The essence of the gradual type is that a value of type ? can be used in place of anything, and any value can be used where the type ? is expected. So in this case, the function will work exactly as it would in the untyped world: the argument can be used as a value of any type inside the body, and any value can be passed as argument.

(The concept of gradual typing also includes adding explicit casts at the boundaries between the typed and untyped worlds so that runtime type errors appear reliably at the right place, but as we do not touch the nix interpreter itself, this is out of scope for this project).

Working around the lack of polymorphism

The first use of gradual typing is a transitional one: we plan to use it to type legacy code, waiting for it to be rewritten in a typed way.

Another use, which is also (I hope) a transitional one is to mitigate the weaknesses of the type system (waiting for it to be improved of course). In particular, there is currently no polymorphism for now (because we don't know how to make polymorphism work with records and − ironically − gradual typing). This is rather annoying, mainly because some basic functions (head, tail, fix, …) are polymorphic (and typing them otherwise wouldn't make sense). There are people working on this, and hopefully a solution will land soon, but in the meantime, we have to deal with the absence of polymorphism.

For some really basic and important functions, we may hardcode some typing rules to implement in an ad-hoc way the missing polymorphism. But as we can't do this for every function, an acceptable solution is to type the other one gradually (so for example the identity function could be typed by ? → ? or the head function by [? ?*] → ?. This would of course be rather imprecise in some cases, but nonetheless allows us to give a useful type to those polymorphic functions.

Some examples

Let's now see some real nix code. This is an example from the first post of this blog

Gradual typing of a function

x:
if isInteger x then
  toString x
else if isBool x then
  x
else
  raise "Invalid argument"

If we leave this as such, the type-checker will understand it as:

(x::?):
if isInteger x then
  toString x
else if isBool x then
  x
else
  raise "Invalid argument"

In this case, it will try to type the body under the assumption that x is of type ?, see that in this case the return type may be String or Bool, and thus type the whole function as ? → (String ∨ Bool).

With a type annotation

Now, suppose the programmer adds a type annotation to the argument:

(x::Int ∨ Bool):
if isInteger x then
  toString x
else if isBool x then
  x
else
  raise "Invalid argument"

The type-checker will now type the body under the assumption that x is of type Int ∨ Bool. Like in previous case, he will find a type String ∨ Bool, and deduce a type (Int ∨ Bool) → (String ∨ Bool) for the body.

That's cool, but it could do better, this is not the most precise type for the function, we would like the type-system to infer the type (Int → String) ∧ (Bool → Bool) instead.

With a types annotation

Remember somewhere earlier, I told that you sometimes would need to annotate several types for the argument. This has been intended exactly for those situations. If we just change the type annotation to this:

(x::Int; Bool):
if isInteger x then
  toString x
else if isBool x then
  x
else
  raise "Invalid argument"

the type-checker will try to infer the type of the body twice: a first with the assumption x::Int (in which case he infers a return type String), and a second time with the assumption x::Bool (in which case he infers a return type Bool). Then, he will take the intersection of those two results to deduce the final type of the function, which will here be (Int → String) ∧ (Bool → Bool), as expected.

All those reasonings also apply to recursive let-bindings (although the need of annotating several types in a let-binding is rather unlikely to happen).

Further thoughts

Patterns

For simplicity, I eluded here everything related to patterns by assuming that the functions were in the form x:e. When the argument is matched against a pattern, it is of course possible to use this to get more informations about the domain of the function, even without annotation.

Concrete sytax for type annotations

For simplicity again, I assumed that the language was extended with type annotations, which obviously are not present in nix. So to keep compatibility, those will probably have to be written in a way that makes the nix parser happy, most probably inside comments (or we can try to add them to the official parser, which would be even better).

Non-recursive let-bindings

Unlike nix, nix-light has two separate let and let rec constructs. This is nice because the non-recursive version is trivial to type, and doesn't require any type annotation. During the compilation from nix to nix-light, it is possible to translate let-bindings who do not use recursion into non-recursive one, so that some let-bindings in nix won't need to be annotated.

Nix is all about records. They are everywhere in nixpkgs, and even the semantics of nix seems to have been designed with this idea of records everywhere as a first class construct. (In fact, I think that it would be more correct to think of nix as "json with lambda-calculus on top of it" rather than "a functional language with lists and records").

Thus we have to type records.

What are records?

Records (or "attribute sets" as they are called in nix) are a data structure associating expressions (of an arbitrary type) to strings. More precisely, a record is a finite map from strings (the "labels" of the record) to the set of all expressions (the "values" of the record).

There are two main uses of records:

Static records

The first use of records is when you manipulate some data with a known structure that you want to store in a structured way. In this case, you know (statically) the labels and the type of the value associated to each label.

For example, the fetchurl function from nixpkgs (defined in pkgs/build-support/fetchurl/default.nix) expects arguments of the form:

{
  url = "some_string"; # Or nothing
  urls = [ "a" "list" "of" "strings"]; # Or nothing
  curlOpts = "some_string"; # Or nothing
  name = "some_string"; # Or nothing
  sha256 = "some_string"; # Or nothing
  executable = some_boolean; # Or nothing
}

(we only show some of the fields as the whole definition doesn't matter here)

For that kind of use, the name of the fields do not carry any semantic, they are just here to help the programmer (and in most compiled languages with static records, the name of the fields is dropped at compile-time).

This is the structure of the nixos options set (except that it is all done at runtime): all the option declarations generate a rigid structure in which the settings must fit. And (except for a few), the actual name of the options doesn't appear in the result of the evaluation.

Dynamic records (aka hashtables)

Another use of records is when we got some arbitrary data that we want to store with the possibility to retrieve it efficiently and easily, to iterate on it, to pass as a whole to another function... In that case, we may use records as hashtables − or as what functional programmers refer to as "maps" (with the restriction that the keys may only be strings). If the programmer doesn't want to shoot itself in the foot, all the fields will likely be of the same type.

This is used in particular for some nixos options (the one of type attrsOf α).

For example, the environment.etc option accepts as an argument a module whose fields will determine which files are copied (or symlinked) to /etc. By default, the label of each field will be used as the file name.

How do we type them?

Those two uses of records are really different, and require different typing (except of course if someone ever manages to provide some typing rules which unify both and are usable in practice).

The problem is that in nix (and in most untyped languages), both are happily mangled. They are first mangled because the same construct is used in both cases, with only some semantic considerations allowing to distinguish the intention of the programmer, and second because the same record is sometimes used as the same time as a static and as a dynamic one.

For example, the derivation builtins expects as an argument a record in which some fields ("name", "builder", "system", ...) are expected and have a special meaning, and all the others are just passed as environment variables.

Fortunately, we got a powerful enough formalism to be able to be still able do some typing (and some useful one!). The exact typing rules are on the github repository, but here is an informal writeup:

The base elements are atomic records (records with only one field), which are combined together to form bigger record. The rules for a basic record r = { e1 = e2; } where e2 has type τ are:

• If we can prove that e1 has value s where s designs a constant string ( resp. we know that e1 can only take a finite set of values s1, ..., sn), then r will have type { s: τ } (resp. { s1: τ; } | ... | { sn: τ; }).

• If can't determine a finite set of values for e1 (but we still know that it has type string), then we give the type { _: τ; } to r.

Various combination rules explain how to type the various merges of records, depending on whether we know that the fields are distinct or not.

There also are some (non published yet) rules for several builtins which will require some ad-hoc typing such as attrValues (which applied to a record returns the set of fields defined in it) or listToAttr (which applied to a key-value pairs list returns the corresponding record).

A note about nixos "types"

The nixos module system already has a notion of "types" and this new type system may seem redundant at least for this part of nixpkgs (or may seem to obsolete the old one).

A small explanation of how both can play together may however be quite useful. In general, embedding a type system into a language isn't really nice for the host type-system, because the guest may prove stuff than the host can't prove even with some help, and thus will want to bypass the restrictions it enforces. Fortunately, our type-system should be expressive enough to be able to understand the inner type system, and thus the actual typing of nixos options could be (for the most part) embedded into the new one. And for the cases where it would not be possible, the gradual part of the type system provides a nice way of bypassing the static type-system.

Munich NixOS Meetup

Der Augsburger Linux-Infotag ist eine eintägige Konferenz mit ca. 20 Vorträgen und 9 Workshops rund um Linux, Open-Source-Software und die digitale Gesellschaft. Der Eintritt ist frei.
Wir sind dort mit einem Stand zu NixOS vertreten :-)
https://www.luga.de/A...

Augsburg - Germany

Saturday, April 22 at 9:30 AM

6

https://www.meetup.com/Munich-NixOS-Meetup/events/239077440/

Munich NixOS Meetup

Let's do another hackathon! Bring the Nix project you are currently working on or struggling with and discuss it with other people. Followed by a barbecue in the evening. Please add to the Pad which food you will bring to the barbecue: https://etherpad.wiki...

Augsburg - Germany

Monday, May 1 at 2:00 PM

5

https://www.meetup.com/Munich-NixOS-Meetup/events/239077247/