Idris (programming language): Difference between revisions

Revision as of 11:44, 4 December 2014

Latest revision as of 12:44, 15 November 2024

(130 intermediate revisions by 79 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>

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>

==Features==

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.

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.

===Functional programming===

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

<syntaxhighlight lang="idris">

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

<source lang="haskell">

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

Like most modern functional programming languages, Idris supports a notion of [[inductively-defined data type]]s and [[parametric polymorphism]]. Such types can be defined both in traditional "Haskell98"''[[Haskell]] 98''-like syntax:

<syntaxhighlight lang="idris">

Like most modern functional programming languages, Idris supports a notion of inductively-defined data type and parametric polymorphism. Such types can be defined both in traditional "Haskell98" syntax:

<source lang="haskell">

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

</syntaxhighlight>

</source>

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

<sourcesyntaxhighlight lang="haskellidris">

data Tree : Type -> Type where

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

Leaf : a -> Tree a

</syntaxhighlight>

</source>

====Dependent types====

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

<syntaxhighlight lang="idris">

With [[Dependent type|dependent types]], it is possible for values to appear in the types; in effect, any value-level computation can be performed during typechecking. The following defines a type of lists of statically known length, traditionally called 'vectors':

<source lang="haskell">

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

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

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/Agda (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}}

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/Agda style). Idris supports both modes of interaction, although the set of available tactics is not yet as useful as that of Coq.

===Code generation===

Because Idris contains a proof assistant, Idris programs can be written to pass proofproofs around. If treated naivelynaïvely, such proofs remain around at runtime. Idris aims to avoid this pitfall by aggressively erasing unused terms,.<ref>https{{cite web |url=http://githubidris.readthedocs.comorg/idris-langen/Idris-devlatest/wikireference/erasure.html |title=Erasure-by-usage-analysis</ref> withBy promisingUsage resultsAnalysis – 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 generates native code through [[C (programming language)|C]]. The other officially supported backend generates [[JavaScript]].

Because Idris contains a proof assistant, Idris programs can be written to pass proof around. If treated naively, such proofs remain around at runtime. Idris aims to avoid this pitfall by aggressively erasing unused terms,<ref>https://github.com/idris-lang/Idris-dev/wiki/Erasure-by-usage-analysis</ref> with promising results.<ref>http://ziman.functor.sk/erasure-bm/</ref>

==Idris 2==

By default, Idris generates native code by going through C. Other backends are available for generating Javascript and Java.

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