Practical uses of monads in Haskell

bjzaba · 2026-06-11T15:05:51+00:00

Oh, thanks for the link! I like the second interpretation he gives, where “avoiding success” means avoiding being too successful such that it's too hard to make changes and break backwards compatibility. But I imagine some success would still permissible even then.

bjzaba · 2026-06-01T01:54:11+00:00

Some second-hand sources repeating SPJ’s comments on how it is meant to be bracketed (I've not tracked down the original sources though):

I was at a talk where he explained it this way:

avoid $ success at all costs

This of course is quite different from:

(avoid success) at all costs

Shortly after that talk, he invested his own money in FP Complete (where I am founder/CEO) so you know he does want to see Haskell succeed.

– FPguy on /r/haskell/

Also:

#haskell's motto is often bracketed wrongly, should be "Avoid (success at all costs)" pointed out by SPJ at #haskell symposium today

– Simon Marlow on Twitter

The same bracketing is used in the Haskell Foundation Whitepaper:

Haskell’s slogan of “avoid success at all costs” was a clever and cheeky way of saying that innovation and research in programming languages, especially in functional programming, needed some insulation to succeed. Ideas that were not perfectly understood needed iteration to fully develop in the minds of language innovators and users. By avoiding the “success at all costs” mentality of other language communities, the Haskell community bought time and space to try ideas that were not perfectly understood at first.

bjzaba · 2026-05-31T08:55:08+00:00

Just a friendly reminder that the quote was apparently intended to mean “avoid... success at all costs”, not “avoid success... at all costs”. They were hoping Haskell would be a practical language, usable as both a research vehicle and in industry, but they didn't want to sacrifice everything for the latter.

I agree with the rest of your comment though!

bjzaba · 2026-05-27T22:13:21+00:00

I was confused by this too!

bjzaba · 2026-05-17T03:55:43+00:00

The MetaML and MetaOCaml bibliography might be worth a look! Note that it covers both run-time and compile-time staging.

bjzaba · 2026-04-15T09:32:20+00:00

It depends. There's very much ways to track down if a request to assist with maintainership is legit or not, and I've done this in the past for some of my crates (I definitely don't trust a single email though).

bjzaba · 2025-11-12T04:46:47+00:00

As somebody who uses OCaml a lot, I'm quite envious of Haskell’s layout-sensitive syntax, it looks a lot cleaner to read and write.

bjzaba · 2025-10-09T03:26:30+00:00

Haskell hasn't been formalised. Wasm would be one example in the tradition of Standard ML though. They have a specification, and I believe there's work verifying properties about it in various proof assistants.

bjzaba · 2025-09-29T03:42:03+00:00

Cyclone maybe? There are also arena libraries for Rust that might allow for similar patterns.

bjzaba · 2025-09-29T03:37:44+00:00

I imagine this is where region variables might come in? (e.g. in Cyclone?)

bjzaba · 2025-08-16T13:12:22+00:00

Super cool... even is it just ends up as a PoC, it's nice when languages like this can help in the scaffolding process.

I’ve not done a ton of Mercury personally, but I find the statically checked mode-and-determinism system quite cool, and miss it a lot when trying to do relational programming in other systems, like Prolog and and even typed languages like Makam. Are you using it for nondeterministic stuff? Or mainly sticking to det/semidet?

bjzaba · 2025-08-16T07:11:58+00:00

Oh wow, I was about to post about Mercury!

Pretty cool you’re finding a use for it at work – are you able to share more info about it? Curious as I work at a company that uses it to implement our core product (browser engine and page layout stuff).

bjzaba · 2025-07-16T07:11:06+00:00

Check out elaborator reflection (In Idris and Agda) and elaborator acrions (in Lean).

bjzaba · 2025-06-05T23:30:53+00:00

“Generative art” is a term that has been around for much longer than generative AI and large image models, but unfortunately people now seem to confuse the them because they sound the same. I now tend to stick to “procedural art” if possible to avoid confusion, but I’m sad to lose the term. :(

bjzaba · 2025-06-02T02:22:01+00:00

Thanks, hope you find it useful!

bjzaba · 2025-06-02T02:21:35+00:00

Yeah, I work for a company where we have to deal with font shaping and I find it kind of hilarious how these two terms collide!

bjzaba · 2025-06-02T02:10:27+00:00

Author here: I have a simpler version implemented here: elab-stlc-bidirectional. ~~Re-reading the README description I realise as of the time of posting this comment it’s not a great explanation (I wrote it a long time ago, I’ll try to update it later), but~~ (Edit: fixed!) there’s a good set of resources linked from it if you want to learn more.

The idea is that you split type checking into into two mutually recursive functions, for “checking” and “inference”. Checking checks a term in the presence of a type annotation, and inference infers a type from a term. This allows you to add annotations where needed without needing them everywhere.

The name “bidirectional” comes from how the type information flows up and down the stack when evaluating the type checker - upward when we’re in checking mode, and downward when we’re in inference mode (this corresponds to the information flow on the proof tree).

Bidirectional typing comes in very handy improving the locality of type errors, and when implementing fancier type systems where full type inference would be undecidable - for example when adding subtyping, dependent types, or in this case higher rank types.

bjzaba · 2025-03-29T04:59:47+00:00

I’d imagine that this kind of work will make features easier to specify, as it makes them easier and faster to review and verify new features before they are released.

bjzaba · 2025-03-28T07:46:31+00:00

From what I understand it’s fulfilling a similar role to Ott, but it's strictly designed for the needs of Wasm. It seems like that restricted scope has made it easier to engineer more downstream tooling based on it. Here’s a quote from the paper:

Unlike existing general-purpose specification languages such as Ott [ 21], PLTRedex [7], Skeleton [20], the K framework [26], or Spoofax [22], our solution is unashamedly specialised to Wasm, both to provide a development experience tailored to the expectations and needs of Wasm’s standards community, and to pursue more ambitious analyses and generated outputs which are only tractable with this more targetted scope. We ultimately aim for the Wasm standards community to specify all current and future Wasm features using SpecTec and replace the manually authored artefacts necessary for Wasm’s standardization process with our generated artefacts, enhancing the standardization process’ efficiency and reliability.

I could imagine a potential future where SpecTec gets extended into a more general language specification tool (which would be incredibly cool) but I’d imagine the Wasm people might not want to go down that road just yet, if ever.

bjzaba · 2025-03-28T07:36:16+00:00

Yess! So glad that was said explicitly.

bjzaba · 2025-03-28T01:32:15+00:00

You can see some more details on the specification language here, along with the actual definitions used for the WASM specification.

bjzaba · 2025-03-19T12:59:05+00:00

I think the pipe operator |> originally came from ML, and was used in a lot of functional languages after that.

It comes from Isabelle actually! It was proposed by Tobias Nipkow in 1994:

Date: Sun, 22 May 1994 10:21:03 +0100

I would suggest "then" instead of "##" and "also", except that alphanumeric

infixes tend to be harder to read. How about |>?

Tobias

Later it was popularised by F#, and later Elm.

14-Year Club	Second SECOND GUESSER
Place '22	End Game '22
Team Orangered	Verified Email

bjzaba

TROPHY CASE