git.iko.soy/Idris-dev
on f572cd0 help sign in
Idris-dev/docs/tutorial/views.rst
98 lines 3.7 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 down
12the implicit length arguments to ``(++)``, we’d see that the form of the
13length argument was determined by whether the vector was empty or not:
15.. code-block:: idris
17 (++) : Vect n a -> Vect m a -> Vect (n + m) a
18 (++) {n=Z} [] ys = ys
19 (++) {n=S k} (x :: xs) ys = x :: xs ++ ys
21If ``n`` was a successor in the ``[]`` case, or zero in the ``::`` case,
22the definition would not be well typed.
26.. _sect-nattobin:
28The ``with`` rule — matching intermediate values
29------------------------------------------------
31Very often, we need to match on the result of an intermediate
32computation. ``Idris`` provides a construct for this, the ``with`` rule,
33inspired by views in ``Epigram`` [1]_, which takes account of
34the fact that matching on a value in a dependently typed language can
35affect what we know about the forms of other values. In its simplest
36form, the ``with`` rule adds another argument to the function being
37defined, e.g. we have already seen a vector filter function, defined as
38follows:
40.. code-block:: idris
42 filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
43 filter p [] = ( _ ** [] )
44 filter p (x :: xs) with (filter p xs)
45 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
47Here, the ``with`` clause allows us to deconstruct the result of
48``filter p xs``. Effectively, it adds this value as an extra argument,
49which we place after the vertical bar.
51If the intermediate computation itself has a dependent type, then the
52result can affect the forms of other arguments — we can learn the form
53of one value by testing another. For example, a ``Nat`` is either even
54or odd. If it’s even it will be the sum of two equal ``Nat``\ s.
55Otherwise, it is the sum of two equal ``Nat``\ s plus one:
57.. code-block:: idris
59 data Parity : Nat -> Type where
60 Even : Parity (n + n)
61 Odd : Parity (S (n + n))
63We say ``Parity`` is a *view* of ``Nat``. It has a *covering function*
64which tests whether it is even or odd and constructs the predicate
65accordingly.
67.. code-block:: idris
69 parity : (n:Nat) -> Parity n
71We’ll come back to the definition of ``parity`` shortly. We can use it
72to write a function which converts a natural number to a list of binary
73digits (least significant first) as follows, using the ``with`` rule:
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 the
85patterns for the result of the intermediate computation (``Even`` and
86``odd``) right of the ``\mid``, we also write how the results affect the
87other patterns left of the :math:`\mid`. Note that there is a function
88in the patterns (``+``) and repeated occurrences of ``j``—this is
89allowed because another argument has determined the form of these
90patterns.
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ñ