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 deﬁned 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 deﬁne 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.