3 ms·
> Something that is emblematic of the problem: Nix has an implication operator. That's something that virtually no other language supports - it's normally somet
by chriswarbo 3y ago
> Something that is emblematic of the problem: Nix has an implication operator. That's something that virtually no other language supports - it's normally something found in formal verification systems.
I wholeheartedly disagree. Nix's `a -> b` is just a boolean function, like `&&`, `||`, `==`, etc. It's meant for assertions, e.g.
assert format == "csv" -> depth data == 2;
Most languages allow assertions like this; they'd just be more awkward, like
assert(depth(data) == 2 if format == "csv" else True)
In fact, a common complaint about the Nix language is that it's untyped: which shows just how informal it is!
> The Nix language is designed by people that think everyone is familiar with lambda calculus and function programming. That's fine. But it's crazy to use a language like that for something that everyone has to use.
The Nix language is basically just "JSON with functions" (although the syntax is unfortunately different, since JSON wasn't so popular back around 2003; it does support XML though!). There's only an emphasis placed on functions since they're the USP of the language; otherwise we could just use plain JSON. Lambda calculus is just a simple model of functions; you don't need to know or care about it in order to write functions in the Nix language. In the same way that you can write integer arithmetic in Nix without knowing Peano's axioms, or von Neumann's set encoding of ordinals, or whatever.
I've not used Starlark, but it seems to be waaaay more complicated than "JSON with functions"; e.g. it has loops, which makes the semantics dependent on some notion of time/temporal-ordering, which is sounds like a massive headache.