.. _sec-views: *****************************Views and the “``with``” rule***************************** [NOT UPDATED FOR IDRIS 2 YET] Dependent pattern matching========================== Since types can depend on values, the form of some arguments can bedetermined by the value of others. For example, if we were to writedown the implicit length arguments to ``(++)``, we’d see that the formof the length argument was determined by whether the vector was emptyor not: .. code-block:: idris     (++) : Vect n a -> Vect m a -> Vect (n + m) a    (++) {n=Z}   []        ys = ys    (++) {n=S k} (x :: xs) ys = x :: xs ++ ys If ``n`` was a successor in the ``[]`` case, or zero in the ``::``case, the definition would not be well typed. .. _sect-nattobin: The ``with`` rule — matching intermediate values================================================ Very often, we need to match on the result of an intermediatecomputation. Idris provides a construct for this, the ``with``rule, inspired by views in ``Epigram`` [#McBridgeMcKinna]_, which takes account ofthe fact that matching on a value in a dependently typed language canaffect what we know about the forms of other values. In its simplestform, the ``with`` rule adds another argument to the function beingdefined. We have already seen a vector filter function. This time, we define itusing ``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)      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``. 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 theoriginal function argument pattern, then the left side of ``|`` isextraneous and may be omitted: .. code-block:: idris     filter p (x :: xs) with (filter p xs)      | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' ) ``with`` clauses can also be nested: .. code-block:: idris     foo : Int -> Int -> Bool    foo n m with (n + 1)      foo _ m | 2 with (m + 1)        foo _ _ | 2 | 3 = True        foo _ _ | 2 | _ = False      foo _ _ | _ = False If the intermediate computation itself has a dependent type, then theresult can affect the forms of other arguments — we can learn the formof one value by testing another. In these cases, view refined argumentpatterns must be explicit. For example, a ``Nat`` is either even orodd. 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     data Parity : Nat -> Type where       Even : {n : _} -> Parity (n + n)       Odd  : {n : _} -> Parity (S (n + n)) We say ``Parity`` is a *view* of ``Nat``. It has a *covering function*which tests whether it is even or odd and constructs the predicateaccordingly. Note that we're going to need access to ``n`` at run time, soalthough it's an implicit argument, it has unrestricted multiplicity. .. code-block:: idris     parity : (n:Nat) -> Parity n We’ll come back to the definition of ``parity`` shortly. We can use itto write a function which converts a natural number to a list ofbinary digits (least significant first) as follows, using the ``with``rule: .. code-block:: idris     natToBin : Nat -> List Bool    natToBin Z = Nil    natToBin k with (parity k)       natToBin (j + j)     | Even = False :: natToBin j       natToBin (S (j + j)) | Odd  = True  :: natToBin j The value of ``parity k`` affects the form of ``k``, because theresult of ``parity k`` depends on ``k``. So, as well as the patternsfor the result of the intermediate computation (``Even`` and ``Odd``)right of the ``|``, we also write how the results affect the otherpatterns 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 right 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 right side of ``|``, again with the natural number  ``j`` used on the right side of the ``=`` sign. Note that there is a function in the patterns (``+``) and repeatedoccurrences of ``j`` - this is allowed because another argument hasdetermined the form of these patterns. Defining ``parity``=================== The definition of ``parity`` is a little tricky, and requires some knowledge oftheorem proving (see Section :ref:`sect-theorems`), but for completeness, hereit is: .. code-block:: idris     parity : (n : Nat) -> Parity n    parity Z = Even {n = Z}    parity (S Z) = Odd {n = Z}    parity (S (S k)) with (parity k)      parity (S (S (j + j))) | Even          = rewrite plusSuccRightSucc j j in Even {n = S j}      parity (S (S (S (j + j)))) | Odd          = rewrite plusSuccRightSucc j j in Odd {n = S j} For full details on ``rewrite`` in particular, please refer to the theoremproving tutorial, in Section :ref:`proofs-index`. .. [#McBridgeMcKinna] Conor McBride and James McKinna. 2004. The view from the       left. J. Funct. Program. 14, 1 (January 2004),       69-111. https://doi.org/10.1017/S0956796803004829