Idris (programming language): Difference between revisions

Revision as of 16:58, 19 June 2021

Revision as of 18:58, 19 June 2021

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

Line 58:

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

<syntaxhighlight lang="idris">

Line 75:

</syntaxhighlight>

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:

Line 87:

</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 (programming language)|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.1 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]].