Agda vs Idris 2 — is the difference meaningful for everyday use?

AgdaAdorer wrote:

is the philosophical difference between these two languages actually meaningful when you sit down to write code day-to-day?

YES. Emphatically yes. The unicode thing you mention isn't just aesthetic — it's a symptom of deep design priorities. Agda uses Unicode characters in source files (UTF-8), such as ℕ, →, and ∷. Many mathematical symbols can be typed using the corresponding LaTeX command names. That's intentional: Agda wants your code to look like a paper.

Idris 2 explicitly pushes back on this. The Idris project FAQ literally says there's "a tendency to go over the top with use of Unicode" and that "words are often better." Compared to Agda, Idris prioritizes management of side effects and support for embedded domain-specific languages.

If you're writing a program that ships, Idris 2. If you're formalising a categorical theorem for a paper, Agda. For "everyday use" — define your everyday.

The IO story alone makes this a non-contest for "everyday" programming. In Agda, IO is technically handled via a Haskell FFI backend — Agda's Haskell FFI is very good and easy to use, so you can use any Haskell library in Agda, or use Agda to write a Haskell library. But that's a bridge, not a native solution. There's no first-class monadic IO baked into the language the way Idris has it.

Idris 2 treats effects as first-class. You write IO () the same way you'd write it in Haskell, but with dependent types backing everything up. And with QTT (Quantitative Type Theory), you can now track resource usage at the type level. That's genuinely new.

Agda is beautiful. But we have to use Agda for modelling and formal verification, and then reimplement the same functionality in Haskell. The Agda code serves as a machine-checked specification. Is that your everyday workflow? If yes, Agda. If no... reconsider.

I want to talk about totality since both claim to be total. Agda is a total functional programming language — each program in it must terminate and all possible patterns must be matched. Without this feature, the logic behind the language becomes inconsistent.

Idris 2 has a totality checker too, but it's optional per-function. You can mark something total and get the checker. Or you can just... not. This is pragmatic but it means the totality guarantee is only as strong as your discipline.

In Agda, you cannot escape. The termination checker will haunt you. I find this annoying 40% of the time and profoundly correct 60% of the time. It means every Agda program that compiles carries a stronger correctness story.

The flip side: you spend a non-trivial amount of time convincing the termination checker that your structurally-recursive function is, in fact, structurally recursive. You get used to it but it's real friction.

TotallyTyped wrote:

If you're writing a program that ships, Idris 2.

But see, the Idris compiler includes backends for Chez Scheme, Racket, JavaScript (both browser- and Node.js-based), and C. That's genuinely impressive for "programs that ship." Agda only really compiles through its GHC backend (MAlonzo) or the JS backend, and the performance story is... not great.

For what it's worth, when running Agda via the MAlonzo backend compiled to Haskell, the produced code cannot offer competitive performance. It has no choice but to insert numerous unsafeCoerce calls so that GHC would accept code that has been previously checked by the Agda type checker, and the very same unsafeCoerce is what destroys the performance.

So for "everyday" programs where you care about what actually runs: Idris 2 wins on tooling. But I maintain that if you're doing proof-heavy formalisation, Agda's metavariable + hole-driven development workflow is unmatched.

-- Agda hole-driven dev: you fill in ? interactively
theorem : ∀ (n : ℕ) → n + 0 ≡ n
theorem zero    = refl
theorem (suc n) = cong suc (?)

Can we talk about QTT for a second? Because I think this is genuinely the most interesting thing Idris 2 brings to the table that Agda just... doesn't have.

Quantitative Type Theory lets you annotate how many times a value is used: zero times (erased at runtime), exactly once (linear), or unlimited (unrestricted). This means you can write code where certain proof-relevant types are provably erased — they exist only to satisfy the typechecker and have zero runtime cost.

-- Idris 2: 0-quantity means erased at runtime
data Vect : (0 len : Nat) → Type → Type

-- The `len` is phantom at runtime, just a type-level proof
lookup : (0 prf : i < len) → Fin len → Vect len a → a

In Agda you can sort of achieve this with irrelevance annotations, but QTT is more principled and more deeply integrated. Edwin Brady designed Idris 2 from scratch around this idea.

Hot take: Agda's mixfix operators are genuinely one of its killer features and nobody talks about them enough. You can define operators like if_then_else_ where underscores mark argument positions. Combined with unicode, your proofs can read almost exactly like the mathematical prose they formalise.

Agda has inductive families, which are similar to Haskell's GADTs, but they can be indexed by values and not just types. It also has parameterised modules, mixfix operators, Unicode characters, and an interactive Emacs interface.

