Idris (programming language)
| Idris | |
|---|---|
| Paradigm | Functional |
| Designed by | Edwin Brady |
| First appeared | 2007 |
| Stable release | Idris2 v0.8.0
/ October 31, 2025 |
| Typing discipline | Dependent |
| OS | Cross-platform |
| License | BSD |
| Filename extensions | .idr, .lidr |
| Website | www |
| Influenced by | |
| Agda, Clean, Rocq (previously known as Coq), Epigram, F#, Haskell, ML, Rust | |
Idris is a purely-functional programming language with dependent types, quantity annotations, optional lazy evaluation, and features such as a totality checker. Idris is designed to be a general-purpose programming language similar to Haskell, but may also be used as a proof assistant.
The Idris type system is similar to Agda's. Compared to Agda, Idris prioritizes management of side effects and support for embedded domain-specific languages. Idris is compiled by modular backends, which provide code generation and a runtime system. The Idris compiler includes backends for Chez Scheme, Racket, JavaScript (both browser- and Node.js-based), and C. Additional third-party backends are available for other platforms.
Idris is named after a singing dragon from the 1970s UK children's television programme Ivor the Engine.