Idris (programming language): Difference between revisions

Revision as of 10:46, 29 May 2013

Revision as of 09:26, 9 June 2013

Line 20:

}}

'''Idris''' is a general-purpose pure [[Functional programming languages|functional]] programming language with [[Dependentdependent type|dependent types]]s. The [[type system]] is similar to the one used by [[Agda]].

The language supports [[Proof assistant|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_effect_Side effect (computer_sciencecomputer science)|side-effects]] and support for implementing [[EDSL#Usage_patterns|embedded ___domain specific languages]].

Currently, Idris compiles to [[C (programming language)|C]] and relies on a custom copying [[Garbage collection (computer_sciencecomputer science)|garbage collector]] using [[Cheney's algorithm]]. There also exist [[JavaScript]] and [[Java]] backends, and a partial [[LLVM]] backend.<ref>http://idris-lang.org/news</ref>.

The name ''Idris'' goes back to the character of the singing dragon in the 70's UK kids' program [[Ivor_the_Engine#Idris_the_Dragon|Ivor the Engine]].<ref>http://idris-lang.org/documentation/faq</ref>.

==Syntax==