The downside is that almost any character can be used in an Agda identifier (like α, ∧, or ♠). It is therefore necessary to have spaces between most lexical units — for example 3∷2∷1∷[] is a valid identifier, so you need to write 3 ∷ 2 ∷ 1 ∷ [] instead. This trips up newcomers constantly.

Idris 2 has operators too, but nothing as wild as Agda's mixfix system. You sacrifice some expressiveness for readability.

Something nobody's mentioned: the community / library ecosystem split is real and matters a lot for everyday use.

Coq libraries are mostly about proofs and Idris libraries are mostly about programming. Agda has a little bit of both, but this is definitely its weak point.

The Agda standard library is excellent for mathematics (Data.Nat, Relation.Binary, etc.) but if you want to, say, parse JSON or make an HTTP request, you're going to feel the pain. With Idris 2 and its package ecosystem, you're closer to being able to build real things.

I tried to write a verified parser in Agda once. The proof was beautiful. Getting it to actually do IO and interact with the filesystem required me to stare at the Haskell FFI docs for longer than I care to admit. In Idris 2, it would have been more boring but more... done.

GhostlyGADT wrote:

The proof was beautiful. Getting it to actually do IO required me to stare at the Haskell FFI docs for longer than I care to admit.

This is the crux of it honestly. Agda's interactive development is incredible though — one of the distinctive features of Agda is heavy reliance on metavariables for program construction. You can write functions with a ? placeholder — a metavariable. When interacting with the system in Emacs mode, it shows the expected type and allows you to refine the metavariable.

This makes proof construction feel like a dialogue with the typechecker. You're never just staring at a blank page — you ask Agda "what do I need here?" and it tells you. Idris 2 has holes too (the ?name syntax) but the workflow feels slightly less refined to me.

Also want to note: Agda is also a proof assistant based on the propositions-as-types paradigm (Curry–Howard correspondence), but unlike Rocq, has no separate tactics language, and proofs are written in a functional programming style. This means no Ltac, no tactic monad — everything is term-level. Depending on your background, this is either beautiful or infuriating.

I want to zoom out and quote Edwin Brady himself on the original design philosophy distinction, because I think it's illuminating. He basically describes it as starting from opposite ends of a spectrum. Idris started by asking "how do I compile dependently typed programs efficiently?" while Agda asked "what can we express in the type system?"

It's great that both Agda and Idris exist because every time one gets a feature, the other one has to catch up. That sort of competition is really healthy. Brady has literally shared Idris 2 optimisation tricks at Agda meetings so that Agda gets faster, giving him a reason to push Idris 2 further ahead. That's a wonderful ecosystem dynamic.

Think of it as: there's a spectrum — Haskell, Idris, Agda, Coq — where you are on the programming side versus where you are on the proving side. Idris 2 sits between Haskell and Agda on that spectrum. You get dependent types but you also get a language that "wants" to be a programming language first.

For everyday use? I'd say: learn both, use each where it shines. Agda when your everyday involves papers and formalisations. Idris 2 when your everyday involves writing software that needs correctness guarantees.

Adding a concrete data point here. I tried to write the same "verified binary search tree" in both. Summary:

Agda version: Gorgeous. The proof obligations flow naturally. _≤_ relations look exactly like math. Interactive hole-filling made it feel collaborative. Time to finish: ~4 hours including reading the stdlib. Time to make it actually runnable: +2 more hours of Haskell FFI wrestling for the IO parts.

Idris 2 version: Less beautiful syntax, but significantly less friction getting it to compile and run. Dependent types are powerful enough to encode most properties of programs, and an Idris program can prove invariants at compile time. It all worked. I had a binary that did meaningful things in ~5 hours total.

If "everyday" means "code that eventually runs," Idris 2 wins on total wall-clock time to working artifact. If "everyday" means "code that is maximally verified and looks like a proof," Agda wins.

Final point I want to make before bed: universe polymorphism. This is actually a subtle but important difference.

Agda has universe polymorphism — you can write definitions that are parametric over universe levels. This lets you write very generic library code that works for types at any level. It's powerful but also a source of confusion for newcomers (why does my definition need Level parameters all of a sudden?).

Idris 2 takes a different approach: rather than universe polymorphism, Idris has a cumulative hierarchy of universes — Type : Type 1, Type 1 : Type 2, etc. Cumulativity means that if x : Type n and n ≤ m, then x : Type m. Universe levels are always inferred by Idris and cannot be specified explicitly.

This is a genuinely ergonomic choice. Idris handles universe levels automatically so you almost never have to think about them. In Agda, you'll eventually hit a wall where you need to manually plumb universe levels through everything. Not dealbreaker, but it's friction.