@@ -55,7 +55,7 @@ True : Bool
55\useverb{promptprim}
55\useverb{promptprim}
57All of the usual arithmetic and comparison operators are defined for the primitive
57All 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
59\ref{sec:classes} and can be extended to work on user defined types.
59\ref{sec:classes} and can be extended to work on user defined types.
60Boolean expressions can be tested with the \texttt{if...then...else} construct:
60Boolean expressions can be tested with the \texttt{if...then...else} construct:
@@ -132,12 +132,12 @@ mult (S k) y = plus y (mult k y);
132\end{SaveVerbatim}
132\end{SaveVerbatim}
133\useverb{natfns}
133\useverb{natfns}
135−The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded for
135+The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded
136−use by \texttt{Nat}, and are implemented using the above functions.
136+for use by \texttt{Nat}, and are implemented
137−Unlike Haskell, there is no restriction on whether types and function names
137+using the above functions. Unlike Haskell, there is no restriction on whether
138−must begin with a capital letter or not. Function names (\tFN{plus} and \tFN{mult} above),
138+types and function names must begin with a capital letter or not. Function
139−data constructors (\tDC{O}, \tDC{S}, \tDC{Nil} and \tDC{::}) and type
139+names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{O}, \tDC{S},
140−constructors (\tTC{Nat} and \tTC{List}) are
140+\tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are
141all part of the same namespace.
141all part of the same namespace.
143We can test these functions at the Idris prompt:
143We 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
295look up an element in an empty vector would give a compile time type error,
295look up an element in an empty vector would give a compile time type error,
296since it would force \texttt{n} to be \tDC{O}.
296since it would force \texttt{n} to be \tDC{O}.
298−\subsubsection{Dependent Function Types}
298+\subsubsection{Implicit Arguments}
300−The function types we have seen so far have taken the form \texttt{a -> b},
300+Let us take a closer look at the type of \texttt{lookup}:
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:
304−\begin{SaveVerbatim}{ftype}
302+\begin{SaveVerbatim}{vlookupty}
306−(x : a) -> b
304+lookup : Fin n -> Vect a n -> a
308\end{SaveVerbatim}
306\end{SaveVerbatim}
309−\useverb{ftype}
307+\useverb{vlookupty}
312−\ldots where the name \texttt{x} may appear in \texttt{b}. This is a \remph{dependent}
310+It takes two arguments, an element of the finite set of \texttt{n} elements, and a vector
313−function type --- the output type depends on the value of \texttt{x}.
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:
315+\begin{SaveVerbatim}{vlookupimpty}
317+lookup : {a:Set} -> {n:Nat} -> Fin n -> Vect a n -> a
320+\useverb{vlookupimpty}
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:
330+\begin{SaveVerbatim}{vlookupexp}
332+lookup {a=Int} {n=2} fO (2 :: 3 :: VNil)
338+In fact, any argument, implicit or explicit, may be given a name. We could have
339+declared the type of \texttt{lookup} as:
341+\begin{SaveVerbatim}{vlookupn}
343+lookup : (i:Fin n) -> (xs:Vect a n) -> a;
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.
316−\subsubsection{Implicit Arguments}
352+\subsubsection{``\texttt{using}'' notation}
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:
361+\begin{SaveVerbatim}{elem}
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);
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:
376+\begin{SaveVerbatim}{testelem}
378+testVec : Vect Int 4;
379+testVec = 3 :: 4 :: 5 :: 6 :: VNil;
381+inVect : Elem 5 testVec;
382+inVect = there (there here);
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:
392+\begin{SaveVerbatim}{elemusing}
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);
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}:
411+\begin{SaveVerbatim}{ioty}
413+data IO a; -- IO operation returning a value of type a
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
424+\begin{SaveVerbatim}{main}
427+main = putStrLn "Hello world";
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:
436+\begin{SaveVerbatim}{putstr}
438+putStrLn : String -> IO ();
439+putStr : String -> IO ();
443+We can also read strings from user input:
445+\begin{SaveVerbatim}{getline}
453+A number of other I/O operations are defined in the prelude, for example for reading and
454+writing files, including:
456+\begin{SaveVerbatim}{fileops}
458+data File; -- abstract
459+data Mode = Read | Write | ReadWrite;
461+openFile : String -> Mode -> IO File;
462+closeFile : File -> IO ();
464+fread : File -> IO String;
465+fwrite : File -> String -> IO ();
466+feof : File -> IO Bool;
468+readFile : String -> IO String;
473+\subsection{``\texttt{do}'' notation}
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:
480+\begin{SaveVerbatim}{greet}
483+greet = do { putStr "What is your name? ";
485+ putStrLn ("Hello " ++ name);
491+The syntax \texttt{x <- iovalue} executes the I/O operation iovalue, of type
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
499+\begin{SaveVerbatim}{return}
507+As we will see later, \texttt{do} notation is more general than this, and can be
318\subsection{Useful Data Types}
510\subsection{Useful Data Types}
@@ -321,6 +513,4 @@ Lists, syntactic sugar.
321Maybe, Either.
513Maybe, Either.
322Pairs, dependent pairs, syntactic sugar.
514Pairs, dependent pairs, syntactic sugar.
326−\subsection{Modules and Namespaces}