@@ -246,6 +246,70 @@ are both available, or return ``Nothing`` if one or both are not ("fail fast").
246 *ifaces> m_add (Just 20) Nothing
246 *ifaces> m_add (Just 20) Nothing
247 Nothing : Maybe Int
247 Nothing : Maybe Int
249+Pattern Matching Bind
250+---------------------
252+Sometimes we want to pattern match immediately on the result of a function
253+in ``do`` notation. For example, let's say we have a function ``readNumber``
254+which reads a number from the console, returning a value of the form
255+``Just x`` if the number is valid, or ``Nothing`` otherwise:
257+.. code-block:: idris
259+ readNumber : IO (Maybe Nat)
262+ if all isDigit (unpack input)
263+ then pure (Just (cast input))
266+If we then use it to write a function to read two numbers, returning
267+``Nothing`` if neither are valid, then we would like to pattern match
268+on the result of ``readNumber``:
270+.. code-block:: idris
272+ readNumbers : IO (Maybe (Nat, Nat))
276+ Nothing => pure Nothing
277+ Just x_ok => do y <- readNumber
279+ Nothing => pure Nothing
280+ Just y_ok => pure (Just (x_ok, y_ok))
282+If there's a lot of error handling, this could get deeply nested very quickly!
283+So instead, we can combine the bind and the pattern match in one line. For example,
284+we could try pattern matching on values of the form ``Just x_ok``:
286+.. code-block:: idris
288+ readNumbers : IO (Maybe (Nat, Nat))
290+ do Just x_ok <- readNumber
291+ Just y_ok <- readNumber
292+ pure (Just (x_ok, y_ok))
294+There is still a problem, however, because we've now omitted the case for
295+``Nothing`` so ``readNumbers`` is no longer total! We can add the ``Nothing``
296+case back as follows:
298+.. code-block:: idris
300+ readNumbers : IO (Maybe (Nat, Nat))
302+ do Just x_ok <- readNumber | Nothing => pure Nothing
303+ Just y_ok <- readNumber | Nothing => pure Nothing
304+ pure (Just (x_ok, y_ok))
306+The effect of this version of ``readNumbers`` is identical to the first (in
307+fact, it is syntactic sugar for it and directly translated back into that form).
308+The first part of each statement (``Just x_ok <-`` and ``Just y_ok <-``) gives
309+the preferred binding - if this matches, execution will continue with the rest
310+of the ``do`` block. The second part gives the alternative bindings, of which
311+there may be more than one.
249``!``-notation
313``!``-notation
250--------------
314--------------