Idris

Idris is a general-purpose, purely functional programming language with first-class dependent types — types that can be computed from, and depend on, ordinary values. Designed by Edwin Brady, Idris aims to bring the power of dependently typed programming, long confined to proof assistants like Coq and Agda, into a language meant for writing real software. Its guiding idea is type-driven development: writing the type first and letting that type guide, constrain, and verify the implementation.

History & Origins

Idris originated in the mid-2000s out of Edwin Brady’s research into dependently typed functional programming, with the language first appearing around 2007. Brady, based at the University of St Andrews in Scotland, had worked on the experimental dependently typed language Epigram and wanted a language that kept the expressive power of full dependent types while feeling practical for everyday programming — closer in spirit to Haskell than to a pure proof assistant.

The original Idris compiler was written in Haskell. Brady set out the language’s goals in a series of papers, notably “IDRIS — systems programming meets full dependent types” (PLPV, 2011) and the comprehensive “Idris, a general-purpose dependently typed programming language: Design and implementation” in the Journal of Functional Programming (2013), which remains the canonical description of the first-generation language.

The name is a nod to British culture: Idris is named after the singing dragon from the 1970s children’s television series Ivor the Engine.

Reaching 1.0

After years as a research project, Idris 1.0 was released in April 2017. The milestone marked the core language and base libraries as stable, promising source compatibility across future 1.x releases. That same month, Manning published Brady’s book Type-Driven Development with Idris, which became the standard practical introduction to the language and its philosophy.

Idris 2

Around 2020, Brady began a complete rewrite, Idris 2, with two major changes. First, the new compiler is self-hosted — written in Idris itself rather than Haskell — and bootstraps through generated Chez Scheme code. Second, and more fundamentally, its core is based on Quantitative Type Theory (QTT), a type theory developed with Robert Atkey and others that unifies linear types and dependent types in a single framework. The design was documented in “Idris 2: Quantitative Type Theory in Practice”, presented at ECOOP 2021. Idris 2 has since become the primary, actively developed version of the language, continuing through an ongoing 0.x release series — most recently v0.8.0 in October 2025.

Design Philosophy

Idris is built on the conviction that types are a tool for constructing programs, not merely for catching errors after the fact. In a dependently typed language, the type of a value can mention other values — for example, a vector type can carry its exact length, so the type Vect 3 Int is the type of integer vectors with precisely three elements. This lets the compiler reject, at compile time, code that would index out of bounds, mismatch dimensions, or violate a stated invariant.

Core principles include:

• Type-driven development — write a precise type first, then let the compiler’s interactive editing features help fill in an implementation that satisfies it.
• Types as propositions — through the Curry–Howard correspondence, a type can express a logical proposition, and a value of that type is a proof, making Idris usable as a theorem prover.
• Practicality over purity of theory — unlike pure proof assistants, Idris is meant for general-purpose programming, with conveniences like type classes (interfaces), do notation, and a foreign function interface.
• Totality checking — functions can be checked to be total (terminating and covering all cases), which is necessary when a function is also meant to stand as a proof.
• Optional lazy evaluation — Idris is strict by default but supports laziness explicitly where needed.

Key Features

The hallmark of Idris is dependent types, but the language pairs them with a familiar, Haskell-like syntax. A classic example is a length-indexed vector whose type guarantees safety:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

import Data.Vect

-- A Vect carries its length in its type
fourInts : Vect 4 Int
fourInts = [0, 1, 2, 3]

-- The type guarantees the two inputs have the same length,
-- and that the result does too. A mismatch won't compile.
addPairwise : Num a => Vect n a -> Vect n a -> Vect n a
addPairwise [] [] = []
addPairwise (x :: xs) (y :: ys) = (x + y) :: addPairwise xs ys

Other notable features include:

• Interactive, hole-driven editing — programmers can leave typed “holes” in code and ask the compiler what type is expected, then incrementally refine the program.
• Interfaces — Idris’s analogue of Haskell type classes for ad-hoc polymorphism.
• Dependent pattern matching — matching on one value can refine the types of others.
• Quantitative (linear) types in Idris 2 — every variable carries a multiplicity (used 0, 1, or unrestricted-many times). Multiplicity 0 marks data that exists only at the type level and is erased at run time, while multiplicity 1 enforces that a resource is used exactly once.
• Multiple compilation backends — Idris 2 ships official code generators targeting Chez Scheme (the default), Racket, JavaScript (for Node.js and the browser), and C (the RefC backend), with additional community-maintained backends available.

Evolution

Idris’s evolution falls into two distinct generations. The first generation (Idris 1), written in Haskell, established the language’s identity: full dependent types in a programmer-friendly package, culminating in the stable 1.0 release of 2017 and an accompanying textbook.

The second generation (Idris 2) reframed the language around Quantitative Type Theory, adding linearity and run-time erasure to the type system and rebuilding the compiler in Idris itself. This self-hosting was both a practical demonstration and a forcing function: writing a compiler in the language exercised its features at scale. Idris 2 remains in an active 0.x development series, signaling that the maintainers consider the design still open to refinement rather than frozen.

Current Relevance

Idris occupies a distinctive niche: it is more practical and programmer-oriented than pure proof assistants like Coq (now Rocq) and Agda, yet far more experimental and research-driven than mainstream functional languages like Haskell or OCaml. Its primary communities are programming-language researchers, type-theory enthusiasts, and educators and learners exploring how dependent and quantitative types change the way software is written.

While Idris has not seen large-scale industrial adoption, its ideas have rippled outward. The broader movement toward richer type systems — linear types in Haskell and Rust’s ownership model among them — shares intellectual DNA with the resource-tracking concerns that Quantitative Type Theory addresses head-on. As a place to study these ideas in a working, self-hosting language, Idris remains influential well beyond its user count.

Why It Matters

Idris matters as a proof of concept for a different way of programming, one in which the type system is a constant collaborator rather than a gatekeeper. By showing that full dependent types can live inside a usable, general-purpose language — complete with a self-hosting compiler, multiple backends, and a teaching tradition built around type-driven development — Idris has helped move dependently typed programming from the seminar room toward the realm of practical software engineering. Its embrace of Quantitative Type Theory further stakes out a research frontier where correctness and resource discipline are expressed in the same language as the program itself.