git.iko.soy/Idris-dev
on fdbcc73 help sign in
Idris-dev/docs/tutorial/views.rst
146 lines 5.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
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.
38We have already seen a vector filter function. This time, we define it
39using ``with`` as follows:
41.. code-block:: idris
43 filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
44 filter p [] = ( _ ** [] )
45 filter p (x :: xs) with (filter p xs)
46 filter p (x :: xs) | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
48Here, the ``with`` clause allows us to deconstruct the result of
49``filter p xs``. The view refined argument pattern ``filter p (x ::
50xs)`` 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
53original function argument pattern, then the left side of ``|`` is
54extraneous and may be omitted:
56.. code-block:: idris
58 filter p (x :: xs) with (filter p xs)
59 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
61If the intermediate computation itself has a dependent type, then the
62result can affect the forms of other arguments — we can learn the form
63of one value by testing another. In these cases, view refined argument
64patterns must be explicit. For example, a ``Nat`` is either even or
65odd. If it is even it will be the sum of two equal ``Nat``.
66Otherwise, it is the sum of two equal ``Nat`` plus one:
68.. code-block:: idris
70 data Parity : Nat -> Type where
71 Even : Parity (n + n)
72 Odd : Parity (S (n + n))
74We say ``Parity`` is a *view* of ``Nat``. It has a *covering function*
75which tests whether it is even or odd and constructs the predicate
76accordingly.
78.. code-block:: idris
80 parity : (n:Nat) -> Parity n
82We’ll come back to the definition of ``parity`` shortly. We can use it
83to write a function which converts a natural number to a list of
84binary digits (least significant first) as follows, using the ``with``
85rule:
87.. code-block:: idris
89 natToBin : Nat -> List Bool
90 natToBin Z = Nil
91 natToBin k with (parity k)
92 natToBin (j + j) | Even = False :: natToBin j
93 natToBin (S (j + j)) | Odd = True :: natToBin j
95The value of ``parity k`` affects the form of ``k``, because the
96result of ``parity k`` depends on ``k``. So, as well as the patterns
97for the result of the intermediate computation (``Even`` and ``Odd``)
98right of the ``|``, we also write how the results affect the other
99patterns 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
107 ``=`` sign.
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.
115Note that there is a function in the patterns (``+``) and repeated
116occurrences of ``j`` - this is allowed because another argument has
117determined the form of these patterns.
119We will return to this function in the next section :ref:`sect-parity` to
120complete the definition of ``parity``.
122With and proofs
123===============
124To use a dependent pattern match for theorem proving, it is sometimes necessary
125to explicitly construct the proof resulting from the pattern match.
126To do this, you can postfix the with clause with ``proof p`` and the proof
127generated by the pattern match will be in scope and named ``p``. For example:
129.. code-block:: idris
131 data Foo = FInt Int | FBool Bool
133 optional : Foo -> Maybe Int
134 optional (FInt x) = Just x
135 optional (FBool b) = Nothing
137 isFInt : (foo:Foo) -> Maybe (x : Int ** (optional foo = Just x))
138 isFInt foo with (optional foo) proof p
139 isFInt foo | Nothing = Nothing -- here, p : Nothing = optional foo
140 isFInt foo | (Just x) = Just (x ** Refl) -- here, p : Just x = optional foo
143.. [1] Conor McBride and James McKinna. 2004. The view from the
144 left. J. Funct. Program. 14, 1 (January 2004),
145 69-111. DOI=10.1017/S0956796803004829
146 http://dx.doi.org/10.1017/S0956796803004829ñ