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

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

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). The b ...

, and features such as a totality checker. Idris may be used as a

proof assistant 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 ...

, 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 exam ...

similar to

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

. 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 Agda may refer to: * Agda (programming language), the programming language and theorem prover * Agda (Golgafrinchan), the character in ''The Hitchhiker's Guide to the Galaxy'' by Douglas Adams * Liten Agda, the heroine of a Swedish legend * Agda M ...

's, and proofs are similar to

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

's, including

tactics Tactic(s) or Tactical may refer to: * Tactic (method), a conceptual action implemented as one or more specific tasks ** Military tactics, the disposition and maneuver of units on a particular sea or battlefield ** Chess tactics ** Political tact ...

(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 A waste collector, also known as a garbageman, garbage collector, trashman (in the US), binman or (rarely) dustman (in the UK), is a person employed by a public or private enterprise to collect and dispose of municipal solid waste (refuse) and r ...

using

Cheney's algorithm Cheney's algorithm, first described in a 1970 Association for Computing Machinery, ACM paper by C.J. Cheney, is a stop and copy method of tracing garbage collection in computer software systems. In this scheme, the Memory management#Dynamic memory ...

) 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 Node.js is an open-source server environment. Node.js is cross-platform and runs on Windows, Linux, Unix, and macOS. Node.js is a back-end JavaScript runtime environment. Node.js runs on the V8 JavaScript Engine and executes JavaScript code o ...

-based). There are third-party code generators for other platforms, including

JVM A Java virtual machine (JVM) is a virtual machine that enables a computer to run Java programs as well as programs written in other languages that are also compiled to Java bytecode. The JVM is detailed by a specification that formally describes ...

, 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 represen ...

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

Ivor the Engine ''Ivor the Engine'' is a British cutout animation television series created by Oliver Postgate and Peter Firmin's Smallfilms company. It follows the adventures of a small green steam locomotive who lives in the "top left-hand corner of Wales" ...

''.

Features

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

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

of the main function, and the omission of the word "where" in the

module Module, modular and modularity may refer to the concept of modularity. They may also refer to: Computing and engineering * Modular design, the engineering discipline of designing complex devices using separately designed sub-components * Mo ...

declaration.

Inductive and parametric data types

Idris supports inductively-defined data types 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 In functional programming, a generalized algebraic data type (GADT, also first-class phantom type, guarded recursive datatype, or equality-qualified type) is a generalization of parametric polymorphism, parametric algebraic data types. Overview I ...

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

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

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 A scheme is a systematic plan for the implementation of a certain idea. Scheme or schemer may refer to: Arts and entertainment * ''The Scheme'' (TV series), a BBC Scotland documentary series * The Scheme (band), an English pop band * ''The Schem ...

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