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     = Z       | 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
Z     + 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 : Nat -> Type -> Type where
    Nil  : Vect Z a
    (::) : a -> Vect k a -> Vect (S k) a

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 n a -> Vect m a -> Vect (n + m) a
app Nil       ys = ys
app (x :: xs) ys = x :: app xs ys

For more details, see the documentation.