# edwinb/Idris-dev forked from idris-lang/Idris-dev

### Subversion checkout URL

You can clone with
or
.
Fetching contributors…

Cannot retrieve contributors at this time

69 lines (54 sloc) 2.952 kB
 \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} \noindent In a language with \emph{dependent types}, however, the distinction is less clear. Dependent types allow types to depend'' on values --- in other words, types are a \emph{first class} language construct and can be manipulated like any other value. 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) the type of a function can begin to describe its 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} \noindent This tutorial introduces \Idris{}, a general purpose functional programming language with dependent types. The goal of the \Idris{} project is to build a dependently typed language suitable for verifiable \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. \subsection{Example Code} This tutorial includes some example code, which has been tested with \Idris{} version 0.9.2. The files are available in the \Idris{} distribution, so that you can try them out easily, under \texttt{tutorial/examples}. However, it is strongly recommended that you type them in yourself, rather than simply loading and reading them.
Something went wrong with that request. Please try again.