Idris (programming language): Difference between revisions

Revision as of 19:58, 29 April 2013

Revision as of 10:30, 25 May 2013

Line 20:

}}

'''Idris''' is a general-purpose pure [[Functional programming languages|functional]] programming language with [[Dependent type|dependent types]]. The [[Type_system|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_(computer_science)|side-effects]] and support for implementing [[EDSL#Usage_patterns|embedded ___domain specific languages]].

Line 49:

</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 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.