Back Idris (llenguatge de programació) Catalan Idris (programovací jazyk) Czech ادریس (زبان برنامه‌نویسی) Persian Idris (プログラミング言語) Japanese Idris (programmeertaal) Dutch Idris (limbaj de programare) Romanian Idris (язык программирования) Russian Idris Chinese Idris ZH-YUE

Idris (programming language)

Idris
ParadigmFunctional
Designed byEdwin Brady
First appeared2007 (2007)[1]
Stable release
1.3.4[2] / October 22, 2021 (2021-10-22)
Preview release
0.7.0 (Idris 2)[3] / December 22, 2023 (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.

Rich TVX News Network Site

Rich TVX News Network Info

© MMXXIII Rich X Search. We shall prevail. All rights reserved. Rich X Search