Typing the nix language

€3,575 of €3,305 goal

Raised by 33 people in 19 months
Motivation

Nix is a functional untyped and lazyly evaluated language used by the package manager of the same name.

The principal codebase using nix is the nixpkgs repository, which contains the packages descriptions for the NixOS linux distribution. This repo is verified by several CI tools, mainly a Hydra instance, which regularely checks the well-formness of the repository, by evaluating modified expressions and their dependancies.
However, those tests can't ensure the well-formness of the whole codebase, and there often are pieces of the repo whose evaluation may fail (especially in the nixos module system, which is way harder to test than the pure nix part). This is made even harder by the lazy evaluation model.

Furthermore, the structure of most nix expressions lets some hypothetic types be a rather expressive documentation, and it is a shame, not to have it available.

Proposal

The objective of this project is to design a type system suitable for the nix language and implement a − partial − type-inference system for it.

This system should be expressive enough to be used as checking tool for the language  (following the adage that "well typed programs never go wrong"), and be simple enough to be usable as a primary documentation. An  emphasis will be put on being able to cover as much as possible the whole language, using technics from gradual typing to manage some parts that are not typable (or too hard to type) by any known formalism.
The resulting tool should take the form of a standalone program/library ready to be used in a CI or integrated in an editor.

The project will be run as Theophane Hufschmitt's master thesis, and will take the form of a six month length internship between numtide (nixos consulting firm) and the CNRS (french research institute). The expected schedule is the following :

− march-april : bibliography and formalisation of the syntax of the nix language ; writing of a parser
− mai-mid july : design of the type system  and begin of the implementation
− mid july-begin of september : end of the implementation (and writing of the thesis).

A weekly report will be published to follow the advance of the project.
 
Team

Intern : Théophane Hufschmitt
Théophane is a french CS student (mostly studying programing languages design and type systems), and tiny nixos contributor.

Industrial tutor : Jonas Pfenniger
Jonas is an active nix/nixos contributor and founder of the consulting firm numtide.

Academic tutor : Giuseppe Castagna
Guiseppe is a well-known french CS researcher, specialized in type  systems and programing languages. He is particulary involved in designing set-theoric type systems which seems by far the most suitable typing system for nix.

Use of the funds

The requested amount is the minimum that is legally allowed in France for an internship (which represents roundly 500€/month), minus 1000€ that are offered as a starting point by numtide.

A sufficient amount has to be collected before january 31, which is the date at which I must submit the internship proposal to my school.
+ Read More
Dear contributors,

My internship has now began (thanks to your help !) and as promised, I'll try to post regular updates on my work on https://typing-nix.regnat.ovh/ . So if you're interested, just follow the rss feed.

Thanks again everyone !
+ Read More
Hi everyone,

The guys from tweag.io offered to fund the rest of the campaign (a big thanks to them !), so this fundraising is now completed.

The internship will last from March 20 to September. I'll send a link to a blog where you can follow the progress.

Cheers

--
Théophane
+ Read More
Hi all,

The first goal has been reached (and in an amazing time), cheers everyone !

I'll raise the goal − as I said, this goal was just the legal minimum for me to be allowed to do it (but don't worry, I'll do it regardless of how the rest of the campaign goes). So don't stop advertising this ;)

--
Théophane
+ Read More
Read a Previous Update
Be the first to leave a comment on this campaign.

€3,575 of €3,305 goal

Raised by 33 people in 19 months
Created January 9, 2017
Your share could be bringing in donations. Sign in to track your impact.
   Connect
We will never post without your permission.
In the future, we'll let you know if your sharing brings in any donations.
We weren't able to connect your Facebook account. Please try again later.
€200
Tikhon Jelvis
19 months ago

Nix with types would definitely improve my development experience!

€50
Anonymous
19 months ago
€10
Anonymous
19 months ago
Be the first to leave a comment on this campaign.
or
Or, use your email…
Use My Email Address
By continuing, you agree with the GoFundMe
terms and privacy policy
There's an issue with this Campaign Organizer's account. Our team has contacted them with the solution! Please ask them to sign in to GoFundMe and check their account. Return to Campaign

Are you ready for the next step?
Even a €5 donation can help!
Donate Now Not now
Connect on Facebook to keep track of how many donations your share brings.
We will never post on Facebook without your permission.