one-punch

Liquid Types enabled a 6x speed up in high-performance parsing of UDP packets, according to "Scrap your Bounds Checks with Liquid Haskell" of Gabriella Gonzalez [1].

With Liquid Haskell, the bound checks are moved from runtime to compile time, semi-automatically handled by SMT-solvers. Static types help programmers to write correct programs faster, and the programs also run faster.

As an aside, speeding up programs with static analysis (constrained dynamism) are also present in Mojo (a variant of Python) or Swift [2].

[1]: https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Scrap your Bounds Checks with Liquid Haskell"

[2]: https://github.com/modularml/mojo/discussions/466 "Mojo and Dynamism"

Yes, but I meant the trend set by Vision Pro may spill over to similar (commodity) hardware, and we may need to interact with 3D Linux “desktop” in the future.

My wish is a scrollable-tiling Wayland compositor (Niri or otherwise) to have nice animations (think hyprland or wayfire), compositionality/extensibility (IPC sockets of hyprland, and lately wayfire), and optionally be 3D-aware (wayfire, to future-proof when Vision Pro becomes trendy :-) )

PS: I am not affiliated with the repo in anyway, but think that scrollable-tiling should be better known.

Monads are there in computations that we care about, regardless of the implementing programming languages (e.g., Python, C, Assembly, Turing Machines). Just that Haskell is famous for considering Monads as a first class concept, while many programming languages do not name and reason about them (in Python, C, Assembly, etc.).

This is similar to structured loops and function calls (not GOTO), which are in computations that we care about, regardless of the implementing programming languages. Some languages do not name and reason about them (e.g., Assembly, Turing Machines).

While it is possible to program without raising the level of discourse, this is discouraged (considered harmful), as it lacks safety, hurts productivity (developer velocity/experience), and scales worse.

> > when you start considering effectful computation at a deep level, monads come up pretty quickly

> You say that, but they only seem to come up when dealing with haskell.

"when you start considering structured computation at a deep level, loops and function calls come up pretty quickly"

"You say that, but structured loops only seem to come up when dealing with high level languages."

This situation, where a higher level programming language delivers more power (in this case, scales with better developer velocity/experience) but a lower level programmer resists, has been observed many times. Paul Graham calls this the Blub Paradox [1].

    What's so great about Lisp? And if Lisp is so great, why doesn't everyone use it?...

    I'll begin with a shockingly controversial statement: programming languages vary in power.

    ... But when our hypothetical Blub programmer looks in the other direction, up the power continuum, he doesn't realize he's looking up. What he sees are merely weird languages. He probably considers them about equivalent in power to Blub, but with all this other hairy stuff thrown in as well. Blub is good enough for him, because he thinks in Blub.

And using a powerful high level language is "The Secret Weapon" behind the success of Viaweb [1]. Haskell is also a secret weapon for those who know how to use it.

[1]: http://www.paulgraham.com/avg.html "Beating the Averages"

Glass dip pens are easier to clean than fountain pens, especially for shimmering inks.

The pens themselves also allow for different/more playful artistic expressions than fountain pens, due to very disparate materials. It may not be for everyone, but some anime-themed glass dip pens are a hit in certain groups near Japan.

Some examples from someone I know, showing the glassy characters:

https://www.instagram.com/glassophy_bunbou/

The second chart is bucketed by year, while the first chart is not (appears to have more continual changes). Also, the discrepancy you observed around 2023 is on the edge of the second chart, which can be the result of bucketing and it may not be that surprising after all.

> If so then we should look at the slope of the graph for 'growth', and it in fact appears to have flattened recently.

The second graph shows the number of job posts per year, and it seems to reflect the bigger macro-economic situation: dip during pandemic, and a slight drop after 2022. I think these features are not specific to Haskell, just showing that the Haskell segment also follows some bigger trend.

Linear Type/Arrow makes sure values are consumed exactly once (as they cannot be duplicated nor destroyed), and such runtime can be used for efficient resource management without reference counting or garbage collection [1].

