Idris is a purely-functional

programming language A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming l ...

with

dependent type 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 l ...

s, optional

lazy evaluation In programming language theory, lazy evaluation, or call-by-need, is an evaluation strategy which delays the evaluation of an expression until its value is needed ( non-strict evaluation) and which also avoids repeated evaluations ( sharing). T ...

, and features such as a totality checker. Idris may be used as a proof assistant, but it is designed to be a

general-purpose programming language In computer software, a general-purpose programming language (GPL) is a programming language for building software in a wide variety of application domains. Conversely, a domain-specific programming language is used within a specific area. For ex ...

similar to Haskell. The Idris

type system In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer progra ...

is similar to Agda's, and proofs are similar to Coq's, including

tactics Tactic(s) or Tactical may refer to: * Tactic (method), a conceptual action implemented as one or more specific tasks ** Military tactics Military tactics encompasses the art of organizing and employing fighting forces on or near the battlefiel ...

(theorem proving functions/procedures) via elaborator reflection. Compared to Agda and Coq, Idris prioritizes management of

side effects In medicine, a side effect is an effect, whether therapeutic or adverse, that is secondary to the one intended; although the term is predominantly employed to describe adverse effects, it can also apply to beneficial, but unintended, consequence ...

and support for embedded domain-specific languages. Idris compiles to C (relying on a custom copying garbage collector using Cheney's algorithm) and

JavaScript JavaScript (), often abbreviated as JS, is a programming language that is one of the core technologies of the World Wide Web, alongside HTML and CSS. As of 2022, 98% of Website, websites use JavaScript on the Client (computing), client side ...

(both browser- and Node.js-based). There are third-party code generators for other platforms, including JVM, CIL, and

LLVM LLVM is a set of compiler and toolchain technologies that can be used to develop a front end for any programming language and a back end for any instruction set architecture. LLVM is designed around a language-independent intermediate repre ...

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

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 ''Hello'' is a salutation or greeting in the English language. It is first attested in writing from 1826. Early uses ''Hello'', with that spelling, was used in publications in the U.S. as early as the 18 October 1826 edition of the '' Norwich ...

in Idris might look like this: module Main main : 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 In computer science, a type signature or type annotation defines the inputs and outputs for a function, subroutine or method. A type signature includes the number, types, and order of the arguments contained by a function. A type signature is ty ...

of the main function, and the omission of the word "where" in the module declaration.

Inductive and parametric data types

Idris supports

inductively-defined data type In computer programming languages, a recursive data type (also known as a recursively-defined, inductively-defined or inductive data type) is a data type for values that may contain other values of the same type. Data of recursive types are usuall ...

s and

parametric polymorphism In programming languages and type theory, parametric polymorphism allows a single piece of code to be given a "generic" type, using variables in place of actual types, and then instantiated with particular types as needed. Parametrically polymorph ...

. Such types can be defined both in traditional " Haskell98"-like syntax: data Tree a = Node (Tree a) (Tree a) , Leaf a or in the more general GADT-like syntax: data Tree : Type -> Type where Node : Tree a -> Tree a -> Tree a Leaf : a -> Tree a

Dependent types

With

s, it is possible for values to appear in the types; in effect, any value-level computation can be performed during

type checking In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer program ...

. The following defines a type of lists whose lengths are known before the program runs, traditionally called vectors: data Vect : Nat -> Type -> Type where Nil : Vect 0 a (::) : (x : a) -> (xs : Vect n a) -> Vect (n + 1) a This type can be used as follows: total append : Vect n a -> Vect m a -> Vect (n + m) a append Nil ys = ys append (x :: xs) ys = x :: append xs ys 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 In computer science, compile time (or compile-time) describes the time window during which a computer program is compiled. The term is used as an adjective to describe concepts related to the context of program compilation, as opposed to concept ...

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 In computer programming, an infinite loop (or endless loop) is a sequence of instructions that, as written, will continue endlessly, unless an external intervention occurs ("pull the plug"). It may be intentional. Overview This differs from: * ...

. Another common example is pairwise addition of two vectors that are parameterized over their length: 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 Num a signifies that the type a belongs to the

type class 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 a ...

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 An epigram is a brief, interesting, memorable, and sometimes surprising or satirical statement. The word is derived from the Greek "inscription" from "to write on, to inscribe", and the literary device has been employed for over two mille ...

/Agda style). Idris supports both modes of interaction, although the set of available tactics is not yet as useful as that of Coq.

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. By default, Idris generates native code through C. The other officially supported backend generates

Idris 2

Idris 2 is a new self-hosted version of the language which deeply integrates a

linear type system Substructural type systems are a family of type systems analogous to substructural logics where one or more of the structural rules are absent or only allowed under controlled circumstances. Such systems are useful for constraining access to sy ...

, based on quantitative type theory. It currently compiles to Scheme and C.

References

External links

The Idris homepage
including documentation, frequently asked questions and examples
Idris at the Hackage repository

{{Programming languages Dependently typed languages Experimental programming languages Functional languages Free software programmed in Haskell Haskell programming language family Cross-platform free software Free compilers and interpreters Software using the BSD license Programming languages created in 2007 High-level programming languages 2007 software Pattern matching programming languages