Idris 2 and the parts of a type system the README admits are missing

A functional language whose type is a value

The opening line of the README is the whole pitch: Idris 2 is a purely functional programming language with first class types. First class types means a type can be passed to a function, returned from one, stored in a container and computed at runtime, which is the mechanism behind dependent types, elaborator reflection and a good deal of what makes Idris pleasant rather than merely sound.

The project sits at 3,073 stars and 420 forks on the idris-lang organisation, with the repository written largely in Idris itself, on the default branch main. The last push was 2026-09-18. The open issue count is 670, which is high in absolute terms and normal for a language implementation, where nearly every request is a language design discussion with a long tail of duplicates. The topic tags are compiler, dependent-types and hacktoberfest, an accurate summary plus one recurring seasonal influx of new contributors.

Two details about the project sit awkwardly against that description. First, the project is called Idris 2 but the repository, the package manifests and the Makefile all use the name Idris2 without the space. Second, the repository carries a LICENSE file but the language description does not name a license, so this article does not assert one. Both are the sort of thing you notice when you clone it rather than when you read about it.

The homepage is idris-lang.org and the documentation is hosted on Read the Docs, with the badge in the README pointing at the latest build. There are two API references for the standard library, one official and generated from the current tree, and one community-run, plus a community quickdocs site for selected packages.

Two missing features, stated without hedging

Most language READMEs list what the language can do. This one has a section titled things still missing, and it contains two bullets.

The first is cumulativity, with a parenthetical that is worth reading as a warning: currently `Type : Type`. Bear that in mind when you think you have proved something. Universals in Type are not cumulative, so a polymorphism over types does not automatically accept every type, and the compiler will not stop you from writing a proof that a later refactor invalidates.

The second is that `rewrite` does not yet work on dependent types. `rewrite` is the tactic Idris inherited from Agda for using an equality proof to change one term into another. When the target of the rewrite depends on the term being rewritten, it does not work, which removes a large and familiar corner of the proof idiom.

Stating these in the README rather than in an issue tracker is a deliberate choice, and it changes how you evaluate the project. You are not discovering the limits when a proof fails to compile three hours in. You are reading them before you start, which is the difference between a language with known gaps and a language with a reputation.

The two features also explain a fair amount of the workarounds you will find in Idris code and in the pack collection. Proofs get restructured so the equality is between indices that do not depend on the rewritten term. Universals get replaced by concrete instantiations or by functions that take the type as an explicit argument.

Bootstrapping the compiler with Chez and Racket

Idris 2 is written in Idris 2, which raises the obvious question of how it compiles itself. The answer is a staged bootstrap, and the root of the repository shows the phases.

There are three bootstrap scripts at the top level: bootstrap-stage1-chez.sh, bootstrap-stage1-racket.sh and bootstrap-stage2.sh. Stage one is built using an existing Idris 2 executable, and the Makefile names that variable and its default:

include config.mk

# Idris 2 executable used to bootstrap
export IDRIS2_BOOT ?= idris2

Stage one exists in two flavours because Chez Scheme and Racket are both usable as the bootstrap runtime, and the tree carries a bootstrap/ directory and a bootstrap-build path used by the bootstrap test. The Makefile also names the default code generator for the compiled output, which is overridable by environment variable or by argument:

IDRIS2_CG ?= chez

The standard library is not a single library but a set of them, and the build assembles a search path across them:

IDRIS2_LIBRARIES = prelude base linear network contrib test

The same Makefile handles the Windows case separately, calling cygpath to produce D:/../.. style paths, switching the path separator from a colon to a semicolon and using cp -rf in place of ln -sf. It also distinguishes a support library, libidris2_support with a shared library suffix, from the application and library package manifests idris2.ipkg and idris2api.ipkg. Versions are set from MAJOR, MINOR and PATCH, and when the build is inside a git repository but not on an exact tag, the build appends the short commit hash between releases, which means an untagged build identifies itself rather than claiming to be a release.

This is a build that has to be understood rather than merely run, and it is why the README points installation instructions at INSTALL.md instead of trying to compress them.

pack, packages and the shape of the ecosystem

The recommended way to install Idris and its packages is pack, an Idris package manager kept in a separate repository. The README describes the whole flow and it is short. You install pack following its own instructions, create a project manifest by running `idris2 --init`, and then `pack switch latest` gets you the latest version of Idris.

Once a project has an .ipkg file, pack gives access to the pack collection, described as a set of compatible libraries in the ecosystem. The mechanism is a depends field in your .ipkg file: if a dependency is listed there, pack pulls it from the matching pack collection automatically, which is dependency resolution by curated database rather than by solving a version graph. A wiki page lists curated packages by the community.

pack also handles the language server. Because idris2-lsp and other Idris-related programs are fetched and kept up to date through the same mechanism, an editor gets its language support from the package manager rather than from a separate installation ritual.

The repository structure follows from this. libs/ holds the standard library, src/ the compiler, ipkg/ the package tooling, support/ for the runtime support library, tests/ for the test suites and lint/ for linting configuration. There is also benchmark/, which is worth noting for a language whose selling point is type-level computation, since compile times are the thing that distinguishes it from more mainstream alternatives. docs/ and www/ hold the two documentation sources, CHANGELOG.md and CHANGELOG_NEXT.md are separate so that unreleased work is visible, CITATION.cff is present for academic citation, and there is a CONTRIBUTORS file and a default.nix alongside flake.nix for Nix users.

