Compendium

Idris — Reference

8 min read

Idris — Reference

Source: https://www.idris-lang.org/

Idris

  • Created: 2007 (Idris 1, by Edwin Brady, University of St Andrews); Idris 2 announced 2019, self-hosted in Idris itself.
  • Latest stable: Idris 2 v0.8.0 (Oct 31, 2025) — Idris 2 is still pre-1.0 but is the actively developed line; Idris 1 is unmaintained.
  • Paradigms: Purely functional, dependently-typed, type-driven development.
  • Typing: Dependent types built on Quantitative Type Theory (QTT) — every binding carries a quantity (0 = erased / compile-time, 1 = linear, ω = unrestricted). This generalizes both linear types and erasure into one system.
  • Memory: Garbage-collected via the backend runtime (Boehm GC on the Chez/RefC backends).
  • Compilation: Whole-program compiler with multiple backends. Default is Chez Scheme; also Racket, Node.js, browser JavaScript, and an experimental C backend (RefC).
  • Primary domains: Research in dependent types, type-driven development teaching, formal modeling of protocols and data structures, lightweight verification.
  • Official docs: https://www.idris-lang.org/ • https://idris2.readthedocs.io/

At a glance

Idris is the most “practical-programmer-facing” of the dependently-typed languages — it deliberately positions itself as a general-purpose language that happens to have full dependent types, not a proof assistant first. Idris 2 (the current line) is a complete rewrite by Edwin Brady, self-hosted, and built on Quantitative Type Theory. Compared to Coq/Lean/Agda, Idris emphasizes programs that compute and run fast rather than proofs you read. Sources: https://www.idris-lang.org/ and the Idris 2 paper “Idris 2: Quantitative Type Theory in Practice” (Brady, ECOOP 2021, https://drops.dagstuhl.de/storage/00lipics/lipics-vol194-ecoop2021/LIPIcs.ECOOP.2021.9/LIPIcs.ECOOP.2021.9.pdf).

