Idris (programming language)

Last updated
Idris
Paradigm Functional
Designed by Edwin Brady
First appeared2007;16 years ago (2007) [1]
Stable release
1.3.4 [2] / October 22, 2021;2 years ago (2021-10-22)
Preview release
0.6.0 (Idris 2) [3] / October 28, 2022;12 months ago (2022-10-28)
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 which 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

In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that map values to other values, rather than a sequence of imperative statements which update the running state of the program.

ML is a functional programming language. It is known for its use of the polymorphic Hindley–Milner type system, which automatically assigns the 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.

<span class="mw-page-title-main">Abstract syntax tree</span> Tree representation of the abstract syntactic structure of source code

In computer science, an abstract syntax tree (AST), or just syntax tree, is a tree representation of the abstract syntactic structure of text written in a formal language. Each node of the tree denotes a construct occurring in the text.

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

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, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of theorem provers.

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.

Curry is an experimental functional logic programming language, based on the Haskell language. It merges elements of functional and logic programming, including constraint programming integration.

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 one 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.

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, and Idris, 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 known as 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 a number of 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).

Racket has been under active development as a vehicle for programming language research since the mid-1990s, and has accumulated many features over the years. This article describes and demonstrates some of these features. Note that one of Racket's main design goals is to accommodate creating new languages, both domain-specific languages and completely new languages. Therefore, some of the following examples are in different languages, but they are all implemented in Racket. Please refer to the main article for more information.

A conc-tree is a data structure that stores element sequences, and provides amortized O(1) time append and prepend operations, O(log n) time insert and remove operations and O(log n) time concatenation. This data structure is particularly viable for functional task-parallel and data-parallel programming, and is relatively simple to implement compared to other data-structures with similar asymptotic complexity. Conc-trees were designed to improve efficiency of data-parallel operations that do not require sequential left-to-right iteration order, and improve constant factors in these operations by avoiding unnecessary copies of the data. Orthogonally, they are used to efficiently aggregate data in functional-style task-parallel algorithms, as an implementation of the conc-list data abstraction. Conc-list is a parallel programming counterpart to functional cons-lists, and was originally introduced by the Fortress language.

Futhark is a functional data parallel array programming language 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, in particular on 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.

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" . Retrieved 2022-12-31.
  3. ↑ "Idris 2 version 0.6.0 Released". www.idris-lang.org. Retrieved 2022-12-31.
  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.