Idris (programming language): Difference between revisions

Revision as of 09:15, 13 October 2019

Revision as of 23:48, 24 March 2020

Line 26:

The Idris [[type system]] is similar to [[Agda (programming language)|Agda]], and proofs are similar to [[Coq]], including [[Tactic (proof assistant)|tactics]]. 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, whichan hasunreleased asuccessor [[Chezto Scheme]]Idris backendbased and useson [[quantitative type theory]], is currently beingcompiles workedto on[[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>

Idris is named after a singing dragon from the 1970s UK children's television program ''[[Ivor the Engine#Idris the Dragon|Ivor the Engine]]''.<ref>{{cite web|title=Frequently Asked Questions|url=http://docs.idris-lang.org/en/latest/faq/faq.html#what-does-the-name-idris-mean|accessdate=2015-07-19}}</ref>