@@ -69,15 +69,236 @@ Boolean expressions can be tested with the \texttt{if...then...else} construct:
6969
7070\subsection{Data Types}
7171
72+Data types are declared in a similar way to Haskell data types, with a similar
73+syntax. The main difference is that Idris syntax is not whitespace sensitive,
74+and declarations must end with a semi-colon. Natural numbers and lists, for
75+example, can be declared as follows:
7276
77+\begin{SaveVerbatim}{natlist}
78+
79+data Nat = O | S Nat; -- Natural numbers
80+ -- (zero and successor)
81+data List a = Nil | (::) a (List a); -- Polymorphic lists
82+
83+\end{SaveVerbatim}
84+\useverb{natlist}
85+
86+The above declarations are taken from the standard library. Unary natural
87+numbers can be either zero (\texttt{O} - that's a capital letter 'o', not the digit), or
88+the successor of another natural number (\texttt{S k}).
89+Lists can either be empty (\texttt{Nil})
90+or a value added to the front of another list (\texttt{x :: xs}).
91+In the declaration for \tTC{List}, we used an infix operator \tDC{::}. New operators
92+such as this can be added using a fixity declaration, as follows:
93+
94+\begin{SaveVerbatim}{infixcons}
95+
96+infixr 7 :: ;
97+
98+\end{SaveVerbatim}
99+\useverb{infixcons}
100+
101+Functions, data constructors and type constuctors may all be given infix
102+operators as names. They may be used in prefix form if enclosed in brackets,
103+e.g. (::). Infix operators can use any of the symbols:
104+
105+\begin{SaveVerbatim}{infixsyms}
106+
107+:+-*/=_.?|&><!@$%^~.
108+
109+\end{SaveVerbatim}
110+\useverb{infixsyms}
111+
112+\subsection{Functions}
113+
114+Functions are implemented by pattern matching, again using a similar syntax to
115+Haskell. The main difference is that \Idris{} requires type declarations for all
116+functions, using a single colon \texttt{:} (rather than
117+Haskell's double colon \texttt{::}). Some natural number arithmetic functions can be
118+defined as follows, again taken from the standard library:
119+
120+\begin{SaveVerbatim}{natfns}
121+
122+-- Unary addition
123+plus : Nat -> Nat -> Nat;
124+plus O y = y;
125+plus (S k) y = S (plus k y);
126+
127+-- Unary multiplication
128+mult : Nat -> Nat -> Nat;
129+mult O y = O;
130+mult (S k) y = plus y (mult k y);
131+
132+\end{SaveVerbatim}
133+\useverb{natfns}
134+
135+The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded for
136+use by \texttt{Nat}, and are implemented using the above functions.
137+Unlike Haskell, there is no restriction on whether types and function names
138+must begin with a capital letter or not. Function names (\tFN{plus} and \tFN{mult} above),
139+data constructors (\tDC{O}, \tDC{S}, \tDC{Nil} and \tDC{::}) and type
140+constructors (\tTC{Nat} and \tTC{List}) are
141+all part of the same namespace.
142+
143+We can test these functions at the Idris prompt:
144+
145+\begin{SaveVerbatim}{fntest}
146+
147+Idris> plus (S (S O)) (S (S O))
148+S (S (S (S O))) : Nat
149+Idris> mult (S (S (S O))) (plus (S (S O)) (S (S O)))
150+S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat
151+
152+\end{SaveVerbatim}
153+\useverb{fntest}
154+
155+Like arithmetic operations, integer literals are also overloaded using type classes,
156+meaning that we can also test the functions as follows:
157+
158+\begin{SaveVerbatim}{fntest}
159+
160+Idris> plus 2 2
161+S (S (S (S O))) : Nat
162+Idris> mult 3 (plus 2 2)
163+S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat
164+
165+\end{SaveVerbatim}
166+\useverb{fntest}
167+
168+You may wonder, by the way, why we have unary natural numbers when our
169+computers have perfectly good integer arithmetic built in. The reason is
170+primarily that unary numbers have a very convenient structure which is easy to
171+reason about, and easy to relate to other data structures as we will see later.
172+Nevertheless, we do not want this convenience to be at the expense of
173+efficiency. Fortunately, \Idris{} knows about the relationship between
174+\tTC{Nat} (and similarly structured types) and numbers, so optimises the
175+representation and functions such as \tFN{plus} and \tFN{mult}.
73176
74177\subsection{Dependent Types}
75178
76179\subsubsection{Vectors}
77180
181+A standard example of a dependent type is the type of ``lists with length'',
182+conventionally called vectors in the dependent type literature. In \Idris{},
183+we declare vectors as follows:
184+
185+\begin{SaveVerbatim}{vect}
186+
187+data Vect : Set -> Nat -> Set where
188+ Nil : Vect a O
189+ | (::) : a -> Vect a k -> Vect a (S k);
190+
191+\end{SaveVerbatim}
192+\useverb{vect}
193+
194+Note that we have used the same constructor names as for \tTC{List}. Ad-hoc
195+name overloading such as this is accepted by \Idris{}, provided that the names
196+are declared in different namespaces (in practice, normally in different modules).
197+Ambiguous constructor names can normally be resolved from context.
198+
199+This declares a family of types, and so the form of the declaration is rather
200+different from the simple type declarations above. We explicitly state the type
201+of the type constructor \tTC{Vect} - it takes a type and a \tTC{Nat} as an
202+argument, where \tTC{Set} stands for the type of types. We say that \tTC{Vect}
203+is \emph{parameterised} by a type, and \emph{indexed} over \tTC{Nat}. Each
204+constructor targets a different part of the family of types. \tDC{Nil} can only
205+be used to construct vectors with zero length, and \tDC{::} to constructor
206+vectors with non-zero length.
207+
208+We can define functions on dependent types such as \tTC{Vect} in the same way
209+as on simple types such as \tTC{List} and \tTC{Nat} above, by pattern matching.
210+The type of a function over \tTC{Vect} will describe what happens to the
211+lengths of the vectors involved. For example, \tFN{app}, defined in the
212+library, appends two \tTC{Vect}s:
213+
214+\begin{SaveVerbatim}{vapp}
215+
216+app : Vect A n -> Vect A m -> Vect A (n + m);
217+app Nil ys = ys;
218+app (x :: xs) ys = x :: app xs ys;
219+
220+\end{SaveVerbatim}
221+\useverb{vapp}
222+
223+The type of \tFN{app} states that the resulting vector's length will be the sum of
224+the input lengths. If we get the definition wrong in such a way that this does
225+not hold, \Idris{} will not accept the definition. For example:
226+
227+\begin{SaveVerbatim}{vapperr}
228+
229+app : Vect a n -> Vect a m -> Vect a (n + m);
230+app Nil ys = ys;
231+app (x :: xs) ys = x :: app xs xs; -- BROKEN
232+
233+\end{SaveVerbatim}
234+\useverb{vapperr}
235+
236+\begin{SaveVerbatim}{vapperrmsg}
237+
238+$ idris app.idr --check
239+app.idr:3:Can't unify Vect a m with Vect a (plus n m)
240+
241+\end{SaveVerbatim}
242+\useverb{vapperrmsg}
243+%$
244+
245+This error message suggests that there is a length mismatch between two vectors.
246+Note that the terms in the error message have been \emph{normalised}, so in
247+particular \texttt{n + m} has been reduced to \texttt{plus n m}.
248+
78249\subsubsection{The Finite Sets}
79250
251+Finite sets, as the name suggests, are sets with a finite number of elements.
252+They are declared as follows (again, in the prelude):
253+
254+\begin{SaveVerbatim}{findecl}
255+
256+data Fin : Nat -> Set where
257+ fO : Fin (S k)
258+ | fS : Fin k -> Fin (S k);
259+
260+\end{SaveVerbatim}
261+\useverb{findecl}
262+
263+\tDC{fO} is the zeroth element of a finite set with \texttt{S k} elements;
264+\texttt{fS n} is the
265+\texttt{n+1}th element of a finite set with \texttt{S k} elements.
266+\tTC{Fin} is indexed by a \tTC{Nat}, which
267+represents the number of elements in the set. Obviously we can't construct an
268+element of an empty set, so neither constructor targets \texttt{Fin O}.
269+
270+A useful application of the \tTC{Fin} family is to represent numbers with
271+guaranteed bounds. For example, the following function which looks up an element in a \tTC{Vect}
272+is defined in the prelude:
273+
274+\begin{SaveVerbatim}{vlookup}
275+
276+lookup : Fin n -> Vect a n -> a;
277+lookup fO (x :: xs) = x;
278+lookup (fS k) (x :: xs) = lookup k xs;
279+
280+\end{SaveVerbatim}
281+\useverb{vlookup}
282+
283+This function looks up a value at a given location in a vector. The location is
284+bounded by the length of the vector (\texttt{n} in each case), so there is no
285+need for a run-time bounds check. The type checker guarantees that the location
286+is no larger than the length of the vector.
287+
288+Note also that there is no case for \texttt{Nil} here. This is because it is
289+impossible. Since there is no element of \texttt{Fin O}, and the location is a
290+\texttt{Fin n}, then \texttt{n} can not be \tDC{O}. As a result, attempting to
291+look up an element in an empty vector would give a compile time type error,
292+since it would force \texttt{n} to be \tDC{O}.
293+
80294\subsubsection{Implicit Arguments}
81295
82−\subsection{Modules and Namespaces}
296+\subsection{Useful Data Types}
297+
298+Lists, syntactic sugar.
299+Maybe, Either.
300+Pairs, dependent pairs, syntactic sugar.
83301
302+\subsection{I/O}
303+
304+\subsection{Modules and Namespaces}