Some time ago I wanted to write a Nix configuration dsl for an application I use.
My effort halted due to lack of type checking, and implementing one felt like too much effort which would never pay back.
I'll give a try.
Meh. Runtime assertions are a poor substitute for a type system, even if you give them a type-system-like syntax.
I think it's more nuanced than that.
For a long-running program, like a network service or whatever, yes absolutely runtime assertions are a poor substitute.
For an impure program, where which branches of code are hit or aren't hit depends on the result of network calls, filesystem state, user input, etc, then yes, a type-system will be more powerful.
However, nix is more-or-less pure. By fully evaluating the output, you can hit all of the non-dead code, and hit every runtime assertion every time.
For a completely pure program, runtime and compiletime might as well be the same, running it and caching the output is the exact same as compiling it, and if it fails to run and outputs an error, that's the same as it failing to compile.
I know the "more-or-less pure" is doing a lot of work there, and in reality there's a lot of bits that aren't really pure, but it's close enough that a runtime type system gives you a lot more than you'd get from one in a traditional language.
Nix already has a ton written in it and it works... Magically.
Gradual typing for a system like this is the proper thing to do. You can always write a static linter for sections you need tested and maybe eventually you'll be able to type nixpkgs as well.
Any solution to the nix typing problem NEEDS graduality. Nixpkgs is too large to make it possible to have one commit that fixes everything. Starting from scratch is not a realistic option either.
Maybe you need graduality, sure. Plenty of systems (e.g. Typescript) have added a real type system that works gradually onto an existing system. While there are compromises to that approach, it's still a lot more effective than contracts IME.
[dead]
Sorry to be that guy. I love nix, I want to read more about how people use nix.
The font presented under NixOS + Firefox is near unreadable on this website.
The font (family) is a variant of Computer Modern. Computer Modern is, unfortunately, an extreme example of the problem where a font designed to compensate for ink spread on physical paper looks overly thin on a computer screen. It is also, unfortunately, one of the very few free fonts with good support for mathematics.
Looks amazing!
Some time ago I wanted to write a Nix configuration dsl for an application I use. My effort halted due to lack of type checking, and implementing one felt like too much effort which would never pay back.
I'll give a try.
Meh. Runtime assertions are a poor substitute for a type system, even if you give them a type-system-like syntax.
I think it's more nuanced than that.
For a long-running program, like a network service or whatever, yes absolutely runtime assertions are a poor substitute.
For an impure program, where which branches of code are hit or aren't hit depends on the result of network calls, filesystem state, user input, etc, then yes, a type-system will be more powerful.
However, nix is more-or-less pure. By fully evaluating the output, you can hit all of the non-dead code, and hit every runtime assertion every time.
For a completely pure program, runtime and compiletime might as well be the same, running it and caching the output is the exact same as compiling it, and if it fails to run and outputs an error, that's the same as it failing to compile.
I know the "more-or-less pure" is doing a lot of work there, and in reality there's a lot of bits that aren't really pure, but it's close enough that a runtime type system gives you a lot more than you'd get from one in a traditional language.
Nix already has a ton written in it and it works... Magically.
Gradual typing for a system like this is the proper thing to do. You can always write a static linter for sections you need tested and maybe eventually you'll be able to type nixpkgs as well.
Any solution to the nix typing problem NEEDS graduality. Nixpkgs is too large to make it possible to have one commit that fixes everything. Starting from scratch is not a realistic option either.
Maybe you need graduality, sure. Plenty of systems (e.g. Typescript) have added a real type system that works gradually onto an existing system. While there are compromises to that approach, it's still a lot more effective than contracts IME.
[dead]
Sorry to be that guy. I love nix, I want to read more about how people use nix.
The font presented under NixOS + Firefox is near unreadable on this website.
The font (family) is a variant of Computer Modern. Computer Modern is, unfortunately, an extreme example of the problem where a font designed to compensate for ink spread on physical paper looks overly thin on a computer screen. It is also, unfortunately, one of the very few free fonts with good support for mathematics.