git.iko.soy/Idris-dev
on d1663cc help sign in
Idris-dev/tutorial/content/intro.tex
65 lines 2.9 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}
19\noindent
20In a language with \emph{dependent types}, however, the distinction is less
21clear.
22Dependent types allow types to ``depend'' on values --- in other words,
23types are a \emph{first class} language construct and can be manipulated like
24any other value. The standard
25example is the type of lists of a given length\footnote{Typically, and perhaps
26confusingly, referred to in the dependently typed programming literature as
27``vectors''}, \texttt{Vect n a}, where \texttt{a} is the element type and
28\texttt{n} is the length of the list and can be an arbitrary
29term.
31When types can contain values, and where those values describe properties (e.g.
32the length of a list)
33the type of a function can begin to describe its own properties. For example,
34concatenating two lists has the property that the resulting list's length is
35the sum of the lengths of the two input lists. We can therefore give the following type
36to the \texttt{app} function, which concatenates vectors:
38\begin{lstlisting}
39app : Vect n a -> Vect m a -> Vect (n + m) a
40\end{lstlisting}
42\noindent
43This tutorial introduces \Idris{}, a general purpose functional
44programming language with dependent types.
45The goal of the \Idris{} project is to build a dependently typed language suitable
46for verifiable \emph{systems} programming. To this end, \Idris{} is a compiled language
47which aims to generate efficient executable code. It also has a lightweight foreign
48function interface which allows easy interaction with external C libraries.
50\subsection{Intended Audience}
52This tutorial is intended as a brief introduction to the language, and is aimed
53at readers already familiar with a functional language such as Haskell or
54OCaml. In particular, a certain amount of familiarity with Haskell syntax is
55assumed, although most concepts will at least be explained briefly. The reader
56is also assumed to have some interest in using dependent types for writing and
57verifying systems software.
59\subsection{Example Code}
61This tutorial includes some example code, which has been tested with \Idris{} version
62\version{}. The files are available in the \Idris{} distribution,
63so that you can try them out easily,
64under \texttt{tutorial/examples}. However, it is strongly recommended that you
65type them in yourself, rather than simply loading and reading them.