@@ -55,7 +55,7 @@ True : Bool
5555\useverb{promptprim}
5656
5757All of the usual arithmetic and comparison operators are defined for the primitive
58−types. They are overloaded using type classes, as we will discuss in section
58+types. They are overloaded using type classes, as we will discuss in Section
5959\ref{sec:classes} and can be extended to work on user defined types.
6060Boolean expressions can be tested with the \texttt{if...then...else} construct:
6161
@@ -132,12 +132,12 @@ mult (S k) y = plus y (mult k y);
132132\end{SaveVerbatim}
133133\useverb{natfns}
134134
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
135+The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded
136+for use by \texttt{Nat}, and are implemented
137+using the above functions. Unlike Haskell, there is no restriction on whether
138+types and function names must begin with a capital letter or not. Function
139+names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{O}, \tDC{S},
140+\tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are
141141all part of the same namespace.
142142
143143We can test these functions at the Idris prompt:
@@ -295,25 +295,217 @@ impossible. Since there is no element of \texttt{Fin O}, and the location is a
295295look up an element in an empty vector would give a compile time type error,
296296since it would force \texttt{n} to be \tDC{O}.
297297
298−\subsubsection{Dependent Function Types}
298+\subsubsection{Implicit Arguments}
299299
300−The function types we have seen so far have taken the form \texttt{a -> b},
301−where \texttt{a} stands for the input type and \texttt{b} stands for the output
302−type. More generally, function types take the following form:
300+Let us take a closer look at the type of \texttt{lookup}:
303301
304−\begin{SaveVerbatim}{ftype}
302+\begin{SaveVerbatim}{vlookupty}
305303
306−(x : a) -> b
304+lookup : Fin n -> Vect a n -> a
307305
308306\end{SaveVerbatim}
309−\useverb{ftype}
307+\useverb{vlookupty}
310308
311309\noindent
312−\ldots where the name \texttt{x} may appear in \texttt{b}. This is a \remph{dependent}
313−function type --- the output type depends on the value of \texttt{x}.
310+It takes two arguments, an element of the finite set of \texttt{n} elements, and a vector
311+with \texttt{n} elements of type \texttt{a}. But there are also two names,
312+\texttt{n} and \texttt{a}, which are not declared explictly. These are \emph{implicit}
313+arguments to \texttt{lookup}. We could also write the type of \texttt{lookup} as:
314314
315+\begin{SaveVerbatim}{vlookupimpty}
315316
316−\subsubsection{Implicit Arguments}
317+lookup : {a:Set} -> {n:Nat} -> Fin n -> Vect a n -> a
318+
319+\end{SaveVerbatim}
320+\useverb{vlookupimpty}
321+
322+Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are not given in
323+applications of \texttt{lookup}; their values can be inferred from the types of
324+the \texttt{Fin n} and \texttt{Vect a n} arguments. Any name which appears as a parameter
325+or index in a type declaration, but which is otherwise free, will be automatically
326+bound as an implicit argument.
327+Implicit arguments can still be given explicitly in applications, using
328+{a=value} and {n=value}, for example:
329+
330+\begin{SaveVerbatim}{vlookupexp}
331+
332+lookup {a=Int} {n=2} fO (2 :: 3 :: VNil)
333+
334+\end{SaveVerbatim}
335+\useverb{vlookupexp}
336+
337+\noindent
338+In fact, any argument, implicit or explicit, may be given a name. We could have
339+declared the type of \texttt{lookup} as:
340+
341+\begin{SaveVerbatim}{vlookupn}
342+
343+lookup : (i:Fin n) -> (xs:Vect a n) -> a;
344+
345+\end{SaveVerbatim}
346+\useverb{vlookupn}
347+
348+\noindent
349+It is a matter of taste whether you want to do this --- sometimes it can help
350+document a function by making the purpose of an argument more clear.
351+
352+\subsubsection{``\texttt{using}'' notation}
353+
354+Sometimes it is necessary to provide types of implicit arguments where
355+the type checker can not work them out itself. This can happen if there is a
356+dependency ordering --- obviously, \texttt{a} and \texttt{n} must be given as arguments above
357+before being used --- or if an implicit argument has a complex type. For example,
358+we will need to state the types of the implicit arguments in the following
359+definition, which defines a predicate on vectors:
360+
361+\begin{SaveVerbatim}{elem}
362+
363+data Elem : a -> (Vect a n) -> Set where
364+ here : {x:a} -> {xs:Vect a n} -> Elem x (x :: xs)
365+ | there : {x,y:a} -> {xs:Vect a n} -> Elem x xs -> Elem x (y :: xs);
366+
367+\end{SaveVerbatim}
368+\useverb{elem}
369+
370+\noindent
371+An instance of \texttt{Elem x xs} states that \texttt{x} is an element of
372+\texttt{xs}. We can construct
373+such a predicate if the required element is \texttt{here}, at the head of the vector,
374+or \texttt{there}, in the tail of the vector. For example:
375+
376+\begin{SaveVerbatim}{testelem}
377+
378+testVec : Vect Int 4;
379+testVec = 3 :: 4 :: 5 :: 6 :: VNil;
380+
381+inVect : Elem 5 testVec;
382+inVect = there (there here);
383+
384+\end{SaveVerbatim}
385+\useverb{testelem}
386+
387+\noindent
388+If the same implicit arguments are being used a lot, it can make a definition
389+difficult to read. To avoid this problem, a \texttt{using} block gives the types and
390+ordering of any implicit arguments which can appear within the block:
391+
392+\begin{SaveVerbatim}{elemusing}
393+
394+using (x:a, y:a, xs:Vect a n) {
395+ data Elem : a -> (Vect a n) -> Set where
396+ here : Elem x (x :: xs)
397+ | there : Elem x xs -> Elem x (y :: xs);
398+}
399+
400+\end{SaveVerbatim}
401+\useverb{elemusing}
402+
403+\subsection{I/O}
404+
405+Computer programs are of little use if they do not interact with the user or
406+the system in some way. The difficulty in a pure language such as \Idris{} ---
407+that is, a language where expressions do not have side-effects --- is that I/O
408+is inherently side-effecting. Therefore in \Idris{}, such interactions are
409+encapsulated in the type \texttt{IO}:
410+
411+\begin{SaveVerbatim}{ioty}
412+
413+data IO a; -- IO operation returning a value of type a
414+
415+\end{SaveVerbatim}
416+\useverb{ioty}
417+
418+We'll leave the definition of \texttt{IO} abstract, but effectively it describes what
419+the I/O operations to be executed are, rather than how to execute them. The
420+resulting operations are executed externally,
421+by the run-time system. We've already seen one IO
422+program:
423+
424+\begin{SaveVerbatim}{main}
425+
426+main : IO ();
427+main = putStrLn "Hello world";
428+
429+\end{SaveVerbatim}
430+\useverb{main}
431+
432+The type of \texttt{putStrLn} explains that it takes a string, and returns an
433+element of the unit type () via an I/O action. There is a variant \texttt{putStr} which
434+outputs a string without a newline:
435+
436+\begin{SaveVerbatim}{putstr}
437+
438+putStrLn : String -> IO ();
439+putStr : String -> IO ();
440+
441+\end{SaveVerbatim}
442+
443+We can also read strings from user input:
444+
445+\begin{SaveVerbatim}{getline}
446+
447+getLine : IO String;
448+
449+\end{SaveVerbatim}
450+\useverb{getline}
451+
452+\noindent
453+A number of other I/O operations are defined in the prelude, for example for reading and
454+writing files, including:
455+
456+\begin{SaveVerbatim}{fileops}
457+
458+data File; -- abstract
459+data Mode = Read | Write | ReadWrite;
460+
461+openFile : String -> Mode -> IO File;
462+closeFile : File -> IO ();
463+
464+fread : File -> IO String;
465+fwrite : File -> String -> IO ();
466+feof : File -> IO Bool;
467+
468+readFile : String -> IO String;
469+
470+\end{SaveVerbatim}
471+\useverb{fileops}
472+
473+\subsection{``\texttt{do}'' notation}
474+
475+I/O programs will typically need to sequence actions, feeding the output of one
476+computation into the input of the next. \texttt{IO} is an abstract type, however, so we
477+can't access the result of a computation directly. Instead, we sequence
478+operations with \texttt{do} notation:
479+
480+\begin{SaveVerbatim}{greet}
481+
482+greet : IO ();
483+greet = do { putStr "What is your name? ";
484+ name <- getLine;
485+ putStrLn ("Hello " ++ name);
486+ };
487+
488+\end{SaveVerbatim}
489+\useverb{greet}
490+
491+The syntax \texttt{x <- iovalue} executes the I/O operation iovalue, of type
492+\texttt{IO a}, and
493+puts the result, of type \texttt{a} into the variabel \texttt{x}.
494+In this case, \texttt{getLine} returns an \texttt{IO String},
495+so \texttt{name} has type \texttt{String}.
496+The \texttt{return} operation allows us to inject a value directly into an IO
497+operation:
498+
499+\begin{SaveVerbatim}{return}
500+
501+return : a -> IO a;
502+
503+\end{SaveVerbatim}
504+\useverb{return}
505+
506+\noindent
507+As we will see later, \texttt{do} notation is more general than this, and can be
508+overloaded.
317509
318510\subsection{Useful Data Types}
319511
@@ -321,6 +513,4 @@ Lists, syntactic sugar.
321513Maybe, Either.
322514Pairs, dependent pairs, syntactic sugar.
323515
324−\subsection{I/O}
325516
326−\subsection{Modules and Namespaces}