Typing the nix language
Donation protected
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.
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.
Organizer
Théophane Hufschmitt
Organizer
Palaiseau
