git.iko.soy/Idris-dev
on 11d4fee help sign in
Idris-dev/tutorial/intro.tex
56 lines 2.5 kB history raw
1\section{Introduction}
3In conventional programming languages, there is a clear distinction between
4\remph{types} and \remph{values}. For example, in Haskell~\cite{haskell-report},
5the following are types, representing integers, characters, lists of characters,
6and lists of any value respectively:
8\begin{itemize}
9\item \texttt{Int}, \texttt{Char}, \texttt{[Char]}, \texttt{[a]}
10\end{itemize}
12\noindent
13Correspondingly, the following values are examples of inhabitants of those types:
15\begin{itemize}
16\item \texttt{42}, \texttt{'a'}, \texttt{"Hello world!"}, \texttt{[2,3,4,5,6]}
17\end{itemize}
19In a language with \emph{dependent types}, however, the distinction is less
20clear. Dependent types allow types to ``depend'' on values. The standard
21example is the type of lists of a given length\footnote{Typically, and perhaps
22confusingly, referred to in the dependently typed programming literature as
23``vectors''}, \texttt{Vect a n}, where \texttt{a} is the element type and
24\texttt{n} is the length of the list and can be an arbitrary
25term.
27When types can contain values, and where those values describe properties (e.g.
28the length of a list)
29functions over those types begin to describe their own properties. For example,
30concatenating two lists has the property that the resulting list's length is
31the sum of the lengths of the two input lists. We can therefore give the following type
32to the \texttt{app} function, which concatenates vectors:
34\begin{SaveVerbatim}{appendv}
36app : Vect a n -> Vect a m -> Vect a (n + m);
38\end{SaveVerbatim}
39\useverb{appendv}
42This tutorial introduces \Idris{}, a general purpose dependently typed functional
43programming language.
44The goal of the \Idris{} project is to build a dependently typed language suitable
45for verifable \emph{systems} programming. To this end, \Idris{} is a compiled language
46which aims to generate efficient executable code. It also has a lightweight foreign
47function interface which allows easy interaction with external C libraries.
49\subsection{Intended Audience}
51This tutorial is intended as a brief introduction to the language, and is aimed
52at readers already familiar with a functional language such as Haskell or
53OCaml. In particular, a certain amount of familiarity with Haskell syntax is
54assumed, although most concepts will at least be explained briefly. The reader
55is also assumed to have some interest in using dependent types for writing and
56verifying systems software.