Let's type nix !

March 28, 2017

So this is it, my internship has begun.
As promised, I will try to post regular updates on my work on this blog.
I (with my advisor) have been working on the nix grammar : our goal was to define the simplest version of the grammar (by removing everything that can reasonably be considered as syntactic sugar) which will be used as a basis for all the reasoning, and to define a subset of the language that we will support.

We are of course still far away from an effective type system, but here is an
overview of what it could look like (note that this is just an *a priori*
overview and that the actual result may be totally different) :

The types

`τ`

are union, intersections and difference of basic types (`int`

,`bool`

, ...) and arrow ("function") types (and type variables`α, β, …`

and universally quantified types`∀ α. τ`

). Here "union", "intersection" and "difference" can be interpreted in a set-theoritic way : an expression`e`

is of type`τ|σ`

(τ "union" σ) if it is of type`τ`

or of type`σ`

. Likewise, it is of type`τ & σ`

(τ "inter" σ) if it is of type`τ`

and of type`σ`

at the same time, and it is of type`τ \ σ`

if it is of type`τ`

and not of type`σ`

.A function whose argument can be of type

`τ`

or of type`τ'`

and which returns a type`σ`

will have type`(τ | τ') -> σ`

. This type is equivalent to the type`(τ -> σ) & (τ' -> σ)`

. This means that this function can be considered as a function from`τ`

to`σ`

or as a function from`τ'`

to`σ`

.

x: if isInteger x then toString (1 - x) else if isBool x then toString (!x) else raise "Invalid argument"

would have type `(int|bool) -> string`

(or ```
(int -> string) & (bool ->
string)
```

which is equivalent). Note that although the argument x has type
`(int|bool)`

outside the "if", the expressions `1-x`

and `!x`

are both well
typed. This requires type-checker to be able to infer that in the first branch,
`x`

can only be of type `int`

(because `isInteger`

is true), and only of type
`bool`

in the second.

In the same vein, the function

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

would have type `(int -> string) & (bool -> bool)`

.

Those types are slightly different from what one may find in an ML-like type system where both functions would be ill-typed, and thus will require a different formalism.

This formalism will also require the addition of gradual typing (*ie* adding a
special type `?`

called the *gradual type* which means "I don't know how to
type this, so I rely on the programmer not to mess with it"), because every
correct code can't be typed, and nix expressions are full of correct but almost
impossible to type constructions.