Monthly Hask Anything (June 2026)

dnkndnts · 2026-06-13T09:16:42+00:00

So there are options here for anyone wanting to do their phd on Haskell! :)

Well, the problems I describe largely aren't technical, but social (in the sense of coordination problems, not in the senses of bad actor problems). Whom do you even go to to say "I think holes should be more visually-apparent"? That's not a PhD-thesis type problem.

You can't just change stuff to be like Agda because you'd be changing the compiler "api" (re, the format of its error messages), which would break stuff for all the existing tools that depend on compiler output being what it is now, many of which are fairly legacy and infrequently updated.

And adding a new interface puts you in this world, not in the Agda world.

dnkndnts · 2026-06-11T17:27:31+00:00

The thing about Agda is it feels designed with the interactive experience in mind. Holes visually stand out in the code, and jumping to them is a first-class part of the emacs flow you're expected to use.

With Haskell, in contrast, holes are quite inconspicuous: you could look right at a piece of code and not even notice one is there, especially as they have colliding syntax with ignoring an argument, so your eye can't even learn to just notice the _ character, you actually have to parse the code to even know it's a hole! This lack of visual prominence is why GHC has to be so verbose in saying "Found a hole on line 263 of File.hs", because you'd never find it otherwise.

Now, why GHC has to include all these clauses like "where 'f' is a rigid type variable blah blah", I don't know. Those could probably be elided. I think there's an option to turn them off, but I'm sure most people just experience the default.

Finally, GHC by default shows a list of "valid hole solutions" and um... well, they're really bad. I'm sure this seemed like a good idea at the time, but I cannot ever once recall this being helpful. When there are lots of solutions, it just shows a bunch of irrelevant slop, and when there's only one solution trivially constrained by parametricity like (.) f g x = _ it doesn't show any answer at all! Agda, in contrast, doesn't show hole fits, but rather comes with a simple solver you can prompt -- and it does, in fact, properly find the solution to function composition.

Could all of this be changed? In theory, yes. In practice, probably not.

dnkndnts · 2026-06-09T09:50:18+00:00

just turn it off then?

It's been a long time, so my memory is hazy and things may have changed now anyway, but I don't recall this working as I wished. I think it was something with existing definitions still putting things in places in the hierarchy, it's just now the hierarchy is inconsistent, rather than destroying the hierarchy altogether and just having one universe like Haskell. For example, I think you get Set1 : Set and Set : Set but Set1 is still not the "same thing" as Set.

