Idris (programming language): Difference between revisions

Revision as of 23:31, 6 April 2013

Latest revision as of 12:44, 15 November 2024

(173 intermediate revisions by 99 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.7

| latest_release_date latest release date = {{release_dateStart date and age|2013|032021|10|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 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]],<ref name="idris-web"/> [[ML (programming language)|ML]],<ref name="idris-web"/> [[Rust (programming language)|Rust]]<ref name="uniqueness-types"/>

| influenced =

| influenced =

| influenced_by = [[Agda (programming language)|Agda]], [[Epigram (programming language)|Epigram]], [[Haskell (programming language)|Haskell]], [[ML (programming language)|ML]], [[Coq]]

| 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 [[Dependentdependent type]]s, optional [[lazy evaluation]], and features such as a [[Termination analysis|dependenttotality typeschecker]]. TheIdris may be used as a [[Type_system|typeproof systemassistant]], but is similardesigned to thebe onea used[[general-purpose byprogramming language]] similar to [[AgdaHaskell]].

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

Currently, 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 exists a [[JavaScript]] backend.

==Features==

Idris combines a number of features from relatively mainstream functional programming languages with features borrowed from [[proof assistant]]s.

===Functional programming===

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

<syntaxhighlight lang="idris">

module Main

main : IO ()

main = putStrLn "Hello, World!"

</syntaxhighlight>

The only differences between this program and its [[Haskell#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''-like syntax:

<syntaxhighlight lang="idris">

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>

The function <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:

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

<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. Because the type system can prove that the vectors have the same length, we can be sure at compile time that case will not occur and there is no need to include that case in the function’s definition.

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

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

{{refbeginReflist}}

* Brady: IDRIS — Systems Programming Meets Full Dependent Types, PLPV 2012 http://www.cs.st-andrews.ac.uk/~eb/writings/plpv11.pdf

* Brady: Programming in Idris: a tutorial http://www.cs.st-andrews.ac.uk/~eb/writings/idris-tutorial.pdf

* Brady, Hammond: Resource-safe Systems Programming with Embedded Domain Specific Languages, PADL 2012 http://www.cs.st-andrews.ac.uk/~eb/drafts/dsl-idris.pdf

{{refend}}

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