git.iko.soy/Idris-dev
on cf47310 help sign in
Idris-dev/docs/tutorial/views.rst
98 lines 3.6 kB history raw
1.. _sec-views:
3*****************************
4Views and the “``with``” rule
5*****************************
7Dependent pattern matching
8==========================
10Since types can depend on values, the form of some arguments can be
11determined by the value of others. For example, if we were to write
12down the implicit length arguments to ``(++)``, we’d see that the form
13of the length argument was determined by whether the vector was empty
14or not:
16.. code-block:: idris
18 (++) : Vect n a -> Vect m a -> Vect (n + m) a
19 (++) {n=Z} [] ys = ys
20 (++) {n=S k} (x :: xs) ys = x :: xs ++ ys
22If ``n`` was a successor in the ``[]`` case, or zero in the ``::``
23case, the definition would not be well typed.
25.. _sect-nattobin:
27The ``with`` rule — matching intermediate values
28================================================
30Very often, we need to match on the result of an intermediate
31computation. Idris provides a construct for this, the ``with``
32rule, inspired by views in ``Epigram`` [1]_, which takes account of
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
35form, the ``with`` rule adds another argument to the function being
36defined, e.g. we have already seen a vector filter function, defined
37as follows:
39.. code-block:: idris
41 filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
42 filter p [] = ( _ ** [] )
43 filter p (x :: xs) with (filter p xs)
44 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
46Here, the ``with`` clause allows us to deconstruct the result of
47``filter p xs``. Effectively, it adds this value as an extra argument,
48which we place after the vertical bar.
50If the intermediate computation itself has a dependent type, then the
51result can affect the forms of other arguments — we can learn the form
52of one value by testing another. For example, a ``Nat`` is either even
53or odd. If it’s even it will be the sum of two equal ``Nat``.
54Otherwise, it is the sum of two equal ``Nat`` plus one:
56.. code-block:: idris
58 data Parity : Nat -> Type where
59 Even : Parity (n + n)
60 Odd : Parity (S (n + n))
62We say ``Parity`` is a *view* of ``Nat``. It has a *covering function*
63which tests whether it is even or odd and constructs the predicate
64accordingly.
66.. code-block:: idris
68 parity : (n:Nat) -> Parity n
70We’ll come back to the definition of ``parity`` shortly. We can use it
71to write a function which converts a natural number to a list of
72binary digits (least significant first) as follows, using the ``with``
73rule:
75.. code-block:: idris
77 natToBin : Nat -> List Bool
78 natToBin Z = Nil
79 natToBin k with (parity k)
80 natToBin (j + j) | Even = False :: natToBin j
81 natToBin (S (j + j)) | Odd = True :: natToBin j
83The value of the result of ``parity k`` affects the form of ``k``,
84because the result of ``parity k`` depends on ``k``. So, as well as
85the patterns for the result of the intermediate computation (``Even``
86and ``odd``) right of the ``|``, we also write how the results
87affect the other patterns left of the ``|``. Note that there is
88a function in the patterns (``+``) and repeated occurrences of
89``j``—this is allowed because another argument has determined the form
90of these patterns.
92We will return to this function in Section :ref:`sect-provisional` to
93complete the definition of ``parity``.
95.. [1] Conor McBride and James McKinna. 2004. The view from the
96 left. J. Funct. Program. 14, 1 (January 2004),
97 69-111. DOI=10.1017/S0956796803004829
98 http://dx.doi.org/10.1017/S0956796803004829ñ