Content deleted Content added
New Version 0.9.8 |
LambdaTotoro (talk | contribs) Added second syntax example and changed reference style. |
||
Line 24:
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_patterns|embedded ___domain specific languages]].
Currently, 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_Engine#Idris_the_Dragon|Ivor the Engine]]<ref>http://idris-lang.org/documentation/faq</ref>.
==Syntax==
Line 51:
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 [[Partial function|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:
<source lang="haskell">
total
pairAdd : Num a => Vect a n -> Vect a n -> Vect a n
pairAdd Nil Nil = Nil
pairAdd (x::xs) (y::ys) = (x+y) :: pairAdd xs ys
</source>
Num a signifies that the type a belongs to the [[type class]] Num. Note that this function is 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 must have, ensured via type system, exactly the same length we can be sure at compile time that this is a case that will not occur. Hence it does not need to be mentioned for the function to be total.
==References==
{{
==External links==
| |||