Idris (programming language): Difference between revisions

Revision as of 09:43, 2 November 2014

Revision as of 23:13, 10 November 2014

Line 13:

| dialects =

| influenced =

| influenced_by = [[Agda (programming language)|Agda]], [[Coq]] ,<ref name="idris-web">{{cite web|title=Idris, a language with dependent types|url=http://www.idris-lang.org/|accessdate=2014-10-26}}</ref>, [[Epigram (programming language)|Epigram]], [[Haskell (programming language)|Haskell]],<ref name="idris-web"/> [[ML (programming language)|ML]],<ref name="idris-web"/>

| license = BSD-3

| website = [http://idris-lang.org/ Idris website]

Line 22:

'''Idris''' is a general-purpose pure [[Functional programming languages|functional]] programming language with [[dependent type]]s. The [[type system]] is similar to the one used by [[Agda (programming language)|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 (computer science)|side-effects]] and support for implementing [[EDSL#Usage_patternsUsage patterns|embedded ___domain specific languages]].

{{As of|2014|10}}, Idris compiles to [[C (programming language)|C]] and relies on a custom copying [[Garbage collection (computer 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_EngineIvor the Engine#Idris_the_DragonIdris the Dragon|Ivor the Engine]].<ref>http://idris-lang.org/documentation/faq</ref>

==Syntax==