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.

Current work

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.

Overview of a possible type system for functions

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) :

For example, the function

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.


Commentaires