For Linear Type/Arrow in Haskell, see [2][3][4]. For Linear Type (or Relevant Type) in Rust, see [5].

[1]: https://news.ycombinator.com/item?id=16100840 "Linear types can change the world"

[2]: https://www.tweag.io/blog/2017-03-13-linear-types/ "Linear types make performance more predictable"

[3]: https://www.tweag.io/blog/2023-01-26-linear-constraints-free... "Linear Constraints: the problem with O(1) freeze"

[4]: https://www.reddit.com/r/haskell/comments/v3gouc/linear_text... "Linear Text Builder: up to 20x faster than alternatives"

[5]: https://faultlore.com/blah/linear-rust/ "The Pain Of Real Linear Types in Rust"

Golang prioritizes compile time (hence it took them so long to get Generics), which Rust and Haskell are unlikely to beat, as they both prioritize high-levels of abstractions (more compile time for zero cost abstractions at runtime).

That said, since GHC is implemented in Haskell, the compile time will likely improve if linear type/arrow, or a better runtime (such as optimal reductions), is used by GHC itself.

> I really wished there was a GC-ed but strictly-evaluating Haskell.

To answer this question literally, there are PureScript (transpile to JavaScript), Idris (dependently typed), OCaml, and Standard ML (as discarded1023 pointed out).

But I think the wish for a strictly-evaluating Haskell is sometimes in fact a wish for a Haskell with more predictable performance (especially in memory usage). If so, the Linear Type/Arrow of recent GHC may fit the bill [1].

My wish is for Haskell to have a better runtime [2] with optimal reductions (with more predictable performance and without GC) [3], which could have Rust-like performance without lifetimes, while being lazy.

[1]: https://www.tweag.io/blog/2017-03-13-linear-types/

[2]: https://discourse.haskell.org/t/high-order-virtual-machine-h...

[3]: https://github.com/HigherOrderCO/HVM

> For example, if you Ctrl-C while its downloading an update, you get in a weird state where nothing works. …

There is a new Nix installer from Determinate Systems, a company heavily invested in Nix, which should make installing Nix more atomic, reversible, and thus easier:

The Determinate Nix Installer https://news.ycombinator.com/item?id=34957953

And after getting pass the installation, Nix is great for production.

An alternative to have both `shfmt` and `shellcheck` and all pre-commit hooks managed (that is, automatically installed until no longer used and garbage collected) is to use https://devenv.sh/.

After `devenv init`, update `devenv.nix` as follows:

    { pkgs, ... }:

    {
      pre-commit.hooks = {
        shellcheck.enable = true;
        shfmt.enable = true;
      };
    }

> Nix has an install step to use a package

Not true. See "Using Nix to run software with no installation steps" https://determinate.systems/posts/nix-run for example.

This feature has been one of the main use cases of Nix.

> Nix has an install step ... AppFS does not... I'm the author of AppFS.net...

I appreciate the disclosure, as it helps readers (like me) to judge the merits of your claims, especially regarding AppFS vs other options, and whether those claims could be biased (due to differences in familiarity, for example).

> I'm not sure what kind of disclosure is needed...

Over Hacker News and other forums, when the author of a tool wants to promote their work (nothing wrong with this, I learnt a lot with such promotions) in the context of competing tools, the following disclosures are common:

1. Disclosure: I wrote AppFS.

2. Author of AppFS here. (Just like what you did.)

3. Shameless plug. (Note: I personally do not see this as a shame, but I just want to give examples of common disclosure styles in such contexsts.)

> There’s no shebang support in nix3.

This is a pain point, but there appears to be discussions and a PR for Shebang support with flakes: https://github.com/NixOS/nix/pull/5189

1. Not sure how AppFS could have lower overhead than Nix in terms of removing the install step.

2. AppFS appears to be written by a user named rkeene, and I am replying to a comment by rkeene2. I think a disclosure would be helpful when comparing AppFS with other tools.

(disclosure: not a PL person, so my question could be really dumb.)

> Informally, a function is type stable if the type of the output depends only on the types of the inputs, not their values.

