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