Idris (programming language)

Last updated
Idris
Paradigm Functional
Designed by Edwin Brady
First appeared2007;18 years ago (2007) [1]
Stable release
1.3.4 [2] / October 22, 2021;3 years ago (2021-10-22)
Preview release
0.7.0 (Idris 2) [3] / December 22, 2023;20 months ago (2023-12-22)
Typing discipline Inferred, static, strong
OS Cross-platform
License BSD
Filename extensions .idr, .lidr
Website idris-lang.org
Influenced by
Agda, Clean, [4] Rocq (previously known as Coq), [5] Epigram, F#, Haskell, [5] ML, [5] Rust [4]

Idris is a purely-functional programming language with dependent types, optional lazy evaluation, and features such as a totality checker. Idris may be used as a proof assistant, but is designed to be a general-purpose programming language similar to Haskell.

Contents

The Idris type system is similar to Agda's, and proofs are similar to Rocq's, including tactics (theorem proving functions/procedures) via elaborator reflection. [6] Compared to Agda and Rocq, Idris prioritizes management of side effects and support for embedded domain-specific languages. Idris compiles to C (relying on a custom copying 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. [7]

Idris is named after a singing dragon from the 1970s UK children's television program Ivor the Engine . [8]

Features

Idris combines a number of features from relatively mainstream functional programming languages with features borrowed from proof assistants.

Functional programming

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

moduleMainmain:IO() main=putStrLn"Hello, World!"

The only differences between this program and its Haskell equivalent are the single (instead of double) colon in the type signature of the main function, and the omission of the word "where" in the module declaration. [9]

Inductive and parametric data types

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

dataTreea=Node(Treea)(Treea)|Leafa

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

dataTree:Type->TypewhereNode:Treea->Treea->Treea Leaf:a->Treea

Dependent types

With dependent types, 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 vectors:

dataVect:Nat->Type->TypewhereNil:Vect0a (::):(x:a)->(xs:Vectna)->Vect(n+1)a

This type can be used as follows:

totalappend:Vectna->Vectma->Vect(n+m)a appendNilys=ys append(x::xs)ys=x::appendxsys

The function append appends a vector of m elements of type a to a vector of n elements of type a. 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 (n + m) elements of type a. The word "total" invokes the totality checker which will report an error if the 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:

totalpairAdd:Numa=>Vectna->Vectna->Vectna pairAddNilNil=Nil pairAdd(x::xs)(y::ys)=x+y::pairAddxsys

Num a signifies that the type a belongs to the type class Num. Note that this function still typechecks successfully as total, even though there is no case matching Nil 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 (Rocq 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 Rocq.[ vague ]

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. [10] [11]

By default, Idris generates native code through C. The other officially supported backend generates JavaScript.

Idris 2

Idris 2 is a new self-hosted version of the language which deeply integrates a linear type system, based on quantitative type theory. It currently compiles to Scheme and C. [12]

See also

References

  1. ↑ Brady, Edwin (12 December 2007). "Index of /~eb/darcs/Idris". University of St Andrews School of Computer Science. Archived from the original on 2008-03-20.
  2. ↑ "Release 1.3.4". GitHub . Retrieved 2022-12-31.
  3. ↑ "Idris 2 version 0.7.0 Released". GitHub . Retrieved 2024-04-20.
  4. 1 2 "Uniqueness Types". Idris 1.3.1 Documentation. Retrieved 2019-09-26.
  5. 1 2 3 "Idris, a language with dependent types" . Retrieved 2014-10-26.
  6. ↑ "Elaborator Reflection – Idris 1.3.2 documentation" . Retrieved 27 April 2020.
  7. ↑ "Code Generation Targets – Idris Latest documentation". docs.idris-lang.org.
  8. ↑ "Frequently Asked Questions" . Retrieved 2015-07-19.
  9. ↑ "Syntax Guide – Idris 1.3.2 documentation" . Retrieved 27 April 2020.
  10. ↑ "Erasure By Usage Analysis – Idris latest documentation". idris.readthedocs.org.
  11. ↑ "Benchmark results". ziman.functor.sk.
  12. ↑ "idris-lang/Idris2". GitHub. Retrieved 2021-04-11.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.