Wikipedia

Idris (programming language)

This is an old revision of this page, as edited by Msnicki (talk | contribs) at 21:14, 27 April 2013 (Nominated for deletion; see Wikipedia:Articles for deletion/Idris (programming language). (TW)). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

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

Idris
ParadigmFunctional
Designed byEdwin Brady
Stable release
0.9.7 / March 10, 2013 (2013-03-10)
OSCross-platform
LicenseBSD-3
Filename extensions.idr
WebsiteIdris website
Influenced by
Agda, Epigram, Haskell, ML, Coq

The language supports interactive theorem-proving compareable 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.

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

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 a n -> Vect a m -> Vect a (n + m)
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.

References

Retrieved from "https://en.wikipedia.org/w/index.php?title=Idris_(programming_language)&oldid=552473671"