Idris (programming language)

Last updated
Idris
Paradigm Functional
Designed by Edwin Brady
First appeared2007;17 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;10 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] 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 Coq's, including tactics (theorem proving functions/procedures) via elaborator reflection. [6] Compared to Agda and Coq, 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 (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.[ 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

Related Research Articles

ML is a general-purpose, high-level, functional programming language. It is known for its use of the polymorphic Hindley–Milner type system, which automatically assigns the data types of most expressions without requiring explicit type annotations, and ensures type safety; there is a formal proof that a well-typed ML program does not cause runtime type errors. ML provides pattern matching for function arguments, garbage collection, imperative programming, call-by-value and currying. While a general-purpose programming language, ML is used heavily in programming language research and is one of the few languages to be completely specified and verified using formal semantics. Its types and pattern matching make it well-suited and commonly used to operate on other formal languages, such as in compiler writing, automated theorem proving, and formal verification.

OCaml is a general-purpose, high-level, multi-paradigm programming language which extends the Caml dialect of ML with object-oriented features. OCaml was created in 1996 by Xavier Leroy, Jérôme Vouillon, Damien Doligez, Didier Rémy, Ascánder Suárez, and others.

<span class="mw-page-title-main">Miranda (programming language)</span> Programming language by David Turner

Miranda is a lazy, purely functional programming language designed by David Turner as a successor to his earlier programming languages SASL and KRC, using some concepts from ML and Hope. It was produced by Research Software Ltd. of England and was the first purely functional language to be commercially supported.

Standard ML (SML) is a general-purpose, high-level, modular, functional programming language with compile-time type checking and type inference. It is popular for writing compilers, for programming language research, and for developing theorem provers.

<span class="mw-page-title-main">Clean (programming language)</span> Functional programming language

Clean is a general-purpose purely functional programming language. Originally called the Concurrent Clean System or the Clean System, it has been developed by a group of researchers from the Radboud University in Nijmegen since 1987. Although development of the language has slowed, some researchers are still working in the language. In 2018, a spin-off company was founded that uses Clean.

In computer science, pattern matching is the act of checking a given sequence of tokens for the presence of the constituents of some pattern. In contrast to pattern recognition, the match usually has to be exact: "either it will or will not be a match." The patterns generally have the form of either sequences or tree structures. Uses of pattern matching include outputting the locations of a pattern within a token sequence, to output some component of the matched pattern, and to substitute the matching pattern with some other token sequence.

In computer programming, especially functional programming and type theory, an algebraic data type (ADT) is a kind of composite type, i.e., a type formed by combining other types.

In computer science, a tagged union, also called a variant, variant record, choice type, discriminated union, disjoint union, sum type, or coproduct, is a data structure used to hold a value that could take on several different, but fixed, types. Only one of the types can be in use at any one time, and a tag field explicitly indicates which type is in use. It can be thought of as a type that has several "cases", each of which should be handled correctly when that type is manipulated. This is critical in defining recursive datatypes, in which some component of a value may have the same type as that value, for example in defining a type for representing trees, where it is necessary to distinguish multi-node subtrees and leaves. Like ordinary unions, tagged unions can save storage by overlapping storage areas for each type, since only one is in use at a time.

<span class="mw-page-title-main">Coq (software)</span> Proof assistant

Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics (procedures) and various decision procedures.

<span class="mw-page-title-main">Proof assistant</span> Software tool to assist with the development of formal proofs by human–machine collaboration

In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human–machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.

In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers like "for all" and "there exists". In functional programming languages like Agda, ATS, Coq, F*, Epigram, Idris, and Lean, dependent types help reduce bugs by enabling the programmer to assign types that further restrain the set of possible implementations.

In computer science, a type class is a type system construct that supports ad hoc polymorphism. This is achieved by adding constraints to type variables in parametrically polymorphic types. Such a constraint typically involves a type class T and a type variable a, and means that a can only be instantiated to a type whose members support the overloaded operations associated with T.

In computer programming, append is the operation for concatenating linked lists or arrays in some high-level programming languages.

<span class="mw-page-title-main">Agda (programming language)</span> Functional programming language

Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis. The original Agda system was developed at Chalmers by Catarina Coquand in 1999. The current version, originally named Agda 2, is a full rewrite, which should be considered a new language that shares a name and tradition.

In functional programming, fold refers to a family of higher-order functions that analyze a recursive data structure and through use of a given combining operation, recombine the results of recursively processing its constituent parts, building up a return value. Typically, a fold is presented with a combining function, a top node of a data structure, and possibly some default values to be used under certain conditions. The fold then proceeds to combine elements of the data structure's hierarchy, using the function in a systematic way.

This article describes the features in the programming language Haskell.

Haskell is a general-purpose, statically-typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research, and industrial applications, Haskell has pioneered several programming language features such as type classes, which enable type-safe operator overloading, and monadic input/output (IO). It is named after logician Haskell Curry. Haskell's main implementation is the Glasgow Haskell Compiler (GHC).

<span class="mw-page-title-main">Elm (programming language)</span> Functional programming language

Elm is a domain-specific programming language for declaratively creating web browser-based graphical user interfaces. Elm is purely functional, and is developed with emphasis on usability, performance, and robustness. It advertises "no runtime exceptions in practice", made possible by the Elm compiler's static type checking.

Futhark is a multi-paradigm, high-level, functional, data parallel, array programming language. It is a dialect of the language ML, originally developed at UCPH Department of Computer Science (DIKU) as part of the HIPERFIT project. It focuses on enabling data parallel programs written in a functional style to be executed with high performance on massively parallel hardware, especially graphics processing units (GPUs). Futhark is strongly inspired by NESL, and its implementation uses a variant of the flattening transformation, but imposes constraints on how parallelism can be expressed in order to enable more aggressive compiler optimisations. In particular, irregular nested data parallelism is not supported. It is free and open-source software released under an ISC license.

This article compares the syntax for defining and instantiating an algebraic data type (ADT), sometimes also referred to as a tagged union, in various programming languages.

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.