Idris (programming language)
|Designed by||Edwin Brady|
|Stable release||0.9.14 / July 16, 2014|
|Influenced by||Agda, Coq, Epigram, Haskell, ML|
|Filename extension(s)||.idr, .lidr|
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.
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.