Idris (programming language): Difference between revisions

Revision as of 23:48, 24 March 2020

Revision as of 11:34, 27 April 2020

Line 24:

'''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 (proofcomputer assistantscience)|tactics]] (theorem proving [[Subroutine|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>

Idris 2, an unreleased successor to Idris based on [[quantitative type theory]], currently compiles to [[Scheme (programming language)|Scheme]].<ref>{{Citation|last=Brady|first=Edwin|title=A dependently typed programming language, a successor to Idris: edwinb/Idris2|date=2019-08-13|url=https://github.com/edwinb/Idris2|access-date=2019-08-13}}</ref>