What is Idris?
Idris is a general-purpose dependently typed programming language designed to allow programs and proofs to coexist. Unlike typical statically typed languages where types merely validate structure, Idris types can express logic, constraints, and correctness properties—ensuring entire classes of runtime errors never occur.
It takes inspiration from Agda and Coq but focuses more on practical programming, offering features like IO, concurrency, and compilation—making it one of the most usable dependently typed languages available.
Specs
Language Type: Dependently typed functional language
Released: 2011
Creator: Edwin Brady
Execution Model: Compiled, with REPL support
Typing: Dependently typed + totality checks
Primary Focus: Type-driven development and provable correctness
Example Code (Hello World)
module Main
main : IO ()
main = putStrLn "Hello, Idris!"
A more signature-focused example:
add : (n : Nat) -> (m : Nat) -> Nat
add n m = n + m
The type signature can describe exact mathematical constraints, not just data shapes.
How It Works
Idris integrates:
- Dependent types
- Pattern matching
- Type-level computations
- Interactive editor assistance
- Totality checking (ensuring all cases are handled)
A core principle is type-driven development, where the developer writes a type, and Idris guides the definition interactively.
Idris supports advanced type features:
| Feature | Meaning |
|---|---|
| Dependent types | Types depend on values |
| Type-level proofs | Code can represent theorems |
| Totality checking | Prevents partial or undefined behavior |
| Interfaces | Typeclasses and modular abstraction |
Unlike purely academic languages, Idris also supports practical constructs like FFI, modules, and compilation.
Strengths
- Guarantees correctness through expressive types
- Encourages mathematical clarity in program design
- Powerful type inference and interactive feedback
- Can compile to native code, JS, or bytecode through backends
Weaknesses
- Steep learning curve, especially for non-functional programmers
- Community size smaller than mainstream languages
- Some tooling remains academic rather than production-focused
- Writing proofs can become complex for large systems
Where to Run
Idris runs via:
- Official compiler and REPL
- VS Code and Emacs extensions
- Online playground interpreters
- TIO.run (subset support depending on version)
Two major versions exist: Idris 1 and Idris 2 (rewritten on a self-hosted type theory).
Should You Learn It?
- For everyday programming: No
- For research, formal verification, and type theory: Yes
- For exploring dependently typed languages beyond Coq and Agda: Ideal
- For hobby esolang exploration: Interesting but advanced
Summary
Idris bridges the gap between theorem provers and practical programming. With expressive dependent types and strong guarantees, it allows developers to create mathematically verified software—transforming correctness from an afterthought into a core design structure.
Top comments (0)