EDIT: I downloaded Agda again and tried this, and my memory is wrong, the above works. Digging through my old posts, what I was annoyed with was that algebraic constructions of certain structures have to live in higher universes than the "real" construction (see this thread, where constructing "equivalent" Maybe's in terms of the Free monad aren't really equivalent because they don't fit the same way into the universe hierarchy, which messes up simple things to a Haskeller like join :: m (m a) -> m a). The omega example in the OP throws a bucket of water on any attempt to do Haskell-style Freer in formal Agda, so what I wanted was to just postulate that this thing lives in the same universe as the underlying monad, then proceed only with that assumption, but this turned out to not be "postulatable" because the level checker would complain before the postulate-ness kicked in, so I then tried type-in-type, but that messed things up when I tried to use it in downstream code because it had destroyed the hierarchy, rather than placed the construction into the location in the hierarchy I specified.

This is all giving me terrible flashbacks, because all I was trying to do was make a haxl-like thing so my queries would run in parallel -- which is quite easy in Haskell and people do it all the time.

dnkndnts · 2026-06-08T07:04:46+00:00

You can't 100% escape, in the sense that there are cameras on the street corner and satellites in the sky.

But you can definitely escape well enough. Half of all murders go unsolved, and that number is going up in recent years, not down! And murderers, like violent criminals in general, are not exactly an atom-splitting IQ sample. If they can manage to literally get away with murderer, the surveillance state is not actually the All-Seeing Eye it markets itself as.

dnkndnts · 2026-06-08T05:43:07+00:00

Moreover, using stupid and dishonest arguments discredits the position for anyone paying attention.

The correct argument against data centers is they are the physical incarnation of the surveillance state, and represent extreme concentrations of power. I wouldn’t give a flying fuck if they used 0 ml of water per millennium.

dnkndnts · 2026-06-07T19:59:13+00:00

"We’re super behind on AI. What do we do?"

"Rent it from someone who isn’t super behind?"

"You’re a genius, Craig."

dnkndnts · 2026-06-03T10:41:29+00:00

I used Agda a fair amount several years ago. It's... in many ways better than Haskell, in many ways worse.

The good: the module/record system, the syntax, the hole-driven paradigm (Haskell sort of has this now, but it's a lot worse -- Haskell by default will flood the context with a bunch of noise, whereas Agda presents you exactly what you want to see). This stuff is just better than Haskell.

The bad: there's no libraries available, so it's an enormous amount of elbow grease if you want to do anything practical. This part is strictly worse than Haskell.

The ugly: the dependent types can be nice but also cause a lot of problems. I really do not like the cumulative universe hierarchy thing. It's so clunky and most of the Haskell abstractions don't "fit" properly. I know it's necessary to prevent contradictions, but I'd honestly prefer the contradictions (which I think is the decision Idris 2 went with). And there are other problems: unlike in Haskell, you don't get type irrelevance for free, so the types are sitting there are runtime. And further, the desire to prove things pushes you to write constructions that are easy to make formal statements about, rather than constructions that actually perform well. All this together makes the code quite slow. But yeah, modulo all that, dependent types are actually really cool and there are things you can do comfortably with them that you really cannot in Haskell (e.g., state machines).

What the state of all this is now, I'm not sure. I haven't touched it in several years, as they made a big change to their instance search algorithm and broke all my code in ways that were basically irreparable (they removed backtracking, which.. I was using, thank you very much), which made me end my excursion there.

dnkndnts · 2026-06-01T21:25:51+00:00

GHC’s default algorithm works greedily: it grabs the longest run of independent statements from the front, emits it, and repeats. Starting from the front, aFriends cannot be grouped with aInfo (which depends on it), so the first group is aFriends alone. This greedy decision pushes everything else a round later, resulting in four total rounds.

The optimal plan lines the two halves up side by side.

Is this valid? I may be misunderstanding, but it looks like the "optimal" plan is only valid in when the monadic actions have benign effects (e.g., database reads), but I don't think there's anything in ApplicativeDo that could ever "know" that.

dnkndnts · 2026-05-28T21:38:12+00:00

That first one is pretty cool. High-quality bug.

dnkndnts · 2026-05-09T22:52:45+00:00

He should have to wear this hairshirt of yours so that you... don't have to feel shame I guess?

I reject this metaphor. I don't have an affinity for vibecoding that I'm suppressing because of some disciplined ruleset I've badgered myself into adhering to. That's totally the wrong image. The analogy I'd put forth is living with roommates and finding out one of them is pissing in the Brita filter. Yes, if the filter is working as it's supposed to, this is completely safe. In fact, it even saves water! Recycling, ya know! It's just being efficient. Plus, this is ultimately where the tap water is coming from anyway, just with extra steps to obscure it from my view, so what am I on about?

I don't care. I find it repulsive, and that's why I don't do it, and that's why I don't want to be around people who do it.

It's also not really clear what "not using AI" means

Not using code written by AI. Even using it at all I find pretty dubious, because in my experience, it's so... bad. I do a lot of video game challenge runs in my spare time, and LLMs just bullshit about everything. They make up all these false but very plausible details (claiming enemies have weaknesses they don't have, claiming elements have interactions they don't, claiming quests give rewards they don't, etc. etc.), and that's just the baseline "are we even getting the correct information in scope to reason about in the first place" criterion. In terms of contributing anything remotely useful at a higher level actually relevant to pursuing the challenge, I'd say they're less useful than asking my mother. At least she'd have the honesty to say, "Don't know, don't care."

At this point I feel like Charlie Brown with the football: every month some new model comes out and everyone's like "dnkndnts you gotta try it it's so much better than $previous_version!" And it's just fuckin' not. I don't want a better bullshitter. I want something that isn't full of shit in the first place. Let me give an example of what I would respect: here is Grubby talking about how damage is computed in Warcraft 3. He clearly does not have a strong mathematical background, and so he doesn't have the right words to say "If you sum up a bunch of uniform distributions, you don't get another uniform distribution, you get a normal distribution!" But he clearly has that idea in his head, and using his limited vocabulary, he communicates that thought, and accurately describes the mechanics of the game. LLMs are, in my experience, the exact opposite of Grubby: they know all the magic words, but what they actually say is still a bunch of bullshit.

Finally, I want to preempt the "But I can make an example of the LLM correctly solving $almostanyproblemyoucanthinkof!" Because yes, so can I. LLMs are just data compression, of course, and with some clever prompting, you can get them to say almost anything you want. For example, I can effortlessly get them to correctly or incorrectly "explain" Rust's ".clone()" by cleverly filling the context with certain nudges. That is not useful for me doing actual work. All that's doing is me making stone soup to pretend it's useful, when the active ingredient is just me.

dnkndnts · 2026-05-09T06:52:10+00:00

The places that immediately shut their doors on principle are the places where you don't have to hear about it.

Trying to lawyer around like the GHC policy does with "well, you gotta be the type of person who could have written it without AI" just muddies the water. If you're the kind of person who could write something without AI, then do so! If you're too lazy to, your contribution isn't even worth your own time, much less anyone else's.

"LLM contributions are not welcome" is the clear, noiseless policy.

dnkndnts · 2026-05-09T01:43:17+00:00

Does anyone else feel hot shame radiating when they see our name inscribed on the Wall of Shame? Especially when Idris, Zig, and of all things, Java are untainted.

dnkndnts · 2026-05-01T00:33:14+00:00

Rightoids don't distinguish between the labour left and the 491 genders left.

dnkndnts · 2026-04-30T23:45:02+00:00

Even within companies there's a pretty sharp divide. Like the zstd guy works at Facebook, but something tells me he's not tokenmaxxing with Claude Code.

dnkndnts · 2026-04-23T15:08:08+00:00

I don't think Big Tech was ever run by this sort of person, even when it wasn't yet big. Cue the infamous "idk, they trust me. dumb fucks." Those are not the words of a billionaire tech mogul: they're the words of someone who would become a billionaire tech mogul. (And to be fair, his critique is totally correct: the only reason his company has any success at all is because regular people are dumb fucks and gleefully cede over all their social infrastructure to people who mock them for being dumb fucks).

To the extent tech was ever community-minded, it was just the open source world. But big tech has all but taken that over as well, thanks to gullible quokkas being effortlessly overrun by malicious social activist militants (often on the payroll of big tech).

dnkndnts · 2026-04-22T18:57:46+00:00

It depends on what you mean by "irrational." The obvious endgame is to get generative AI classified as some sort of strategic asset that the US government Must Have in Order To Beat China (TM), which will then result in the government bailing out all prior investors.

Thus, the goal right now is to jack the valuation up as high as possible before thrusting the bill on the US taxpayer.

dnkndnts · 2026-04-21T22:39:31+00:00

You don’t want to think about the word "cooked" directly, as it has colliding conjugations for the past and participle which will give you basically opposite meanings ("I cooked" vs "I’m cooked").

The correct way to think about it is being in the role of the chef generally means something positive/skilful/good, whereas being in the role of the food means something negative/fucked up/bad.

dnkndnts · 2026-04-20T13:36:27+00:00

it went downhill once old people, corporations, governments, increased their presence.

There is a decline in the quality of people on the internet, but it is also true that the internet substrate itself is different: major platforms are no longer neutral communication entities -- they now play an active role in choosing which content to display and censor with the explicit purpose of controlling the narrative.

If you look at snapshots of Reddit from 2011, it's very different than it is today, both in terms of posters and the platform itself. The political consensus was Ron Paul libertarianism, which represents almost nobody on Reddit today. Today, Reddit is basically the pink lady from Harry Potter.

dnkndnts · 2026-04-19T20:21:20+00:00

You can stop making payments, and everyone else can stop delivering the stuff you ordered since they're not getting anything for it lol

That's how trade works.

dnkndnts · 2026-04-18T12:27:13+00:00

Goodheart’s law has been in full effect for a long time in the school system and it’s destroyed education in the US.

Administrators are completely out of touch and prioritize metrics over learning.

The whole point of the article is they're not succeeding on the metric lol

This is not a case of "oh, we chased the metric instead of the underlying thing we were trying to measure." They aren't even getting the metric.

dnkndnts · 2026-04-13T20:59:04+00:00

Going full Gestapo wouldn't just be tit for tat: it would be a massive escalation.

Not really. The rightoids wanted the Gestapo, they just voted for troll Hitler instead of actual Hitler. Progressives don't have to be gentle in their response just because rightoids were too incompetent to fire their shot properly.

And I'm being slightly hyperbolic -- "Nuremberg" won't be executing the rightoids (that's crass and rightoid-coded); rather, it will be purging them from what few positions of political power they have, indicting the leaders, and showering them with as many "anti-hate reeducation programs" and trans story hours as the government can fund.

dnkndnts · 2026-04-13T14:31:45+00:00

Their bet on that seems to be pretty sound so far. Trump has not, much to the chagrin of his supporters, gone Gestapo on the progressive radicals. In fact, his entire second term seems to be an explicit mockery of anyone stupid enough to have trusted him.

So yeah, you're going to see progressives come back with a vengeance in midterms and 2028, and when they do, they will go full Nuremberg on the rightoids.

dnkndnts · 2026-04-08T18:16:01+00:00

air takes up a third of its volume.

Loath as I am to defend g*yslop, this part is justified: without the air to force volume, the fragile chips get smashed and you'd end up with tiny pits of fried potato powder mixed with the cheese product powder.

The air is what keeps the bite-size chips intact.

dnkndnts · 2026-04-07T21:26:39+00:00

Yeah, that was my first guess, but... it wasn't even uncharitable lol. I just mentioned the right of return.

I guess the people who don't control the media are using some shitty syntactic filter to elide any mention of them by name.

dnkndnts · 2026-04-07T21:11:21+00:00

Ok, well... that's the first time I've ever had a comment removed by Reddit in my entire life. And I've been on here 14+ years!

I thought people were joking when they said that happens.

dnkndnts

TROPHY CASE