Learning resources and the samples directory

The README curates its own learning path, which is unusual and useful. It separates four categories.

The books category has one entry, Edwin Brady's Type-Driven Development with Idris from Manning, with an explicit note that it was written for Idris 1 and a link to the changes needed for Idris 2. That caveat is the kind of detail that saves a reader a wasted afternoon.

The tutorials category has Functional Programming in Idris 2 from the idris-community organisation, a tutorial on elaborator reflection in Idris 2 by Stefan Hoeck with accompanying library utilities, and a community attempt at explaining decidable equality.

The official talks are all Edwin Brady's, and they cover the Berlin Functional Programming Group on what is new in Idris 2, an ACM SIGPLAN Scheme Workshop keynote, Curry On 2019, Code Mesh LDN 18, and a full playlist on the implementation of Idris 2 from SPLV 2020 with the compiler source used for that talk published alongside it. The community talks are the more interesting list for anyone considering their own backend: extending RefC to write Idris 2 backends while avoiding most of the work, an introduction to the JVM backend, a domain driven design talk that made dependent typing useful to that audience, and a talk on Idris data science infrastructure.

The samples directory in the repository matches that list of talks rather than duplicating it. It holds files that name their subject: Proofs.idr, Vect.idr, BTree.idr, Interp.idr and InterpE.idr for two versions of an interpreter, MyOrd.idr, NamedSemi.idr, Prims.idr, Void.idr and With.idr for the small type classes and data types everyone needs. There are directories for FFI work including an FFI-readline sample, one for proofs, and files for features rather than programs: holes.idr, params.idr, multiplicity.idr, wheres.idr, listcomp.idr, io.idr, deprec.idr, fctypes.idr and bmain.idr. There is also a dummy.ipkg, which tells you the samples are themselves managed packages.

The compiler README points contributors at a good first issue label and a wiki page listing what contributions are needed, plus a map of the source code and a separate page on getting started with compiler development. For a project with this much design surface, having a maintained map is the difference between a newcomer contributing and a newcomer giving up.

Release history shows where the effort went

The release cadence is slow and lumpy, which is normal for a language implementation and worth planning around.

v0.6.0 came on 2022-10-27 and the release notes carry no detail. v0.7.0 followed on 2023-12-22, with highlights rather than a full account, pointing readers at the changelog: size-change graphs became matrices, faithfully implementing a 2001 result by Lee, Jones and Ben-Amram, elaborator scripts gained access to project files so type-providers and similar could work, and there were warnings on conflicting fixity declarations along with %hide support for them, plus documentation, error message and performance work.

The size-change graph change is the substantive one. Size-change termination is how the compiler decides a recursive function terminates, and moving from the original formulation to a matrix representation following published work is a correctness and scalability change, not a cosmetic one.

v0.8.0 arrived on 2025-10-31 after what the notes describe as nearly two years. It added autobind and typebind modifiers on operators, letting you make an operator's syntax look more like a binder, which is a real ergonomic gain for anyone writing DSLs. Totality checking started looking under data constructors, so `Just xs` counts as smaller than `Just (x :: xs)`. Typst files can be compiled as literate Idris, which is a documentation toolchain change that will matter to anyone writing tutorials.

Two entries are compiler internals with visible consequences. Constructors carrying certain tags are replaced with built-in equivalents, letting the identity optimisation optimise conversions between list-shaped things, and the RefC backend can now emit precise reference counting instructions where a reference is dropped as soon as possible, so unique variables get reused and memory consumption drops. The same release fixed memory leaks of IORef in the RefC backend and removed global_IORef_Storage as a result. The rest of the Uninhabited implementation was refactored across Data.List.Elem, Data.List1.Elem, Data.SnocList.Elem and Data.Vect.Elem so it serves both homogeneous and heterogeneous equality.

Between releases, the branch is active, and CHANGELOG_NEXT.md sitting next to CHANGELOG.md means the in-progress changes are public rather than accumulated for a surprise.

Editorial conclusion

Idris 2 is a research language that happens to be pleasant to use, and the repository is unusually honest about the gap between the two. The README lists exactly two missing features, cumulativity and rewrite on dependent types, and both of them are the kind of gap that turns a proof into an unsound argument rather than a compile error. That candour is worth more than a longer feature list. What you get instead is a bootstrapping compiler in five distinct phases, a package manager named pack that pulls a curated collection of compatible libraries, an elaborator reflective enough that type-level computation is ordinary code, a set of community talks on writing backends, and a samples directory that reads as a catalogue of what the type system can express. If you are evaluating it, the honest test is whether your use case lives inside dependent types or outside them. Inside, the tooling and the writing are unusually good. Outside, the same expressivity costs you compile times you will feel. Install it through pack rather than from source, work through samples/Proofs.idr and samples/Vect.idr to calibrate, and read the missing features list before you commit to anything.

Frequently asked questions

Official sources

1. idris-lang/Idris2 on GitHub
2. Issues
3. Project website
4. README
5. Releases