Content deleted Content added
No edit summary |
LambdaTotoro (talk | contribs) Added Syntax section |
||
Line 25:
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.
==Syntax==
The Syntax of Idris shows many similarities with that of Haskell. A [[hello world program]] in Idris might look like this:
<source lang="haskell">
module Main
main : IO ()
main = putStrLn "Hello, World!"
</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. 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:
<source lang="haskell">
total
append : Vect a n -> Vect a m -> Vect a (n + m)
append Nil ys = ys
append (x :: xs) ys = x :: (append xs ys)
</source>
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 cartain 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.
==References==
| |||