Idris (programming language): Difference between revisions

Revision as of 00:26, 31 December 2022

Revision as of 00:58, 31 December 2022

Line 8:

| developer =

| released = {{Start date and age|2007}}<ref>{{cite web |last=Brady |first=Edwin |date=2007-12-12 |title=Index of /~eb/darcs/Idris |url=http://www-fp.cs.st-and.ac.uk/~eb/darcs/Idris/ |website=[[University of St Andrews]] School of Computer Science |archive-url=https://web.archive.org/web/20080320233322/http://www-fp.cs.st-and.ac.uk/~eb/darcs/Idris/ |archive-date=2008-03-20 |df=dmy}}</ref>

| latest_release_version = 1.3.34<ref>{{cite web|title=Release 1.3.34|url=https://github.com/idris-lang/Idris-dev/releases/tag/v1.3.3/4|access-date=20202022-0512-2531}}</ref>

| latest_release_date = {{Start date and age|20202021|0510|2422}}

| latest_test_version = 0.6.0 (Idris 2)<ref>{{Cite web|title=Idris 2 version 0.6.0 Released|url=https://www.idris-lang.org/idris-2-version-060-released.html|access-date=2022-12-31|website=www.idris-lang.org}}</ref>

| latest_test_date = {{Start date and age|2022|10|28}}

Line 25:

'''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.1Latest documentation|website=docs.idris-lang.org}}</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|access-date=2015-07-19}}</ref>

Line 96:

===Code generation===

Because Idris contains a proof assistant, Idris programs can be written to pass proofs around. If treated naïvely, such proofs remain around at runtime. Idris aims to avoid this pitfall by aggressively erasing unused terms.<ref>{{cite web|url=http://idris.readthedocs.org/en/latest/reference/erasure.html|title=Erasure By Usage Analysis — Idris 1.1.1latest documentation|website=idris.readthedocs.org}}</ref><ref>{{cite web|url=http://ziman.functor.sk/erasure-bm/|title=Benchmark results|website=ziman.functor.sk}}</ref>

By default, Idris generates native code through [[C (programming language)|C]]. The other officially supported backend generates [[JavaScript]].