Idris (programming language): Difference between revisions

Revision as of 13:40, 27 April 2020

Latest revision as of 12:44, 15 November 2024

(39 intermediate revisions by 23 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 |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_versionlatest release version = 1.3.24<ref>{{cite web |title=IdrisRelease 1.3.24 |website=[[GitHub]] released|url=https://wwwgithub.com/idris-lang.org/idris-1Idris-3-2-releaseddev/releases/tag/v1.3.4 |accessdateaccess-date=20192022-0712-2231}}</ref>

| latest_release_datelatest release date = {{Start date and age|20192021|0710|22}}

| latest preview version = 0.7.0 (Idris 2)<ref>{{Cite web |title=Idris 2 version 0.7.0 Released |website=[[GitHub]] |url=https://github.com/idris-lang/Idris2/releases/tag/v0.7.0 |access-date=2024-04-20}}</ref>

| latest_test_version =

| latest preview date = {{Start date and age|2023|12|22}}

| latest_test_date =

| 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 |accessdateaccess-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/ |accessdateaccess-date=2014-10-26}}</ref> [[Epigram (programming language)|Epigram]], [[HaskellF Sharp (programming language)|F#]], [[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 |accessdateaccess-date=2015-07-19}}</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>

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>

==Features==

Line 35 ⟶ 33:

===Functional programming===

The syntax of Idris shows many similarities with that of Haskell. A [[hello world program]] in Idris might look like this:

<sourcesyntaxhighlight lang="idris">

module Main

main : IO ()

main = putStrLn "Hello, World!"

</syntaxhighlight>

</source>

The only differences between this program and its [[Haskell (programming language)#Code examples|Haskell equivalent]] are the single colon (instead of twodouble) colon in the [[Typetype signature|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:

<sourcesyntaxhighlight lang="idris">

data Tree a = Node (Tree a) (Tree a) | Leaf a

</syntaxhighlight>

</source>

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

<sourcesyntaxhighlight lang="idris">

data Tree : Type -> Type where

Node : Tree a -> Tree a -> Tree a

Leaf : a -> Tree a

</syntaxhighlight>

</source>

===Dependent types===

With [[dependent type]]s, it is possible for values to appear in the types; in effect, any value-level computation can be performed during [[typecheckingtype checking]]. The following defines a type of lists whose lengths are known before the program runs, traditionally called [[Array data structure|vectors]]:

<sourcesyntaxhighlight lang="idris">

data Vect : Nat -> Type -> Type where

Nil : Vect 0 a

(::) : (x : a) -> (xs : Vect n a) -> Vect (n + 1) a

</syntaxhighlight>

</source>

This type can be used as follows:

<sourcesyntaxhighlight lang="idris">

total

append : Vect n a -> Vect m a -> Vect (n + m) a

append Nil ys = ys

append (x :: xs) ys = x :: append xs ys

</syntaxhighlight>

</source>

The functionsfunction <code>append</code> appends a vector of <code>m</code> elements of type <code>a</code> to a vector of <code>n</code> elements of type <code>a</code>. Since the precise types of the input vectors depend on a value, it is possible to be certain at [[compile- time]] that the resulting vector will have exactly (<code>n</code> + <code>m</code>) elements of type <code>a</code>.

The word "<code>total</code>" invokes the [[Termination analysis|totality checker]] which will report an error if the function [[Partial function|doesn't cover all possible cases]] or cannot be (automatically) proven not to enter an [[infinite loop]].

Another common example is pairwise addition of two vectors that are parameterized over their length:

<sourcesyntaxhighlight lang="idris">

total

pairAdd : Num a => Vect n a -> Vect n a -> Vect n a

pairAdd Nil Nil = Nil

pairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ys

</syntaxhighlight>

</source>

<code>Num</code> a signifies that the type a belongs to the [[type class]] <code>Num</code>. Note that this function still typechecks successfully as total, even though there is no case matching <code>Nil</code> in one vector and a number in the other. SinceBecause boththe vectorstype aresystem ensuredcan byprove that the type system tovectors have exactly the same length, we can be sure at compile time that this case will not occur. Henceand itthere doesis notno need to beinclude mentionedthat forcase in the functionfunction’s to be totaldefinition.

===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 (programming language)|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 119 ⟶ 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 126 ⟶ 130:

[[Category:2007 software]]

[[Category:Pattern matching programming languages]]

[[Category:Statically typed programming languages]]