Idris (programming language): Difference between revisions

Revision as of 14:53, 27 April 2020

Revision as of 14:56, 27 April 2020

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]], and proofs are similar to [[Coq]], including [[Tactic (computer science)|tactics]] (theorem proving [[Subroutine|functions/procedures]]). 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>