Sur les crédences, au salon vide : nul ptyx
Aboli bibelot d'inanité sonore,
Car le Maître est allé puiser des pleurs au Styx
Avec ce seul objet dont le Néant s'honore.
Stéphane Mallarmé, Sonnet en -yx.
A type-system for the Nix language.
Ptyx is an experimental implementation of a type-system for Nix. It aims at adding some type-safety to the language in the least intrusive way possible. For this purpose, the design of the type system follows two main principles:
- The type-system must embrace as much as possible the existing patterns (provided enough type annotations) instead of enforcing new easier-to-type patterns,
- Non-annotated code must typecheck with little to no modifications (although with very few static guaranties). This is made possible thanks to the use of a gradual type-system and the convention that non-annotated variables will be given the unknown type.
The project is still in early stages and not usable yet.
Implemented:
- Parsing of type-annotations
- Typing of the core language
- Recursive types
- Lists
- Records
- Gradual typing
- Clean error messages
Assuming you have stack installed, just run stack install to install the
ptyx executable in ~/.local/bin/
The project also comes with a
stack2nix-generated nix file
(which is hopefully up-to-date with the stack.yaml file). To use it, just run
nix-build from the root of the repository. The executable should be in
./result/bin/ptyx