Idris (programming language): Difference between revisions

Revision as of 21:08, 13 November 2014

Revision as of 05:32, 14 November 2014

Line 42:

</source>

The only differences between this program and its [[Haskell (programming language)#Code examples|Haskell equivalent]] are the single colon (instead of two) in the [[Type signature|signature]] of the main function and the omission of the word "where" in the module declaration.

====Inductive and parametric data types====

Line 100:

===Code generation===

Because Idris contains a proof assistant, Idris programs can be written to pass proof around. If treated naively, such proofs remain around at runtime. Idris aims to avoid this pitfall by aggressively erasing unused terms,<ref>https://github.com/idris-lang/Idris-dev/wiki/Erasure-by-usage-analysis</ref>, with promising results.<ref>http://ziman.functor.sk/erasure-bm/</ref>.

By default, Idris generates native code by going through C. Other backends are available for generating Javascript and Java.