Example

Idris data types are declared using a similar syntax to Haskell data types. For example, natural numbers, an option type and lists are declared in the standard library:

data Nat     = O       | S Nat
data Maybe a = Nothing | Just a
data List a  = Nil     | (::) a (List a)

Functions are implemented by pattern matching. For example, addition on natural numbers can be defined as follows, again taken from the standard library:

(+) : Nat -> Nat -> Nat
O     + y = y
(S k) + y = S (k + y)

Like Haskell, functions such as (+) above may be overloaded using type classes.

Vectors are lists which carry their size in the type. They are declared as follows in the standard library, using a syntax similar to that for Generalised Algebraic Data Types (GADTs) in Haskell:

infixr 5 ::

data Vect : Type -> Nat -> Type where
    Nil  : Vect a O
    (::) : a -> Vect a k -> Vect a (S k)

We can define functions by pattern matching. The type of a function over Vect will describe what happens to the lengths of the vectors involved. For example, app appends two Vects, returning a vector which is the sum of the lengths of the inputs:

app : Vect a n -> Vect a m -> Vect a (n + m)
app Nil       ys = ys
app (x :: xs) ys = x :: app xs ys

For more details, see the documentation.