@@ -33,24 +33,36 @@ rule, inspired by views in ``Epigram`` [1]_, which takes account of
33the fact that matching on a value in a dependently typed language can
33the fact that matching on a value in a dependently typed language can
34affect what we know about the forms of other values. In its simplest
34affect what we know about the forms of other values. In its simplest
35form, the ``with`` rule adds another argument to the function being
35form, the ``with`` rule adds another argument to the function being
36−defined, e.g. we have already seen a vector filter function, defined
38+We have already seen a vector filter function. This time, we define it
37−as follows:
39+using ``with`` as follows:
39.. code-block:: idris
41.. code-block:: idris
41 filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
43 filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
42 filter p [] = ( _ ** [] )
44 filter p [] = ( _ ** [] )
43 filter p (x :: xs) with (filter p xs)
45 filter p (x :: xs) with (filter p xs)
44− | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
46+ filter p (x :: xs) | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
46Here, the ``with`` clause allows us to deconstruct the result of
48Here, the ``with`` clause allows us to deconstruct the result of
47−``filter p xs``. Effectively, it adds this value as an extra argument,
49+``filter p xs``. The view refined argument pattern ``filter p (x ::
48−which we place after the vertical bar.
50+xs)`` goes beneath the ``with`` clause, followed by a vertical bar
51+``|``, followed by the deconstructed intermediate result ``( _ ** xs'
52+)``. If the view refined argument pattern is unchanged from the
53+original function argument pattern, then the left side of ``|`` is
54+extraneous and may be omitted:
58+ filter p (x :: xs) with (filter p xs)
59+ | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
50If the intermediate computation itself has a dependent type, then the
61If the intermediate computation itself has a dependent type, then the
51result can affect the forms of other arguments — we can learn the form
62result can affect the forms of other arguments — we can learn the form
63+of one value by testing another. In these cases, view refined argument
52−of one value by testing another. For example, a ``Nat`` is either even
64+patterns must be explicit. For example, a ``Nat`` is either even or
53−or odd. If it’s even it will be the sum of two equal ``Nat``.
65+odd. If it is even it will be the sum of two equal ``Nat``.
54Otherwise, it is the sum of two equal ``Nat`` plus one:
66Otherwise, it is the sum of two equal ``Nat`` plus one:
56.. code-block:: idris
68.. code-block:: idris
@@ -80,14 +92,29 @@ rule:
80 natToBin (j + j) | Even = False :: natToBin j
92 natToBin (j + j) | Even = False :: natToBin j
81 natToBin (S (j + j)) | Odd = True :: natToBin j
93 natToBin (S (j + j)) | Odd = True :: natToBin j
83−The value of the result of ``parity k`` affects the form of ``k``,
95+The value of ``parity k`` affects the form of ``k``, because the
84−because the result of ``parity k`` depends on ``k``. So, as well as
96+result of ``parity k`` depends on ``k``. So, as well as the patterns
85−the patterns for the result of the intermediate computation (``Even``
97+for the result of the intermediate computation (``Even`` and ``Odd``)
86−and ``odd``) right of the ``|``, we also write how the results
98+right of the ``|``, we also write how the results affect the other
87−affect the other patterns left of the ``|``. Note that there is
99+patterns left of the ``|``. That is:
101+- When ``parity k`` evaluates to ``Even``, we can refine the original
102+ argument ``k`` to a refined pattern ``(j + j)`` according to
103+ ``Parity (n + n)`` from the ``Even`` constructor definition. So
104+ ``(j + j)`` replaces ``k`` on the left side of ``|``, and the
105+ ``Even`` constructor appears on the right side. The natural number
106+ ``j`` in the refined pattern can be used on the ride side of the
109+- Otherwise, when ``parity k`` evaluates to ``Odd``, the original
110+ argument ``k`` is refined to ``S (j + j)`` according to ``Parity (S
111+ (n + n))`` from the ``Odd`` constructor definition, and ``Odd`` now
112+ appears on the ride side of ``|``, again with the natural number
113+ ``j`` used on the ride side of the ``=`` sign.
88−a function in the patterns (``+``) and repeated occurrences of
115+Note that there is a function in the patterns (``+``) and repeated
89−``j``—this is allowed because another argument has determined the form
116+occurrences of ``j`` - this is allowed because another argument has
90−of these patterns.
117+determined the form of these patterns.
92We will return to this function in the next section :ref:`sect-parity` to
119We will return to this function in the next section :ref:`sect-parity` to
93complete the definition of ``parity``.
120complete the definition of ``parity``.