Idris (programming language): Difference between revisions

Revision as of 18:58, 19 June 2021

Latest revision as of 12:44, 15 November 2024

(19 intermediate revisions by 14 users not shown)

Line 1:

{{Short description|Functional programming language created in 2007}}

{{Primary sources|date=August 2019}}

{{Infobox programming language

| name = Idris

| paradigm = [[functionalFunctional programming|Functional]]

| year =

| 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 |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_versionlatest release version = 1.3.34<ref>{{cite web |title=Release 1.3.34 |website=[[GitHub]] |url=https://github.com/idris-lang/Idris-dev/releases/tag/v1.3.3/4 |access-date=20202022-0512-2531}}</ref>

| latest_release_datelatest release date = {{Start date and age|20202021|0510|2422}}

| latest_test_versionlatest preview version = 0.37.0 (Idris 2)<ref>{{Cite web |title=Idris 2 version 0.37.0 Released |website=[[GitHub]] |url=https://wwwgithub.com/idris-lang.org/idris-2-version-030-releasedIdris2/releases/tag/v0.html7.0 |access-date=20212024-0304-17|website=www.idris-lang.org20}}</ref>

| latest_test_datelatest preview date = {{Start date and age|20212023|0112|1322}}

| typing = [[Type inference|Inferred]], [[Static typing|static]], [[Strong and weak typing|strong]]

| typing =

| implementations =

| dialects =

| influenced_byinfluenced 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 |access-date=2019-09-26}}</ref> [[Coq (software)|Coq]],<ref name="idris-web">{{cite web |title=Idris, a language with dependent types |url=http://www.idris-lang.org/ |access-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_systemoperating system = [[Cross-platform software|Cross-platform]]

| license = [[BSD licenses|BSD]]

| file ext = .idr, .lidr

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]]'s, and proofs are similar to [[Coq (software)|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]] (JVM), [[Common Intermediate Language|CIL]] (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>

==Features==

Line 40:

</syntaxhighlight>

The only differences between this program and its [[Haskell (programming language)#Code examples|Haskell equivalent]] are the single (instead of double) colon in the [[type signature]] of the main function, and the omission of the word "<code>where</code>" in the [[Library (computing)|module]] declaration.<ref>{{cite web |url=https://docs.idris-lang.org/en/v1.3.2/reference/syntax-guide.html |title=Syntax Guide —– Idris 1.3.2 documentation |access-date=27 April 2020}}</ref>

===Inductive and parametric data types===

Idris supports [[inductively-defined data type]]s and [[parametric polymorphism]]. Such types can be defined both in traditional "''[[Haskell]] 98|Haskell98]]"''-like syntax:

<syntaxhighlight lang="idris">

Line 49:

</syntaxhighlight>

or in the more general [[Generalizedgeneralized algebraic data type|GADT]] (GADT)-like syntax:

<syntaxhighlight lang="idris">

Line 90:

===Proof assistant features===

Dependent types are powerful enough to encode most properties of programs, and an Idris program can prove invariants at compile time. This makes Idris into a proof assistant.

There are two standard ways of interacting with proof assistants: by writing a series of tactic invocations (Coq style), or by interactively elaborating a proof term ([[Epigram (programming language)|Epigram]]/Agda–Agda style). Idris supports both modes of interaction, although the set of available tactics is not yet as useful as that of Coq.{{Vague|date=October 2019}}

===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]].

==Idris 2==

Idris 2 is a new [[Self-hosting (compilers)|self-hosted]] version of the language which deeply integrates a [[linear type system]], based on [[quantitative type theory]]. It currently compiles to [[Scheme (programming language)|Scheme]] and [[C (programming language)|C]].<ref>{{Cite web |title=idris-lang/Idris2 |url=https://github.com/idris-lang/Idris2 |access-date=2021-04-11 |website=GitHub |language=en}}</ref>

==See also==

* [[List of proof assistants]]

* [[Total functional programming]]

==References==

{{reflistReflist}}

==External links==

* [http://{{Official website|idris-lang.org/ The Idris homepage]}}, including documentation, frequently asked questions and, examples

* [http://hackage.haskell.org/package/idris Idris at the Hackage repository]

* [http://docs.idris-lang.org/en/latest/index.html Documentation for the Idris Language (tutorial, language reference, etc.)]

{{Haskell programming}}

{{Programming languages}}

Line 120 ⟶ 122:

[[Category:Free software programmed in Haskell]]

[[Category:Haskell programming language family]]

[[Category:Articles with example Haskell code]]

[[Category:Cross-platform free software]]

[[Category:Free compilers and interpretersopen source compilers]]

[[Category:Software using the BSD license]]

[[Category:Programming languages created in 2007]]

Line 127 ⟶ 130:

[[Category:2007 software]]

[[Category:Pattern matching programming languages]]

[[Category:Statically typed programming languages]]