git.iko.soy/Idris-dev
on master help sign in
Document comprehensions
commit37bb964187cc01adb6ae910ba25db40c225b9e2f authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 6 Jan 2012, 16:17 (15 years ago) parent817c1a0
3 files changed+89
compare with master
unifiedsplit
tutorial/classes.tex+53 tutorial/idris-tutorial.pdf tutorial/typesfuns.tex+36
tutorial/classes.tex+53
@@ -190,6 +190,8 @@ sortAndShow xs = show (sort xs);
190190
191191\subsection{Monads and \texttt{do}-notation}
192192
193+\label{sec:monad}
194+
193195So far, we have seen single parameter type classes, where the parameter is of type
194196\texttt{Set}. In general, there can be any number (greater than 0) of parameters,
195197and the parameters can have \remph{any} type.
@@ -263,3 +265,54 @@ Nothing : Maybe Int
263265
264266\end{SaveVerbatim}
265267\useverb{maybeaddt}
268+
269+\subsubsection*{Monad comprehensions}
270+
271+The list comprehension notation we saw in Section \ref{sec:listcomp} is more
272+general, and applies to anything which is an instance of \texttt{MonadPlus}:
273+
274+\begin{SaveVerbatim}{monadplus}
275+
276+class Monad m => MonadPlus (m : Set -> Set) where {
277+ mplus : m a -> m a -> m a;
278+ mzero : m a;
279+}
280+
281+\end{SaveVerbatim}
282+\useverb{monadplus}
283+
284+\noindent
285+In general, a comprehension takes the form \texttt{[ exp | qual ]} where
286+\texttt{qual} can be one of:
287+
288+\begin{itemize}
289+\item A generator \texttt{x <- e}
290+\item A \emph{guard}, which is an expression of type \texttt{Bool}
291+\item A let binding \texttt{let x = e}
292+\end{itemize}
293+
294+\noindent
295+To translate a comprehension \texttt{[exp | qual1, qual2, ..., qualn]}, first
296+any qualifier
297+\texttt{qual} which is a \emph{guard} is translated to \texttt{guard qual}, using
298+the following function:
299+
300+\begin{SaveVerbatim}{guardq}
301+
302+guard : MonadPlus m => Bool -> m ()
303+
304+\end{SaveVerbatim}
305+\useverb{guardq}
306+
307+\noindent
308+Then the comprehension is converted to \texttt{do} notation:
309+
310+\begin{SaveVerbatim}{comptrans}
311+
312+do { qual1; qual2; ...; qualn; return exp; }
313+
314+\end{SaveVerbatim}
315+\useverb{comptrans}
316+
317+
318+
tutorial/idris-tutorial.pdf

Binary file not shown.

tutorial/typesfuns.tex+36
@@ -869,6 +869,42 @@ showPerson p = let MkPerson name age = p in
869869\end{SaveVerbatim}
870870\useverb{letp}
871871
872+\subsubsection*{List comprehensions}
873+
874+\label{sec:listcomp}
875+
876+\Idris{} provides \emph{comprehension} notation as a convenient shorthand for
877+building lists. The general form is:
878+
879+\begin{SaveVerbatim}{listcomp}
880+
881+[ expression | qualifiers ]
882+
883+\end{SaveVerbatim}
884+\useverb{listcomp}
885+
886+\noindent
887+This generates the list of values produced by evaluating the
888+\texttt{expression}, according to the conditions given by the comma separated
889+\texttt{qualifiers}. For example, we can build a list of Pythagorean triples as
890+follows:
891+
892+\begin{SaveVerbatim}{triples}
893+
894+pythag : Int -> List (Int, Int, Int);
895+pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
896+ x*x + y*y == z*z ];
897+
898+\end{SaveVerbatim}
899+\useverb{triples}
900+
901+\noindent
902+The \texttt{[a..b]} notation is another shorthand which builds a list of
903+numbers between \texttt{a} and \texttt{b}. Alternatively \texttt{[a,b..c]}
904+builds a list of numbers between \texttt{a} and \texttt{c} with the increment
905+specified by the difference between \texttt{a} and \texttt{c}. This works for
906+any numeric type, using the \texttt{count} function from the prelude.
907+
872908\subsubsection*{\texttt{case} expressions}
873909
874910Another way of inspecting intermediate values of \emph{simple} types