git.iko.soy/Idris-dev
on master help sign in
Document comprehensions
37bb964Edwin Brady
tutorial/classes.tex+53
compare with master
unifiedsplit
@@ -190,6 +190,8 @@ sortAndShow xs = show (sort xs);
190
190
191\subsection{Monads and \texttt{do}-notation}
191\subsection{Monads and \texttt{do}-notation}
192
192
193+\label{sec:monad}
194+
193So far, we have seen single parameter type classes, where the parameter is of type
195So far, we have seen single parameter type classes, where the parameter is of type
194\texttt{Set}. In general, there can be any number (greater than 0) of parameters,
196\texttt{Set}. In general, there can be any number (greater than 0) of parameters,
195and the parameters can have \remph{any} type.
197and the parameters can have \remph{any} type.
@@ -263,3 +265,54 @@ Nothing : Maybe Int
263
265
264\end{SaveVerbatim}
266\end{SaveVerbatim}
265\useverb{maybeaddt}
267\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
869\end{SaveVerbatim}
869\end{SaveVerbatim}
870\useverb{letp}
870\useverb{letp}
871
871
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+
872\subsubsection*{\texttt{case} expressions}
908\subsubsection*{\texttt{case} expressions}
873
909
874Another way of inspecting intermediate values of \emph{simple} types
910Another way of inspecting intermediate values of \emph{simple} types