Getting started

  • Install: Build from source (the canonical path) — make bootstrap SCHEME=chez && make install. See https://idris2.readthedocs.io/en/latest/tutorial/starting.html.

  • Version manager / package manager: pack (https://github.com/stefan-hoeck/idris2-pack) is the de-facto package manager and toolchain manager — installs and switches between Idris 2 versions and a curated package collection.

  • Hello world:

    module Main
main : IO ()
main = putStrLn "Hello, Idris 2!"

    Build: idris2 --build hello.ipkg or idris2 -o hello Main.idr && ./build/exec/hello.

  • Project layout: An .ipkg file declares modules, dependencies, source dir. Example:

    package myproj
modules = Main, MyLib.Foo
depends = base, contrib
main = Main

  • REPL: idris2 opens a REPL with :t, :doc, :c (compile a definition), :cs (case split — type-driven IDE command). Editor integration via idris2-mode (Emacs) or LSP (idris2-lsp).

Basics

  • Types & literals: Nat, Int, Integer (arbitrary precision), Double, Char, String, Bool, (). Numeric literals are polymorphic via the Num interface. (https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html)

  • Variables / scoping: Pure, lexically scoped. let x = e1 in e2 and where-blocks for locals.

  • Control flow: if cond then x else y (both branches must have the same type), pattern matching, case ... of. No statements — everything is an expression.

  • Functions: Curried by default. Type signature first, then equations:

    add : Nat -> Nat -> Nat
add Z     m = m
add (S k) m = S (add k m)

  • Strings: UTF-8 String — concat with ++, pack/unpack to/from List Char. Interpolation with "\{expr}" (Idris 2-only).

  • Collections: List a, Vect n a (length-indexed list — the canonical dependent type), Maybe a, Either a b. The Data.Vect module defines safe head : Vect (S n) a -> a (cannot be called on empty vectors — caught at compile time).

Intermediate

  • Type system depth: Full dependent types — types can mention values, values can mention types. Sigma types (x : A ** B x) for dependent pairs. Type-level case and if. Quantitative Type Theory (Atkey 2018, https://bentnib.org/quantitative-type-theory.html) is the theoretical foundation: every binder has a multiplicity 0/1/ω.

    -- 0-quantity: erased at runtime; only matters for typing
vlen : (0 n : Nat) -> Vect n a -> Nat
vlen n _ = n   -- but this is illegal! n is erased; must compute from the Vect

  • Modules: module Foo.Bar corresponds to Foo/Bar.idr. import plus optional as and import public (re-export).

  • Error handling: Either e a, Maybe a, the MonadError interface. Effect library (Control.App) for tracked algebraic effects — Idris’s answer to monad transformers.

  • Concurrency: Limited and backend-dependent. The Chez backend exposes threads via System.Concurrency.* (mutexes, channels). No first-class STM; not the language’s strong suit.

  • I/O: IO a is the I/O monad as in Haskell. do-notation with <-. interact : (String -> String) -> IO ().

  • Stdlib highlights: base, contrib, network, linear (linear-types stdlib), papers (formalizations of papers). The pack collection adds parsers, JSON, web servers, etc.

Advanced

  • Memory / GC: Determined by the backend. Chez Scheme has a generational GC; RefC uses Boehm GC. No first-class control over allocation.

  • Concurrency: See above — basic threading on Chez. Linear types (QTT 1-quantity) give some help with safe resource handling.

  • FFI: The %foreign pragma binds an Idris signature to one or more backend strings:

    %foreign "C:puts,libc"
         "scheme:display"
prim_puts : String -> PrimIO Int

    One declaration, many backends — the compiler picks the right binding per target. Docs: https://idris2.readthedocs.io/en/latest/ffi/ffi.html.

  • Reflection: Elaborator reflection lets you inspect and synthesize TT terms inside Elab monad — used to write proof tactics and derive instances.

  • Performance tools: idris2 --timing, profiling depends on backend (Chez has its own profiler). The compiler is much slower than mainstream functional compilers.

  • Tactics & proof automation: Idris 2 deemphasizes tactic-style proof in favor of type-driven program synthesis — idris2 -p (proof search), :ps REPL command, ?hole markers in code, :cs (case split) in the editor. The auto implicit and %hint annotations let the compiler search for proofs:

    %hint
zeroPlus : (n : Nat) -> 0 + n = n
zeroPlus n = Refl

God mode

  • Quantitative Type Theory: The 0/1/ω multiplicities are visible in every binder. Erased arguments (0) genuinely vanish at runtime — you can pass proof terms that disappear in the compiled code. Linear (1) gives single-use semantics for resources (file handles, mutable refs in pure code).
  • Totality checking: %total annotation forces the checker to verify every function in a block terminates and is covering. The whole stdlib is total. The %default total pragma makes totality the default in a module.
  • %auto implicits & %hint proof search: Combined with auto arguments, Idris becomes a small Prolog-like solver — used to derive Show, Eq, etc. without typeclass machinery.
  • Elaborator reflection: Inspect the elaborator’s term language directly to write tactics and macros. Lower-level than Lean’s metaprogramming but more direct than Haskell’s TH.
  • Multiple backends: One source, many targets — Chez (fast native), Node (JS), browser (compiles to JS for the web), RefC (C output for embedded). idris2 --cg <backend>.
  • Idris 1 vs Idris 2: Idris 1 used unification-based dependent types (à la Coq, no quantities); the standard library was Haskell-flavored. Idris 2 is a complete rewrite in Idris, uses QTT, and has a faster, more predictable compiler. Idris 1 is unmaintained — start with 2. (https://idris2.readthedocs.io/en/latest/typedd/typedd.html)

Idioms & style

  • Naming: CamelCase for types and constructors, camelCase for functions/values, Module.Submodule for modules.
  • Formatter / linter: No standard formatter (the community uses idiomatic spacing). The compiler’s --check flag plus idris2-lsp give most of the value.
  • Idiomatic patterns: State invariants in types (Vect n a, indexed monads), use with-blocks for “view” pattern matching, prefer total functions, favor auto implicits over typeclasses where the search is short.
  • What experts look for: Quantity annotations on every binder where you care; %total modules; types that make illegal states unrepresentable; avoiding believe_me and assert_total except as last resort.

Ecosystem

  • Standard libraries: base, contrib, network, test.
  • Package collection: idris2-pack (https://github.com/stefan-hoeck/idris2-pack) — curated, tested-against-a-known-Idris-version package set.
  • Notable libraries: idris2-elab-util (elaborator helpers), idris2-prim (primitives), idris2-frex (free algebras), collie (CLI parser), idris2-pg (PostgreSQL), spider (WAI-style web framework).
  • Notable formalizations / projects: Type-Driven Development with Idris (Brady, Manning 2017, https://www.manning.com/books/type-driven-development-with-idris) — the canonical book; the self-hosted Idris 2 compiler itself is the largest Idris codebase.

Gotchas

  • Pre-1.0: Idris 2 is a research compiler; releases come every 6-12 months and may include breaking changes. Pin to a specific version via pack.
  • Erasure surprises: A function whose argument is 0-quantity cannot compute on that argument at runtime. The error is at use, not at signature.
  • Totality is not the default in user modules: Add %default total or face partial functions slipping in.
  • Compiler speed: Type-checking is slow compared to Haskell/OCaml. Large dependent computations at the type level can hang the elaborator.
  • No mature LSP for years; that’s improving: idris2-lsp works but expect rough edges in editor integration.
  • Different from Idris 1: Old tutorials, books (1st-edition TDDI uses Idris 1), and Stack Overflow answers may not type-check. Always confirm “Idris 2” in any reference.
  • believe_me and assert_total exist: They are unsafe escape hatches. Treat sightings in others’ code as a code smell.
  • FFI multiplicity: Foreign declarations must specify backend strings for every backend you target, or you get a runtime error on missing bindings.

Citations

Graph View