Idris (programming language)

Idris
ParadigmFunctional
Designed byEdwin Brady
First appeared2007; 17 years ago (2007)[1]
Stable release
1.3.4[2] / October 22, 2021; 3 years ago (2021-10-22)
Preview release
0.7.0 (Idris 2)[3] / December 22, 2023; 10 months ago (2023-12-22)
Typing disciplineInferred, static, strong
OSCross-platform
LicenseBSD
Filename extensions.idr, .lidr
Websiteidris-lang.org
Influenced by
Agda, Clean,[4] Coq,[5] Epigram, F#, Haskell,[5] ML,[5] Rust[4]

Idris is a purely-functional programming language with dependent types, optional lazy evaluation, and features such as a totality checker. Idris may be used as a proof assistant, but is designed to be a general-purpose programming language similar to Haskell.

The Idris type system is similar to Agda's, and proofs are similar to Coq's, including tactics (theorem proving functions/procedures) via elaborator reflection.[6] Compared to Agda and Coq, Idris prioritizes management of side effects and support for embedded domain-specific languages. Idris compiles to C (relying on a custom copying garbage collector using Cheney's algorithm) and JavaScript (both browser- and Node.js-based). There are third-party code generators for other platforms, including Java virtual machine (JVM), Common Intermediate Language (CIL), and LLVM.[7]

Idris is named after a singing dragon from the 1970s UK children's television program Ivor the Engine.[8]

  1. ^ Brady, Edwin (12 December 2007). "Index of /~eb/darcs/Idris". University of St Andrews School of Computer Science. Archived from the original on 2008-03-20.
  2. ^ "Release 1.3.4". GitHub. Retrieved 2022-12-31.
  3. ^ "Idris 2 version 0.7.0 Released". GitHub. Retrieved 2024-04-20.
  4. ^ a b "Uniqueness Types". Idris 1.3.1 Documentation. Retrieved 2019-09-26.
  5. ^ a b c "Idris, a language with dependent types". Retrieved 2014-10-26.
  6. ^ "Elaborator Reflection – Idris 1.3.2 documentation". Retrieved 27 April 2020.
  7. ^ "Code Generation Targets – Idris Latest documentation". docs.idris-lang.org.
  8. ^ "Frequently Asked Questions". Retrieved 2015-07-19.