Idris (programming language): Difference between revisions

Revision as of 11:52, 14 January 2021

Revision as of 03:16, 7 February 2021

Line 6:

| designer = Edwin Brady

| 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 |archiveurlarchive-url=https://web.archive.org/web/20080320233322/http://www-fp.cs.st-and.ac.uk/~eb/darcs/Idris/ |archivedatearchive-date=2008-03-20 |df=dmy}}</ref>

| latest_release_version = 1.3.3<ref>{{cite web|title=Release 1.3.3|url=https://github.com/idris-lang/Idris-dev/releases/tag/v1.3.3/|accessdateaccess-date=2020-05-25}}</ref>

| latest_release_date = {{Start date and age|2020|05|24}}

| latest_test_version =

Line 14:

| implementations =

| dialects =

| influenced_by = [[Agda (programming language)|Agda]], [[Clean (programming language)|Clean]],<ref name="uniqueness-types">{{cite web|title=Uniqueness Types|url=http://docs.idris-lang.org/en/latest/reference/uniqueness-types.html|website=Idris 1.3.1 Documentation|accessdateaccess-date=2019-09-26}}</ref> [[Coq]],<ref name="idris-web">{{cite web|title=Idris, a language with dependent types|url=http://www.idris-lang.org/|accessdateaccess-date=2014-10-26}}</ref> [[Epigram (programming language)|Epigram]], [[F Sharp (programming language)|F#]], [[Haskell (programming language)|Haskell]],<ref name="idris-web"/> [[ML (programming language)|ML]],<ref name="idris-web"/> [[Rust (programming language)|Rust]]<ref name="uniqueness-types"/>

| influenced =

| operating_system = [[Cross-platform]]

Line 26:

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>

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|accessdateaccess-date=2015-07-19}}</ref>

==Features==