HN user
Be to the point.
To have your Nix-based setup reproducible across different OS (Arch, Debian, Ubuntu, WSL2, MacOS, and NixOS), and have an extensible base config that can be customized to different situations, the go-to framework is home-manager (not NixOS, which only works on NixOS, or NixOS on WSL 2).
You have implemented a form of ‘ad-hoc polymorphism’.
This is different from ‘parametric polymorphism’, which is what people call generics.
For context, see the recent HN discussion on “The Expression Problem and its solutions”:
You might be interested in nickel (https://nickel-lang.org/), which is a modern take on configuration management based on the experience of Nix/NixOS configurations: purely functional configuration, built-in validation (types & contracts), reusable (functions, modules, defaults), and in addition exports to Yaml, Json, etc.
To integrate nickel with nix, see how organist (https://github.com/nickel-lang/organist) does DevShell management.
I have not been following closely this back story, so I am not aware of such ban, or that (allegedly) Lix is Pierre Bourdon’s software.
I am not affiliated with Nix (Cppnix) or Lix.
lix [1] might be less affected. Pierre Bourdon noticed that lix refactored surrounding code 4 months ago [2], and a comment claims that this Lix commit at least patched a different vulnerability GHSA-wf4c-57rh-9pjg [3].
To use lix instead of nix, set `nix.package = pkgs.lix` in your NixOS/home-manager configurations.
[2] https://mastodon.delroth.net/@delroth/113110218127456491
[3] https://lobste.rs/s/ixb3v7/nix_2_24_is_vulnerable_remote_pri...
In Hypothesis shrinking is based on the generation process. In Hypothesis generators act a bit like 'Functors' in Haskell, ie you can map over them. (You can also filter and `<>` and do monadic binds etc.)
You are right that the generators in Hypothesis correspond to `Functor`s, so you can map over it. Indeed, in QuickCheck, its `Gen` [1] (type of `arbitrary` [2], the generator in QuickCheck) is a `Functor`, and moreover a `Monad`, so you can do monadic binds on `Gen`.
So in Hypothesis you can take a generator that produces integers, and create one that produces only even numbers by (in Haskell terms) mapping (2) over it. Now, the shrinker you get for free will also only produce even numbers.
That's not possible (or at least not easily possible) in Haskell. You would have to define at least a newtype wrapper.
Since `Gen` in QuickCheck is a `Functor`, to multiply its output by 2 to generate only even numbers, you can do this in Haskell as:
fmap (\x -> x*2) (arbitrary @Int)
arbitrary @Int <&> (*2)
Have a look at https://hypothesis.works/articles/compositional-shrinking/ and https://hypothesis.works/articles/integrated-shrinking/ for some more write-up, especially about how Hypothesis can preserve information even when shrinking past a monadic bind.
I think what you are hinting at is that, QuickCheck separates generation and shrinking, while Hypothesis combines generation and shrinking. If you prefer combining generation and shrinking, you may want to check out hedgehog in Haskell, see [3] for a discussion of this trade-off.
I think by using the `MonadGen` in hedgehog [4], you should be able to map over and bind over generators, with automatic shrinking, much like Hypothesis.
Hypothesis was first released in 2013, while hedgehog in 2017, so it is possible that hedgehog was inspired by Hypothesis or similar property-based testing libraries.
But in general, I would be surprised if such ‘functional’ APIs (map, filter, reduce, bind, etc.) could not be ported to Haskell.
[1] https://hackage.haskell.org/package/QuickCheck-2.15.0.1/docs...
[2] https://hackage.haskell.org/package/QuickCheck-2.15.0.1/docs...
[3] https://tech.fpcomplete.com/blog/quickcheck-hedgehog-validit...
[4] https://hackage.haskell.org/package/hedgehog-1.4/docs/Hedgeh...
Do you have examples where Python’s Hypothesis (and its shrinking) works better than Haskell’s QuickCheck? This would let us improve Haskell’s QuickCheck.
My understanding is that Haskell’s QuickCheck can shrink functions, and with parametric polymorphism, can work with vector types and more [1], which would be difficult if not impossible in Python.
And in general, the base types covered by the shrinking in Python’s Hypothesis should have analogues by the shrinking in Haskell’s QuickCheck. And with deriving, Haskell’s QuickCheck should get shrinking ‘for free’ as in Python’s Hypothesis.
Also, Haskell’s QuickCheck extends to stateful and parallel checking, which is not supported in Python [2].
[1] https://library.mlabs.city/mastering-quickcheck "Mastering QuickCheck: Advanced yet Practical Techniques for Property-Based Testing"
[2] https://stevana.github.io/the_sad_state_of_property-based_te... "The sad state of property-based testing libraries: A survey of property-based testing libraries"
Thanks for the information.
The linked page shows only integrating Hotwire with Ruby on Rails, giving me my original impression.
Hotwire integrates with Ruby on Rails. (EDIT: The linked page shows how to integrate Hotwire with Ruby on Rails. See fxn's comment https://news.ycombinator.com/item?id=40555577)
I had the same question, then watched the video to get the answer.
Reminds me of nix-output-monitor [1], for example see [2].
It makes it easy to understand how individual steps are progressing, and how individual steps relate to the overall plan. It enables me to locate expensive build steps, and possibly to avoid them if steps are failing.
For those on hyprland:
[1] hyprslidr: https://gitlab.com/magus/hyprslidr
[2] hyprscroller: https://github.com/dawsers/hyprscroller
Though need to extend hyprland to support layout outside viewport: https://github.com/hyprwm/Hyprland/issues/5489
Reminds me of the “Chase your reality” commencement speech by Christopher Nolan at Princeton in 2015.
Software developers often want to customize:
1. their home environments: for packages (some reach for brew on MacOS) and configurations (dotfiles, and some reach for stow).
2. their development shells: for build dependencies (compilers, SDKs, libraries), tools (LSP, linters, formatters, debuggers), and services (runtime, database). Some reach for devcontainers here.
3. or even their operating systems: for development, for CI, for deployment, or for personal use.
Nix provision all of the above in the same language, with Nixpkgs, NixOS, home-manager, and devShells such as https://devenv.sh/. What's more, Nix is (https://nixos.org/):
- reproducible: what works on your dev machine also works in CI and in prod,
- declarative: you version control and review your configurations and infrastructure as code, at a reasonable level of abstraction, to specify what the system should be, not how to get there,
- reliable: all changes (switching generations or profiles) are atomic with easy roll back.
Quoting https://nix.dev/tutorials/nix-language.html:
The Nix language is designed for conveniently creating and composing derivations – precise descriptions of how contents of existing files are used to derive new files. It is a domain-specific, purely functional, lazily evaluated, dynamically typed programming language.
1. domain-specific: designed for conveniently creating and composing derivations. This reason alone already justifies a new language, or an embedded domain-specific language (embedded in the Guile/Scheme for guix), or a mix of both (Starlark, the build language of Bazel embedded in a restricted Python-variant).
2. purely functional: this underlies the philosophy of the Nix package manager, which aims to be purely functional (also known as hermeticity in other build systems, such as Bazel). Being purely functional in turn underlies the congruence of the NixOS operating system, where you declare what the state the system should be in (as opposed to being convergent, so that you specify how to achieve the desired state).
3. lazily evaluated: similar to other build systems (including Bazel), so that you can build only what you need on demand.
4. dynamically typed: this one is controversial. Being dynamically typed—in other words, not developing a type system—gets Nix out of the door 20 years ago. But users often complain about the lack of proper types and modularity. There are experiments to add a type-and-contract system to Nix, such as Nickel (https://github.com/tweag/nickel).
Most of the above are also listed in the Overview of the One Pager.
Chris, how would you respond to the remark that the article is comparing a flawed Mojo implementation against a more correct Rust implementation? https://news.ycombinator.com/item?id=39296559
Insightful Reddit comment https://old.reddit.com/r/rust/comments/1al8cuc/modular_commu...
> The TL;DR is that the Mojo implementation is fast because it essentially memchrs four times per read to find a newline, without any kind of validation or further checking. The memchr is manually implemented by loading a SIMD vector, and comparing it to 0x0a, and continuing if the result is all zeros. This is not a serious FASTQ parser. It cuts so many corners that it doesn't really make it comparable to other parsers (although I'm not crazy about Needletails somewhat similar approach either).
> I implemented the same algorithm in < 100 lines of Julia and were >60% faster than the provided needletail benchmark, beating Mojo. I'm confident it could be done in Rust, too.
Does elixir have an lsp as good as Typescripts? I’m a bit addicted to static types at the moment.
I wonder how IHP [1], the liveview in Haskell, compares with Phoenix liveview for typical use cases now. (Not having used either.)
Some of these interactive simulations for learning are called “Explorable Explanations” [1], coined in 2011 by Bret Victor, the author of your second link (worrydream.com), which also talks about “Explorable Explanations”.
For more examples, see [2].
Very much agree that this is what explanations and presentations should be in the modern age. I think a documentation language (what Nota and Typst aim to be) is still needed in this age of Large Language Models, when the ideas are more complex than those expressible by natural languages.
As Nix Flakes become more prevalent, perhaps there needs to be some way to containerize them.
You may be interested in nix snapshotter, which can run nix packages in containerd.
Liquid Types [1] achieve the same in existing programming languages: no bounds checks at runtime, and reject programs without an in-bounds proof.
For a demo, see "Scrap your Bounds Checks with Liquid Haskell", giving a 6x speed up in high-performance parsing of UDP packets.
[1] https://news.ycombinator.com/item?id=37349276 "A Gentle Introduction to Liquid Types"
[2] https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Scrap your Bounds Checks with Liquid Haskell"
But why have a separate type system instead of just building it into the language.
Excellent question. The existing "mainstream" languages (C++, Rust, Julia, or even Haskell) are not designed to support such applications as bound checks or pointer checks in their type systems, where certain runtime values/checks can affect/refine the types (as in dependent types, or refinement types which Liquid Types are based on).
It could be done (in some newer languages: Idris, Agda, Lean), but people have not figured out an ergonomic way to do so in more "mainstream" languages (e.g., not hurting type inference, light and maintainable proof burdens). Liquid Haskell is an attempt to bring refinement type to Haskell, as an extrinsic type system.
C++ could build in pointer checks and it would be in the same type system.
People have not figured out how to do so (and I doubt if it is possible at all). Suffice to say:
* Rust is an attempt to build in lifetime-and-ownership-checks into the type system of C++, and Rust is a new language,
* Liquid Rust is an attempt to add pointer checks (refinement types) to Rust, and even then it is not built into Rust.
And with _this_ rebuttal, the issue is now double settled.
People are still researching solutions (see Rust and Liquid Rust over C++) to this problem (building in pointer checks in the type system of C++), and they would love it if you can settle their problems.
(Can't resist this one line rebuttal)
So your solution is to rewrite the haskell standard library yourself?
No need--the simplest solution is to pass flags correctly to the dependent library (set all flags BoundsChecks, UnsafeChecks, and InternalChecks to false for the vector package) for release builds.
Explanation after the one-line rebuttal:
This exactly matches the C++ behavior: no bound checks for release builds, but with bounds checks for debug builds. This shows that Haskell can do what C++ can do, very easily, just by passing compiler/cabal/stack flags correctly.
With this rebuttal, I think the issue is completely settled, at least for reasonable readers.
C++ doesn't have bounds checks in the std library in release builds by default, so you can't get better than that.
In Haskell you can provide your own prelude, which uses unsafe functions without bounds checks by default. With CPP or cabal tricks, you can easily have bounds checks only for debug builds, but no bounds checks for release builds. No Liquid Types needed either, though this is only testing in development but not compile time verification. Less safe, but same effort and result as in C++.
loops and bounds checks are complex in the first place isn't true.
Liquid Types people are not thinking about only loops and bounds checks. They think about any properties, for example:
* pointer checks, a huge security issue, see [1] or https://news.ycombinator.com/item?id=37376946.
* valid expression checks (Beyond Bounds Checking of [2]), see https://news.ycombinator.com/item?id=37440896.
[1] https://arxiv.org/abs/2207.04034 "Flux: Liquid Types for Rust"
[2] https://www.tweag.io/blog/2022-01-19-why-liquid-haskell/ "Why Liquid Haskell matters"
Sorting 5 numbers is complex in the first place isn't true. No other technology invests so much complexity as programming and this is barely an issue in modern problem solving in the first place.
My previous comments already said loops and bounds checks are not complex in the first place, and they are only used as a demo in a talk, as Liquid Types scale to handle any properties.
I am pretty certain that a reasonable reader can judge the merits of our arguments and make up their mind. Thanks for raising a possible misconception about Haskell and Liquid Types, and this forced me to strengthen the arguments to clear the misconception for other reasonable readers. This is my last comment on this issue.
It is not fair to think this is a complication specific to Haskell, because you can opt-out of runtime bounds checks as easily as C++, Rust, and Julia, with functions such as unsafeTake and unsafeDrop.
https://news.ycombinator.com/item?id=37382215
If you can afford runtime checks (if they are not much of an issue in the first place), Haskell, C++, Rust, and Julia can have runtime checks.
https://news.ycombinator.com/item?id=37387005
It is unfair to not respond to these points, while calling "this is a complication specific to Haskell." Because Haskell can do what others can do, but more.
lots of complexity for something simple.
"indexing an array of length 8" for parsing UDP headers is simple, agreed. And Haskell can handle that simply with unsafe functions.
Keeping track of properties with complicated dependencies to parse arbitrary content (perhaps application-logic-aware contents, not "just checking for array length before indexing in a loop") is simple, strong disagree. See the section "Beyond Bounds Checking" of "Why Liquid Haskell matters" for example [1]. This might be used to implement the kinds of static analysis needed for Mojo or Swift, for instance [2].
[1] https://www.tweag.io/blog/2022-01-19-why-liquid-haskell/ "Why Liquid Haskell matters"
[2] https://github.com/modularml/mojo/discussions/466 "Mojo and Dynamism"
https://news.ycombinator.com/item?id=37376010
And this cannot be solved in the languages you mentioned, either. Unless you are claiming that all parsing checks are "just checking for array length before indexing in a loop".
https://news.ycombinator.com/item?id=37416911
We are still working on completely different scales.
The talk is using a toy example to show what is possible, and you are using that example too literally, without realizing that the example scales to handle much more complex problems that people need to deal with in the real world.
It is unfair to lump together different scales and call them the same thing.
Your reaction is like criticizing a talk which shows sorting 5 numbers with programs, with "it is simple to sort 5 numbers by hand, why bother learning how to program with all those complexity for something this simple?". And then calling this fair, without realizing that in the real world, sometimes people need to sort way more than 5 numbers.
I think the main confusion is that, "Scrap your Bounds Checks with Liquid Haskell" presented a toy example/implementation which scales to real implementations, for the task of high-performance parsing of UDP packets (used by Awake Security, I guess).
The toy example/implementation is chosen to teach Liquid Types/Haskell, and therefore, covers the simple case of parsing UDP headers, which is a simple bounds check of "indexing an array of length 8". In this case, there is no need to use Liquid Types in any language.
But in the real use case (not shown in the talk), when you want to dig deeper into the content of UDP packets and such, you will need more than "check the input data (length) ahead of time so that you don't have to check the range in the middle of a loop". This is the case where Liquid Types help, tremendously. But such complicated cases, where Liquid Types shines, may not fit into a talk.
Again, it is not fair to think this is a complication specific to Haskell.
static analysis isn't going to deal with every scenario like access based on inputs.
Not true.
With proper abstraction, static analysis proves the absence of bugs under all relevant inputs, which gives stronger guarantees than testing at development time (which only checks for a number of inputs), and is more performant than runtime checks (without runtime overhead).
An example is the use of a static type system, which eliminates a whole class of bugs under all possible values of the same type (those due to type mismatch: passing a string into a function expecting an integer), which is stronger than a test suite testing certain inputs, and does not have runtime overhead (unlike runtime checks).
Going further than usual type systems, people study refining types by possible values (such as positive integers as a refinement of all integers), and the result is refinement types, which is what Liquid Types is based on. And you can see this in action in the full example [1], such as { n : Int | 0 <= n } which refines n to be a positive integer.
[1] https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Full program - Scrap your Bounds Checks with Liquid Haskell"
Lumping them together is pretending there is something happening that isn't.
Correct. Static analysis can formally verify correctness under every access (like runtime checks), but without the runtime overhead (unlike runtime checks), with proper abstraction.
That is why compile time verification is an upgrade from runtime checks.
OK, in reality the trick is that static analysis removes redundant runtime checks (check exactly once), see the sibling discussion https://news.ycombinator.com/item?id=37376963.
PS: I figured that setting the record strict may benefit others, such as https://news.ycombinator.com/item?id=37380176, hence this reply.
Thanks for the great note, I learned something today.
this seems like a lot to go through to solve something that isn't much of an issue in the first place...but with more explicit iteration and runtime checks they are almost never a problem I see anymore.
If you can afford runtime checks (if they are not much of an issue in the first place), Haskell, C++, Rust, and Julia can have runtime checks.
If you want to opt-out of runtime checks, Haskell, C++, Rust, and Julia can opt-out easily, but unsafely.
So, to be fair to Haskell or any of them, this is not a complication specific only to Haskell.
But Haskell enables you to do more. With around 30 lines of Liquid Haskell (those lines between {-@ and @-}), you can upgrade simple runtime checks to compile time verification, see the full example [1]. You get great efficiency, safely, without unnecessary runtime checks, which is impossible in C++, Rust, or Julia without Liquid Types.
[1] https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Full program - Scrap your Bounds Checks with Liquid Haskell"
C++ doesn't have this problem at all, bounds checks are in the std library in debug mode only. Rust and Julia make it very easy to take the bounds checks out.
Haskell can do that too, with unsafeTake and unsafeDrop [1], you can opt-out of runtime bounds checks as easily as C++, Rust, and Julia. But opting-out of machine-checked guarantees is unsafe, and Haskell can do better.
What's more is that Liquid Haskell can move such runtime bounds checks to compile time, made ergonomic with SMT solvers. This way, you get machine-checked guarantees (so programmers can write correct programs faster) with no runtime overhead (the programs also run faster).
Also if you are accessing a data structure out of bounds, that's a show stopping bug that shouldn't ever happen. That should be something that is prevented ahead of time, not recovered from.
Yes, that's the whole point of static analysis, to move runtime checks to compile time, made ergonomic with Liquid Types. Note that this compile time verification is much stronger than testing at development time, which is what C++, Rust, and Julia offer without Liquid Types.
That should be something that is prevented ahead of time, not recovered from.
Gabriella Gonzalez agrees with you, and calls this idea of "Prefer pushing fixes upstream over pushing problems downstream" as "The golden rule of programming", at the 1st slide in her talk [2]. Her talk shows you how such machine-checked verification is possible with Liquid Haskell, which is not possible in C++, Rust, and Julia without Liquid Types.
[1] https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Documented preconditions - Scrap your Bounds Checks with Liquid Haskell"
[2] https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Scrap your Bounds Checks with Liquid Haskell"