@@ -69,15 +69,236 @@ Boolean expressions can be tested with the \texttt{if...then...else} construct:
70\subsection{Data Types}
70\subsection{Data Types}
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:
77+\begin{SaveVerbatim}{natlist}
79+data Nat = O | S Nat; -- Natural numbers
80+ -- (zero and successor)
81+data List a = Nil | (::) a (List a); -- Polymorphic lists
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:
94+\begin{SaveVerbatim}{infixcons}
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:
105+\begin{SaveVerbatim}{infixsyms}
112+\subsection{Functions}
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:
120+\begin{SaveVerbatim}{natfns}
123+plus : Nat -> Nat -> Nat;
125+plus (S k) y = S (plus k y);
127+-- Unary multiplication
128+mult : Nat -> Nat -> Nat;
130+mult (S k) y = plus y (mult k y);
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.
143+We can test these functions at the Idris prompt:
145+\begin{SaveVerbatim}{fntest}
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
155+Like arithmetic operations, integer literals are also overloaded using type classes,
156+meaning that we can also test the functions as follows:
158+\begin{SaveVerbatim}{fntest}
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
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}.
74\subsection{Dependent Types}
177\subsection{Dependent Types}
76\subsubsection{Vectors}
179\subsubsection{Vectors}
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:
185+\begin{SaveVerbatim}{vect}
187+data Vect : Set -> Nat -> Set where
189+ | (::) : a -> Vect a k -> Vect a (S k);
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.
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.
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:
214+\begin{SaveVerbatim}{vapp}
216+app : Vect A n -> Vect A m -> Vect A (n + m);
218+app (x :: xs) ys = x :: app xs ys;
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:
227+\begin{SaveVerbatim}{vapperr}
229+app : Vect a n -> Vect a m -> Vect a (n + m);
231+app (x :: xs) ys = x :: app xs xs; -- BROKEN
236+\begin{SaveVerbatim}{vapperrmsg}
238+$ idris app.idr --check
239+app.idr:3:Can't unify Vect a m with Vect a (plus n m)
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}.
78\subsubsection{The Finite Sets}
249\subsubsection{The Finite Sets}
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):
254+\begin{SaveVerbatim}{findecl}
256+data Fin : Nat -> Set where
258+ | fS : Fin k -> Fin (S k);
263+\tDC{fO} is the zeroth element of a finite set with \texttt{S k} elements;
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}.
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:
274+\begin{SaveVerbatim}{vlookup}
276+lookup : Fin n -> Vect a n -> a;
277+lookup fO (x :: xs) = x;
278+lookup (fS k) (x :: xs) = lookup k xs;
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.
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}.
80\subsubsection{Implicit Arguments}
294\subsubsection{Implicit Arguments}
82−\subsection{Modules and Namespaces}
296+\subsection{Useful Data Types}
298+Lists, syntactic sugar.
300+Pairs, dependent pairs, syntactic sugar.
304+\subsection{Modules and Namespaces}