Idris (programming language): Difference between revisions

Revision as of 20:41, 13 November 2014

Latest revision as of 12:44, 15 November 2024

(139 intermediate revisions by 83 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]]

| designer = Edwin Brady

| year =

| developer = =

| designer = Edwin Brady

| 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>

| developer =

| latest release version = 1.3.4<ref>{{cite web |title=Release 1.3.4 |website=[[GitHub]] |url=https://github.com/idris-lang/Idris-dev/releases/tag/v1.3.4 |access-date=2022-12-31}}</ref>

| latest_release_version = 0.9.15.1

| latest_release_date latest release date = {{release_dateStart date and age|20142021|10|2622}}

| 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_by 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 |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/ |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 = =

| influenced_by = [[Agda (programming language)|Agda]], [[Coq]],<ref name="idris-web">{{cite web|title=Idris, a language with dependent types|url=http://www.idris-lang.org/|accessdate=2014-10-26}}</ref> [[Epigram (programming language)|Epigram]], [[Haskell (programming language)|Haskell]],<ref name="idris-web"/> [[ML (programming language)|ML]],<ref name="idris-web"/>

| operating system = [[Cross-platform software|Cross-platform]]

| license = BSD-3

| license = [[BSD licenses|BSD]]

| website = [http://idris-lang.org/ Idris website]

| file ext = .idr, .lidr

| website = {{URL|idris-lang.org}}

| operating_system = [[Cross-platform]]

}}

'''Idris''' is a general-purpose pure [[Functionalpurely programmingfunctional languagesprogramming|purely-functional]] [[programming language]] with [[dependent type]]s., Theoptional [[typelazy systemevaluation]], isand similarfeatures tosuch as a [[Termination analysis|totality checker]]. Idris themay onebe used byas a [[Agdaproof assistant]], but is designed to be a [[general-purpose (programming language)|Agda]] similar to [[Haskell]].

The Idris [[type system]] is similar to [[Agda (programming language)|Agda]]'s, and proofs are similar to [[Coq (software)|Coq]]'s, including 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 Latest documentation |website=docs.idris-lang.org}}</ref>

The language supports [[Proof assistant|interactive theorem-proving]] comparable to [[Coq]], including tactics, while the focus remains on general-purpose programming even before theorem-proving. Other goals of Idris are "sufficient" performance, easy management of [[Side effect (computer science)|side-effects]] and support for implementing [[EDSL#Usage patterns|embedded ___domain specific languages]].

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>

{{As of|2014|10}}, Idris compiles to [[C (programming language)|C]] and relies on a custom copying [[Garbage collection (computer science)|garbage collector]] using [[Cheney's algorithm]]. There also exist [[JavaScript]] and [[Java]] backends, and a partial [[LLVM]] backend.<ref>http://idris-lang.org/news</ref>

==Features==

The name ''Idris'' goes back to the character of the singing dragon in the 70's UK kids' program [[Ivor the Engine#Idris the Dragon|Ivor the Engine]].<ref>http://idris-lang.org/documentation/faq</ref>

Idris combines a number of features from relatively mainstream functional programming languages with features borrowed from [[proof assistants, in effect blurring the boundary between the two kinds of softwareassistant]]s.

==Syntax==

===Functional programming===

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

<source lang="haskell">

<syntaxhighlight 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 Nevertheless,web Idris|url=https://docs.idris-lang.org/en/v1.3.2/reference/syntax-guide.html supports|title=Syntax ''where''Guide clauses,– ''with''Idris rule,1.3.2 simpledocumentation ''case''|access-date=27 expressions,April pattern matching, ''let'' and lambda bindings.2020}}</ref>

===Inductive and parametric data types===

The following is a common example that makes use of dependent types:

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

<sourcesyntaxhighlight lang="haskellidris">

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

</syntaxhighlight>

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

<syntaxhighlight lang="idris">

data Tree : Type -> Type where

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

Leaf : a -> Tree a

</syntaxhighlight>

===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 [[type checking]]. The following defines a type of lists whose lengths are known before the program runs, traditionally called [[Array data structure|vectors]]:

<syntaxhighlight lang="idris">

data Vect : Nat -> Type -> Type where

Nil : Vect 0 a

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

</syntaxhighlight>

This type can be used as follows:

<syntaxhighlight 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 be have exactly (<code>n</code> + <code>m</code>) elements of type <code>a</code>.

The word "<code>total</code>" invokes the [[PartialTermination functionanalysis|totality checker]] which will report an error if the marked 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="haskellidris">

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

==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 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}}

Idris combines a number of features from relatively mainstream functional programming languages with features borrowed from proof assistants, in effect blurring the boundary between the two kinds of software.

===Code generation===

Idris is a fairly mature functional programming language similar to Haskell (albeit mostly call-by-value), with pattern matching, a rich basic type hierarchy (including machine integers, bignums, strings, floating-point numbers etc.), type classes, a foreign-function interface and imperative features encapsulated within an input/output monad. At the same time, Idris contains a reasonable proof assistant, which supports both the interaction style of Coq (tactics) and that of Epigram and Agda (interactive elaboration of proof terms).

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 latest 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 compiles togenerates native code through [[C, but(programming otherlanguage)|C]]. backendsThe are available that supportother compilationofficially tosupported Javascriptbackend andgenerates Java[[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.)]

* [http://www.cs.st-andrews.ac.uk/~eb/writings/idris-tutorial.pdf Idris Tutorial]

{{Haskell programming}}

{{Programming languages}}

[[Category:Dependently typed languages]]

[[Category:Experimental programming languages]]

[[Category:Functional languages]]

[[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]]

[[Category:High-level programming languages]]

[[Category:2007 software]]

[[Category:Pattern matching programming languages]]

[[Category:Statically typed programming languages]]