This line reminds me of (the opposite of) dependent-type. But I think that intuition may not be useful or relevant for understanding here?

TL;DR: Can we have an experience similar to `guix refresh` with content-addressed nix?

(Disclosure: experimenting with the content-addressed nix now, have not used guix before, but heard good things about it.)

It seems to me that there are some higher-level design decisions around usability that need to be worked out, concerning the push to content-addressed nix and making all build dependencies pure in restricted mode (to separate “fetching from external services with known hash” from “building without accessing external services”), particularly to interface with other language ecosystems (crate2nix of Rust, cabal2nix of Haskell, yarn2nix of Node, etc.), as summarized in this “Status of lang2nix approaches” discourse thread [1].

[1]: https://discourse.nixos.org/t/status-of-lang2nix-approaches/...

I wonder what is the intended user flow for updating hashes of dependencies (say, from a certain language ecosystem).

Can we make it as easy as `guix refresh`, possibly with tools external to nix (similar to niv, lorri, and other nix-related tools which extend nix)?

Before the restricted mode in content-addressed nix, we could do, say, callCabal2nix which indirectly does import-from-derivation (IFD), that is, refer to an intermediate derivation which is computed. With the push to content-addressed nix, this appears to be ruled out (see the thread [1] for the alternatives, but it seems that there is no satisfactory approach yet).

If we want to make it easy to update dependencies with a single command (like `guix refresh`), what needs to be done? Do we need to change nix to accommodate, or we could do it with external tools alone (like the way niv and lorri which “patch” the nix workflow without modifying nix proper).

> Starbucks and ... use it

I have heard of Haskell used in companies mentioned by other comments, but I am surprised, pleasantly, that Starbucks uses Haskell.

Do you have a pointer (job posting, blog post, etc.) to Starbucks using Haskell? It could help me push for using Haskell by my employer, for example.

This is new to me.

I have heard of Haskell used in companies mentioned by other comments, but I am surprised, pleasantly, that Starbucks uses Haskell.

Do you have a pointer (job posting, blog post, etc.) to Starbucks using Haskell? It could help me push for using Haskell by my employer, for example.

> I hate that brew is good enough that it’s got some kind of local maximum such that there’s no replacement forthcoming.

You may be interested in trying out nix for package management [1], or even for configurations and providing development environments (see my other comment [2]).

[1]: https://builtwithnix.org/

[2]: https://news.ycombinator.com/item?id=26038614

I use nixpkgs and home-manager for a consistent package management and configuration across MacOS and Linux (NixOS), which others also reported great success [1]. As noted in the article [1], home-manager has a steeper learning curve, but is much more powerful (e.g., supports providing development dependencies and environment, or even extend to Ops).

For the interested, search for some variants of “homebrew home-manager nix”, and you may find lots of resources [2][3][4].

[1]: https://lucperkins.dev/blog/home-manager/

[2]: https://www.softinio.com/post/moving-from-homebrew-to-nix-pa...

[3]: https://wickedchicken.github.io/post/macos-nix-setup/

[4]: https://dev.to/louy2/use-nix-on-macos-as-a-homebrew-user-22d

While I agree that science should aim for replicability (same result for similar methods on the same scientific question) instead of reproducibility (same methods) [1], it does not hurt to let others to reuse part of your research pipeline.

I think we can in fact test and improve replicability if the whole pipeline is published. We should aim for allowing others to change certain parameters or data in the pipeline. That is, the result should be robust with respect to minor changes in the pipeline, which could be more easily tested by others with a published, fully specified pipeline.

Referring to my other comment [2], Guix or Nix really shine in allowing others to change part of the pipelines, due to their functional approach to composing components.

[1]: https://phys.org/news/2019-05-replicability-science.html

[2]: https://news.ycombinator.com/item?id=25866651

You might be interested in using Guix [1] for reproducible research, as is reported earlier (for genomics analysis) [2] and still actively developed [3].

