Idris (programming language)

From Wikipedia, the free encyclopedia
Jump to: navigation, search
Idris
Paradigm(s) Functional
Designed by Edwin Brady
Stable release 0.9.14 / July 16, 2014 (2014-07-16)
Influenced by Agda, Coq, Epigram, Haskell, ML
OS Cross-platform
License BSD-3
Filename extension(s) .idr, .lidr
Website Idris website

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[edit]

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 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 are ensured by the type system to have exactly the same length, we can be sure at compile time that this case will not occur. Hence it does not need to be mentioned for the function to be total.

References[edit]

External links[edit]