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.