I do AI research and mostly work with Lean these days. I love Haskell, though I wouldn't consider myself a particularly strong Haskell programmer (just never spent a ton of time working in it). I think you're spiritually correct that there are lots of reasons to use extremely strict languages with AI, but the reality is a little messier than you'd expect.

Token efficiency is specifically the place where strict languages get a little trickier. With dynamic languages where the model has a ton of training data, like Python, the agents are really good at writing code that just works. You still have challenges there, but they're just different than the challenges you hit with a language like Haskell/Lean/Agda etc. With Lean, for example, the amount of things the agent decides it needs to prove for a relatively trivial operation can lead to an absurd amount of code. And the way it decides to prove them can be borderline labyrinthian. It sort of plays perfectly towards current agent weaknesses, where agents can run off and reinvent a lot of machinery and build unnecessarily complex abstractions.

And those iterations have a cost. Even if the final artifact is more terse, the path to getting there can involve a huge amount of backtracking and rewriting and off-by-one syntactic corrections.

Ultimately, a lot of this comes down to developer experience. Getting useful error messages for the agent, having fast compile times so that the agent can iterate quickly, providing useful utilities for debugging, etc. There was a popular blog post specifically about Haskell that generally makes this point--the Haskell language is, in a vacuum, ideal in a lot of ways for AI, but the Haskell developer experience and ecosystem made it hard for this team to build with it via agents: https://avi.press/posts/2026-07-10-after-7-years-in-producti...

Note: I am not advocating against using these kinds of language. Obviously, I still work in Lean and a little in Agda and some related languages/projects, so I think this direction is right. Probably biased in that I love them with or without LLMs, but I do think they're also more ideal for AI development. There are still just challenges in getting agents productive in them, and most of the challenges are not about the type systems but the actual ergonomics and dev experience.

▲

lallysingh a day ago | parent | next [-]

I'm wondering the inverse, actually. That LLMs can make regular haskell programming (e.g. typing in code, not english that LLMs convert to code) powerful enough to prefer. Can we have LLMs do enough of the grunt work on building type machinery, dealing with compiler errors, looking up exact types and conversion systems, to make the APIs presented to us preferable?

So, I could write what I want in haskell, and it's faster for me than to have an LLM do it. The haskell would be high-level enough and precise enough to describe what I want the program to do with less iterations than I'd have with an LLM writing code, finding its own bugs, fixing them, then having me ask it what it did, tell it what to do differently, etc.

Direct control is very powerful. LLMs take that away from us, in exchange for a great speedup. But perhaps we can use LLMs to give it back to us by making our actual programming languages more powerful.

	▲	calebkaiser a day ago \| parent [-]
		Yeah, I think this is roughly where things are headed. Or at least, it's part of what I'm working on these days, though I'd characterize myself as "generally kind of bad at things," so maybe that's anti-signal. But I think this is actually in the design of many languages already, especially in languages like Lean, where you can prove that the presentable API is correct. Here's one rough example that is related to this direction: A common convention in Lean is to write essentially two versions of a function, with a theorem proving their equality or correspondence. So you can write a more demonstrative version that is more easily understood, which you can treat sort of as a spec that all other implementations must satisfy. And then you can set the agent loose to do whatever nastiness it wants to do to improve performance. Here's a fun write up from someone doing just this with zip file compression: https://kim-em.github.io/blog/2026-7-24-why-lean-is-faster-t...

▲

sublinear a day ago | parent | prev | next [-]

> I think you're spiritually correct that there are lots of reasons to use extremely strict languages with AI

> With dynamic languages where the model has a ton of training data, like Python, the agents are really good at writing code that just works.

I'm confused how the former supports the latter here.

Surely, you mean that LLMs are not the right kind of "AI". Languages like Haskell expose how fundamentally porous LLMs are with information.

I wouldn't even say it's the dynamic nature of Python that leads to good results, but the consistency. Javascript is the obvious counterexample. There's far more javascript out there to train on than any other programming language, yet LLMs are terrible at writing it too.

▲

3836293648 a day ago | parent | prev [-]

Just reading chain of thought traces for Agda (I'm using Qwen 3.8-Flash-Next) and it's struggling so hard with just the syntax, long before it can struggle with semantics or type errors.

Admittedly I'm not much better, Agda has some crazy scoping rules at times and its operators are a mess, so much worse than Haskell, but at least I don't have to re-learn from scratch after every compaction.

▲

icrbow 11 hours ago | parent | next [-]

Opus 5.5 has no problem with Haskell in any domain whatsoever, including mixing it up with FFI and eDSLs. You call it, it does it.

▲

mietek 13 hours ago | parent | prev | next [-]

No, Agda's mixfix operators and general syntactic malleability is state-of-the-art in programming language design. Try learning how to write it yourself, before relying on LLM to write it for you.

▲

3836293648 12 hours ago | parent [-]

It's a cool hack. It's also a catastrophe for actual usage. State-of-the-art doesn't mean good, it just means new, shiny and complex. Not being able to do syntax highlighting without a full typechecking pass is a usability nightmare.

Anyway, that's not the part I the human struggle with, it's remembering what level of infix each new custom operator has. Why λ() isn't equivalent with λ{}, if `a b , c` is `(a b) , c` or `a (b , c)` with this version of comma (Though now I've given up on the others and just use Σ a (λ _ -> b) for all kinds of tuples just to make it consistent). Why implicits won't unify as I expect them to. Why with just doesn't work in a reasonable fashion at all ever beyond the most basic two cases (no nesting and only nest in the final case). Literally copy pasting from the docs doesn't parse.

Cool trick, but in practice it was a mistake and Haskell's take on custom operators was far enough.

▲

mietek 11 hours ago | parent [-]

Here are some resources to help you get started.

An Agda course taught in Padova since 2024: https://agdapad.quasicoherent.io/~Padova2026/

"Programming Language Foundations in Agda", a course taught at multiple universities since 2018: https://plfa.github.io

Conor Titania McBride's lectures on Agda, including videos: https://github.com/pigworker/CS410-18

Thorsten Altenkirch's lectures on computer-aided formal reasoning using Agda: https://www.cs.nott.ac.uk/~psztxa/g53cfr

▲

3836293648 4 hours ago | parent [-]

Or maybe consider being less patronising and realise that Agda is a mess, regardless of how cool some aspects of it is.

I am returning to the language, not new.

▲

mietek 3 hours ago | parent [-]

There's certainly many things that could be improved about Agda, but they mostly have to do with its semantics. Here's a great blog post about some of them: https://jesper.sikanda.be/posts/why-not-a-core-language.html

Operator fixity is a non-issue; if you don't like how the fixities have been set up, you can change them at will, even in the middle of an `import` statement. Nobody is making you use custom infix operators, either; you can write Agda that looks mostly like a Lisp if you wish.

Improving `with` is ongoing work; there was a presentation on it at the recent Agda implementors' meeting.

There's real people with real feelings building Agda, and not very many of them either. Consider that before publicly denigrating their work, with such shallow criticism to boot.

	▲	3836293648 3 hours ago \| parent [-]
		Yes, and I know some of them and have critiqued it in person.

▲

calebkaiser a day ago | parent | prev [-]

Yeah I know this pain. I actually have had some success by giving the agent a style guide for Lean that is strictly not conventional. The nice syntactic shortcuts and different modes that make Lean more ergonomic for humans, in my experience, actually make it easier for an agent to trip itself up.