From 07ee064a9af5845a3db85beb6289e8dd5a07e23c Mon Sep 17 00:00:00 2001 From: Rob Stewart Date: Mon, 13 Nov 2017 21:37:29 +0000 Subject: [PATCH] Expands on documentation of the 'with' rule (#4195) * Expands on documentation of the 'with' rule This additional text clarifies the syntax of the 'with' rule: - it gives the name "view refined argument pattern" to argument patterns to the left of the | vertical bar. - it explains that when the original function argument patterns are unchanged, then the refined pattern may be omitted, using the 'filter' function as an example. - it decomposes in a bit more detail the body of the 'natToBin' function, explaining in bullet point form where the refined patterns have come from, i.e. Even and Odd constructor definitions. --- docs/tutorial/views.rst | 57 ++++++++++++++++++++++++++++++----------- 1 file changed, 42 insertions(+), 15 deletions(-) diff --git a/docs/tutorial/views.rst b/docs/tutorial/views.rst index 0e1bcf0d7..a305a228e 100644 --- a/docs/tutorial/views.rst +++ b/docs/tutorial/views.rst @@ -33,24 +33,36 @@ rule, inspired by views in ``Epigram`` [1]_, which takes account of the fact that matching on a value in a dependently typed language can affect what we know about the forms of other values. In its simplest form, the ``with`` rule adds another argument to the function being -defined, e.g. we have already seen a vector filter function, defined -as follows: +defined. + +We have already seen a vector filter function. This time, we define it +using ``with`` as follows: .. code-block:: idris filter : (a -> Bool) -> Vect n a -> (p ** Vect p a) filter p [] = ( _ ** [] ) filter p (x :: xs) with (filter p xs) - | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' ) + filter p (x :: xs) | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' ) Here, the ``with`` clause allows us to deconstruct the result of -``filter p xs``. Effectively, it adds this value as an extra argument, -which we place after the vertical bar. +``filter p xs``. The view refined argument pattern ``filter p (x :: +xs)`` goes beneath the ``with`` clause, followed by a vertical bar +``|``, followed by the deconstructed intermediate result ``( _ ** xs' +)``. If the view refined argument pattern is unchanged from the +original function argument pattern, then the left side of ``|`` is +extraneous and may be omitted: + +.. code-block:: idris + + filter p (x :: xs) with (filter p xs) + | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' ) If the intermediate computation itself has a dependent type, then the result can affect the forms of other arguments — we can learn the form -of one value by testing another. For example, a ``Nat`` is either even -or odd. If it’s even it will be the sum of two equal ``Nat``. +of one value by testing another. In these cases, view refined argument +patterns must be explicit. For example, a ``Nat`` is either even or +odd. If it is even it will be the sum of two equal ``Nat``. Otherwise, it is the sum of two equal ``Nat`` plus one: .. code-block:: idris @@ -80,14 +92,29 @@ rule: natToBin (j + j) | Even = False :: natToBin j natToBin (S (j + j)) | Odd = True :: natToBin j -The value of the result of ``parity k`` affects the form of ``k``, -because the result of ``parity k`` depends on ``k``. So, as well as -the patterns for the result of the intermediate computation (``Even`` -and ``odd``) right of the ``|``, we also write how the results -affect the other patterns left of the ``|``. Note that there is -a function in the patterns (``+``) and repeated occurrences of -``j``—this is allowed because another argument has determined the form -of these patterns. +The value of ``parity k`` affects the form of ``k``, because the +result of ``parity k`` depends on ``k``. So, as well as the patterns +for the result of the intermediate computation (``Even`` and ``Odd``) +right of the ``|``, we also write how the results affect the other +patterns left of the ``|``. That is: + +- When ``parity k`` evaluates to ``Even``, we can refine the original + argument ``k`` to a refined pattern ``(j + j)`` according to + ``Parity (n + n)`` from the ``Even`` constructor definition. So + ``(j + j)`` replaces ``k`` on the left side of ``|``, and the + ``Even`` constructor appears on the right side. The natural number + ``j`` in the refined pattern can be used on the ride side of the + ``=`` sign. + +- Otherwise, when ``parity k`` evaluates to ``Odd``, the original + argument ``k`` is refined to ``S (j + j)`` according to ``Parity (S + (n + n))`` from the ``Odd`` constructor definition, and ``Odd`` now + appears on the ride side of ``|``, again with the natural number + ``j`` used on the ride side of the ``=`` sign. + +Note that there is a function in the patterns (``+``) and repeated +occurrences of ``j`` - this is allowed because another argument has +determined the form of these patterns. We will return to this function in the next section :ref:`sect-parity` to complete the definition of ``parity``.