Idris (programming language)

Idris is a general-purpose pure 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.

Currently, 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.^[1]

The name Idris goes back to the character of the singing dragon in the 70's UK kids' program Ivor the Engine.^[2]

Syntax

The Syntax of Idris shows many similarities with that of Haskell. A hello world program 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 colon (instead of two) in the signature of the main function and the omission of the word "where" in the module declaration. Nevertheless, Idris supports where clauses, with rule, simple case expressions, pattern matching, let and lambda bindings.

The following is a common example that makes use of dependent types:

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 functions 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 be have exactly (n + m) elements of type a. The word "total" invokes the totality checker which will report an error if the marked function doesn't cover all possible cases.

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 Num. Note that this function is still typechecks successfully as total, even though there is no case matching Nil in one vector and a number in the other. Since both vectors must have, ensured via type system, exactly the same length we can be sure at compile time that this is a case that will not occur. Hence it does not need to be mentioned for the function to be total.

References

External links

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