As a bonus, Guix and Nix [4] allow for modular and composable pipelines, where you can swap different components (such as to upgrade Python from 3.8 to 3.9, or to enable certain optimizations for some Python libraries, or to run on MacOS and Linux while keeping the whole stack more or less the same), which would be more difficult to do reproducibly with other tools such as Docker (composing Guix or Nix functions are easier than composing DOCKERFILE or Docker Compose).

[1]: https://ambrevar.xyz/guix-advance/

[2]: https://academic.oup.com/gigascience/article/7/12/giy123/511...

[3]: https://hpc.guix.info/blog/2020/11/hpc-reproducible-research...

[4]: https://builtwithnix.org/

The integration with fzf seems nice.

Any plans to integrate with skim, a Rust implementation of fzf?

https://github.com/lotabout/skim

An expressive language should let programmers reason about code, including parsers, for their correctness.

You know it is correct when you see it, and you get more confidence in not making silly mistakes with unit tests. This is a different approach to formal verification using logic solvers or theorem provers.

For an example of parsing with Haskell, see this recent discussion: https://news.ycombinator.com/item?id=25212372

This approach, as hinted in Parse, Don’t Type-Check, is to raise the level of abstraction. The jargons are to create a domain-specific language (DSL) to model the problem, as in language-oriented programming.

With this approach, you understand what the code is trying to do and can change it easily because it reads like pseudo-code. (Pseudo-code is usually a synonym for code at the right level of abstraction.)

Parser combinators showed me what an expressive language (in particular Haskell) can do to let you write code as you intend, so that maintainable code is enjoyable to read, write, and reason about.

I have heard that some people first “get” Haskell because of parser combinators.

> This might be true, but when they were making the case for constructive types they didn't mention it.

Agree.

> The discussions seems to be mostly dependent types vs refinement types, which I'd argue is a false dichotomy.

You are right, I think I confused two notions:

1. constructive vs non-constructive reasoning.

2. intrinsic vs extrinsic types (aka Church vs Curry types[ 1]).

In general, intrinsic types are constructive (because Program-is-Proof due to Brouwer–Heyting–Kolmogorov and Curry–Howard and others).

But extrinsic types could also be constructive, esp. when the external static analyzer has access to the program, such as in refinement reflection [2] (as pointed out in the above Reddit comment thread).

[1]: https://lispcast.com/church-vs-curry-types/

[2]: https://ucsd-progsys.github.io/liquidhaskell-blog/2016/09/18...

Then I think the author is arguing for constructive proofs, which come naturally with intrinsic types, or at least with extrinsic analyzers accessing program structures; and arguing against non-constructive (extrinsic) types, or anything detached from implementation.

> While this is true, I'm not sure how constructive types don't face the very same issue.

Not sure if the author claims that constructive types do not face this issue.

On constructive types vs refinement types, there is a recent Reddit discussion on this topic,[1] prompted by Facebook’s use of Dependent Haskell to eliminate bugs.[2]

[1]: https://www.reddit.com/r/haskell/comments/jh7575/eliminating...

[2]: https://www.youtube.com/watch?v=10gSoVZ5yXY

> arbitrary properties are very difficult to check in general.

To add to this:

In theory, it is not just difficult, but impossible.

Imagine that the refinement predicate is whether the String/Text encode a (non-)halting Turing machine/Haskell program. Checking it would solve the halting problem. And this predicate is the proof of Rice theorem.[1] (Granted, this may require some sufficiently powerful logic such as first order, not sure if this proof applies to LiquidHaskell.)

In practice, I think reasonably intuitive properties are already very difficult to formalize in refinement types.

The justification from the article:

"To some readers, these pitfalls may seem obvious, but safety holes of this sort are remarkably common in practice. ... Proper use of this technique demands caution and care:

* All invariants must be made clear to maintainers of the trusted module...

* Every change to the trusted module must be carefully audited to ensure it does not somehow weaken the desired invariants.

* Discipline is needed to resist the temptation to add unsafe trapdoors that allow compromising the invariants if used incorrectly.

* Periodic refactoring may be needed to ensure the trusted surface area remains small...

In contrast, datatypes that are correct by construction suffer none of these problems."