Idris (programming language): Difference between revisions

Revision as of 20:45, 13 November 2014

Revision as of 20:56, 13 November 2014

Line 28:

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>

==SyntaxFeatures==

Idris combines a number of features from relatively mainstream functional programming languages with features borrowed from proof assistants, in effect blurring the boundary between the two kinds of software.

===Functional programming===

The Syntax of Idris shows many similarities with that of Haskell. A [[hello world program]] in Idris might look like this:

Line 38 ⟶ 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. Nevertheless, Idris supports ''where'' clauses, ''with'' rule, simple ''case'' expressions, pattern matching, ''let'' and lambda bindings.

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

The following is a common example that makes use of dependent types:

Like most modern functional programming languages, Idris supports a notion of inductively-defined data type and parametric polymorphism. Such types can be defined both in traditional "Haskell98" syntax:

<source lang="haskell">

data Tree a = Node (Tree a) (Tree a) | Leaf

</source>

or in the more general [[GADT]] syntax:

<source lang="haskell">

data Tree : Type -> Type where

Node : Tree a -> Tree a -> Tree a

Leaf : a -> Tree a

</source>

====Dependent types====

With [[Dependent Types]], it is possible for values to appear in the types; in effect, any value-level computation can be performed during typechecking. The following defines a type of lists of statically known length, traditionally called 'vectors':

<source lang="haskell">

data Vect : Nat -> Type -> Type where

Nil : Vect 0 a

(::) : (x : a) -> (xs : Vect n a) -> Vect (n + 1) a

This type can be used as follows:

<source lang="haskell">

Line 63 ⟶ 92:

Num a signifies that the type a belongs to the [[type class]] Num. Note that this function 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 are ensured by the type system to have exactly the same length, we can be sure at compile time that this case will not occur. Hence it does not need to be mentioned for the function to be total.

===Proof assistant features===

==Features==

Idris combines a number of features from relatively mainstream functional programming languages with features borrowed from proof assistants, in effect blurring the boundary between the two kinds of software.

Idris is a fairly mature functional programming language similar to [[Haskell (programming language)|Haskell]] (albeit mostly call-by-value), with pattern matching, a rich basic type hierarchy (including machine integers, bignums, strings, floating-point numbers etc.), type classes, a foreign-function interface and imperative features encapsulated within an input/output monad. At the same time, Idris contains a reasonable proof assistant, which supports both the interaction style of [[Coq]] (tactics) and that of [[Epigram (programming language)|Epigram]] and [[Agda (programming language)|Agda]] (interactive elaboration of proof terms).

===Code generation===

By default, Idris compiles to native code through C, but other backends are available that support compilation to Javascript and Java.

==References==