git.iko.soy/Idris-dev
on master help sign in
Monad comprehension example
commitf7c50cfea13f47bcb8d52b555f20bdbec35f8f7a authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 6 Jan 2012, 16:38 (15 years ago) parent37bb964
4 files changed+17−3
compare with master
unifiedsplit
CHANGELOG+3−1 tutorial/classes.tex+11−2 tutorial/examples/classes.idr+3 tutorial/idris-tutorial.pdf
CHANGELOG+3−1
@@ -1,4 +1,4 @@
1−0.1.x to 0.9.0:
1+0.1.x to 0.9:
22
33Complete rewrite. User visible changes:
44
@@ -6,6 +6,8 @@ Complete rewrite. User visible changes:
66* New syntax for pairs/dependent pairs
77* Added type classes
88* Added where clauses
9+* Added case expressions, pattern matching let and lambda
10+* Added monad comprehensions
911* Added cumulativity and universe checking
1012* Ad-hoc name overloading
1113 - Resolved by type or explicit namespace
tutorial/classes.tex+11−2
@@ -282,8 +282,8 @@ class Monad m => MonadPlus (m : Set -> Set) where {
282282\useverb{monadplus}
283283
284284\noindent
285−In general, a comprehension takes the form \texttt{[ exp | qual ]} where
286−\texttt{qual} can be one of:
285+In general, a comprehension takes the form \texttt{[ exp | qual1, qual2, ..., qualn ]} where
286+\texttt{quali} can be one of:
287287
288288\begin{itemize}
289289\item A generator \texttt{x <- e}
@@ -314,5 +314,14 @@ do { qual1; qual2; ...; qualn; return exp; }
314314\end{SaveVerbatim}
315315\useverb{comptrans}
316316
317+\noindent
318+Using monad comprehensions, an alternative definition for \texttt{m\_add} would be:
319+
320+\begin{SaveVerbatim}{maddb}
321+
322+m_add : Maybe Int -> Maybe Int -> Maybe Int;
323+m_add x y = [ x' + y' | x' <- x, y' <- y ];
324+\end{SaveVerbatim}
325+\useverb{maddb}
317326
318327
tutorial/examples/classes.idr+3
@@ -4,5 +4,8 @@ m_add x y = do { x' <- x; -- Extract value from x
44 return (x' + y'); -- Add them
55 };
66
7+m_add' : Maybe Int -> Maybe Int -> Maybe Int;
8+m_add' x y = [ x' + y' | x' <- x, y' <- y ];
9+
710sortAndShow : (Ord a, Show a) => List a -> String;
811sortAndShow xs = show (sort xs);
tutorial/idris-tutorial.pdf

Binary file not shown.