Idris (programming language): Difference between revisions

Revision as of 03:53, 17 March 2021

Revision as of 06:24, 17 March 2021

Line 22:

}}

'''[[Idris]]''' is a [[purely functional programming|purely-functional]] [[programming language]] with [[dependent type]]s, optional [[lazy evaluation]], and features such as a [[Termination analysis|totality checker]]. Idris may be used as a [[proof assistant]], but it is designed to be a [[general-purpose programming language]] similar to [[Haskell (programming language)|Haskell]].

The Idris [[type system]] is similar to [[Agda (programming language)|Agda]]'s, and proofs are similar to [[Coq]]'s, including [[Tactic (computer science)|tactics]] (theorem proving [[Subroutine|functions/procedures]]) via elaborator reflection.<ref>{{cite web|url=https://docs.idris-lang.org/en/v1.3.2/reference/elaborator-reflection.html|title=Elaborator Reflection — Idris 1.3.2 documentation|access-date=27 April 2020}}</ref> Compared to Agda and Coq, Idris prioritizes management of [[Side effect (computer science)|side effects]] and support for [[EDSL#Usage patterns|embedded ___domain-specific languages]]. Idris compiles to [[C (programming language)|C]] (relying on a custom copying [[Garbage collection (computer science)|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]].<ref>{{cite web|url=http://docs.idris-lang.org/en/latest/reference/codegen.html|title=Code Generation Targets — Idris 1.1.1 documentation|website=docs.idris-lang.org}}</ref>