3 ms·

Contracts in Nix

105 points by todsacerdoti 9mo ago

bojo 9mo ago
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.
- mananaysiempre 9mo ago
  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.
- deleted 9mo ago
  [deleted]
- yakshaving_jgt 9mo ago
  Have you tried enabling Reader Mode in your browser?
  - bmacho 9mo ago
    Does not work nice with code blocks. But here's how you can add Javascript Snippets to every webpage via Tampermonkey: // ==UserScript== // @name JS Snippets // @match *://*/* // @grant GM_registerMenuCommand // ==/UserScript== GM_registerMenuCommand("Set font to default", () => { document.querySelectorAll("body *:not(pre *)").forEach(el => { el.style.fontFamily = "nonExistentFont"; }); }); you can run them by clicking the Tampermonkey icon and picking the action you want. You can add website dependent snippets by checking the location before you register the menu items, it's dynamic.
lmm 9mo ago
Meh. Runtime assertions are a poor substitute for a type system, even if you give them a type-system-like syntax.
- TheDong 9mo ago
  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.
  - _kb 9mo ago
    This is a really good take. I think the core caution is this is not type-level checks. Anything this validates still needs to be eval'd. It's not a guarantee of correctness for all inputs but does look to be a fairly light (and useful) tool to make unexpected states easier for you and others to identify.
- anon291 9mo ago
  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.
  - 9mo ago
boycothn 9mo ago
[flagged]
koiueo 9mo ago
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.
sermah 9mo ago
Fun obscene fact! This site’s domain is sraka.xyz. In russian “sraka” is transliterated as “срака” which literally means ass.
- sznio 9mo ago
  in Polish its a vulgar term for "diarrhea"
bjackman 9mo ago
I was a bit skeptical at first coz my experience so far has been that Nix's weak typing quite rarely causes me problems. (Likely because NixOS options tend to be how I communicate between pieces of code, and those have a good enough type system). But actually I think, as something that you just use occasionally like in your JSON example, this could be really cool. I wouldn't wanna use it as "gradual typing" in the sense of aiming to gradually type a whole body of code I think I would be more interested in "selective typing". Just occasionally when you get that itch of "ugh this will fail really ungracefully if the inputs are bad" then you just apply this where it's needed.
OneDeuxTriSeiGo 9mo ago
Is this related to the Contracts RFC[1] and associated implementation[2] or is it its own freestanding work unrelated to upstream efforts? 1. https://github.com/NixOS/rfcs/pull/189 https://github.com/NixOS/rfcs/pull/189 2. https://github.com/NixOS/nixpkgs/pull/485453 https://github.com/NixOS/nixpkgs/pull/485453

105 points by todsacerdoti 9mo ago

bojo 9mo ago

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.

mananaysiempre 9mo ago
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.
deleted 9mo ago
[deleted]
yakshaving_jgt 9mo ago
Have you tried enabling Reader Mode in your browser?
- bmacho 9mo ago
  Does not work nice with code blocks. But here's how you can add Javascript Snippets to every webpage via Tampermonkey: // ==UserScript== // @name JS Snippets // @match *://*/* // @grant GM_registerMenuCommand // ==/UserScript== GM_registerMenuCommand("Set font to default", () => { document.querySelectorAll("body *:not(pre *)").forEach(el => { el.style.fontFamily = "nonExistentFont"; }); }); you can run them by clicking the Tampermonkey icon and picking the action you want. You can add website dependent snippets by checking the location before you register the menu items, it's dynamic.

lmm 9mo ago

Meh. Runtime assertions are a poor substitute for a type system, even if you give them a type-system-like syntax.

TheDong 9mo ago
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.
- _kb 9mo ago
  This is a really good take. I think the core caution is this is not type-level checks. Anything this validates still needs to be eval'd. It's not a guarantee of correctness for all inputs but does look to be a fairly light (and useful) tool to make unexpected states easier for you and others to identify.
anon291 9mo ago
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.
- 9mo ago

boycothn 9mo ago

[flagged]

koiueo 9mo ago

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.

sermah 9mo ago

Fun obscene fact! This site’s domain is sraka.xyz. In russian “sraka” is transliterated as “срака” which literally means ass.

sznio 9mo ago
in Polish its a vulgar term for "diarrhea"

bjackman 9mo ago

I was a bit skeptical at first coz my experience so far has been that Nix's weak typing quite rarely causes me problems. (Likely because NixOS options tend to be how I communicate between pieces of code, and those have a good enough type system). But actually I think, as something that you just use occasionally like in your JSON example, this could be really cool. I wouldn't wanna use it as "gradual typing" in the sense of aiming to gradually type a whole body of code I think I would be more interested in "selective typing". Just occasionally when you get that itch of "ugh this will fail really ungracefully if the inputs are bad" then you just apply this where it's needed.

OneDeuxTriSeiGo 9mo ago

Is this related to the Contracts RFC[1] and associated implementation[2] or is it its own freestanding work unrelated to upstream efforts? 1. https://github.com/NixOS/rfcs/pull/189 https://github.com/NixOS/rfcs/pull/189 2. https://github.com/NixOS/nixpkgs/pull/485453 https://github.com/NixOS/nixpkgs/pull/485453