Our website is made possible by displaying online advertisements to our visitors.
Please consider supporting us by disabling your ad blocker.
Idris (programming language)
&sq=PHP&lang=en&file=File:Question_book-new.svg){kind=small} |
| Paradigm | Functional |
|---|---|
| Designed by | Edwin Brady |
| First appeared | 2007[1] |
| Stable release | 1.3.4[2]
/ October 22, 2021 |
| Preview release | 0.7.0 (Idris 2)[3]
/ December 22, 2023 |
| Typing discipline | Inferred, static, strong |
| OS | Cross-platform |
| License | BSD |
| Filename extensions | .idr, .lidr |
| Website | idris-lang |
| 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]
- ^ 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.
- ^ "Release 1.3.4". GitHub. Retrieved 2022-12-31.
- ^ "Idris 2 version 0.7.0 Released". GitHub. Retrieved 2024-04-20.
- ^ a b "Uniqueness Types". Idris 1.3.1 Documentation. Retrieved 2019-09-26.
- ^ a b c "Idris, a language with dependent types". Retrieved 2014-10-26.
- ^ "Elaborator Reflection – Idris 1.3.2 documentation". Retrieved 27 April 2020.
- ^ "Code Generation Targets – Idris Latest documentation". docs.idris-lang.org.
- ^ "Frequently Asked Questions". Retrieved 2015-07-19.
Previous Page Next Page
