Idris (programming language)

Idris is a general-purpose purely functional programming language with dependent types. The type system is similar to the one used by Agda.

The language supports interactive theorem-proving comparable to Coq, including tactics, while the focus remains on general-purpose programming even before theorem-proving. Other goals of Idris are "sufficient" performance, easy management of side-effects and support for implementing embedded domain specific languages.

As of October 2014^[update], Idris compiles to C and relies on a custom copying garbage collector using Cheney's algorithm. There also exist JavaScript and Java backends, and a partial LLVM backend.

The name Idris goes back to the character of the singing dragon in the 1970s UK kids' program Ivor the Engine.

Idris combines a number of features from relatively mainstream functional programming languages with features borrowed from proof assistants, in effect blurring the boundary between the two kinds of software.

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

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