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.