\section{Introduction}

In conventional programming languages, there is a clear distinction between
\remph{types} and \remph{values}. For example, in Haskell~\cite{haskell-report},
the following are types, representing integers, characters, lists of characters,
and lists of any value respectively:

\begin{itemize}
\item \texttt{Int}, \texttt{Char}, \texttt{[Char]}, \texttt{[a]}
\end{itemize}

\noindent
Correspondingly, the following values are examples of inhabitants of those types:

\begin{itemize}
\item \texttt{42}, \texttt{'a'}, \texttt{"Hello world!"}, \texttt{[2,3,4,5,6]}
\end{itemize}

In a language with \emph{dependent types}, however, the distinction is less
clear.  Dependent types allow types to ``depend'' on values. The standard
example is the type of lists of a given length\footnote{Typically, and perhaps
confusingly, referred to in the dependently typed programming literature as
``vectors''}, \texttt{Vect a n}, where \texttt{a} is the element type and
\texttt{n} is the length of the list and can be an arbitrary
term.

When types can contain values, and where those values describe properties (e.g.
the length of a list)
functions over those types begin to describe their own properties. For example,
concatenating two lists has the property that the resulting list's length is
the sum of the lengths of the two input lists. We can therefore give the following type 
to the  \texttt{app} function, which concatenates vectors: 

\begin{SaveVerbatim}{appendv}

app : Vect a n -> Vect a m -> Vect a (n + m);

\end{SaveVerbatim}
\useverb{appendv}


This tutorial introduces \Idris{}, a general purpose dependently typed functional 
programming language.
The goal of the \Idris{} project is to build a dependently typed language suitable
for verifable \emph{systems} programming. To this end, \Idris{} is a compiled language
which aims to generate efficient executable code. It also has a lightweight foreign
function interface which allows easy interaction with external C libraries.

\subsection{Intended Audience}

This tutorial is intended as a brief introduction to the language, and is aimed
at readers already familiar with a functional language such as Haskell or
OCaml. In particular, a certain amount of familiarity with Haskell syntax is
assumed, although most concepts will at least be explained briefly.  The reader
is also assumed to have some interest in using dependent types for writing and
verifying systems software.