git.iko.soy/Idris-dev
on d689c19 help sign in
Idris-dev/docs/tutorial/views.rst
156 lines 5.9 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' )
61``with`` clauses can also be nested:
63.. code-block:: idris
65 foo : Int -> Int -> Bool
66 foo n m with (succ n)
67 foo _ m | 2 with (succ m)
68 foo _ _ | 2 | 3 = True
69 foo _ _ | 2 | _ = False
70 foo _ _ | _ = False
72If the intermediate computation itself has a dependent type, then the
73result can affect the forms of other arguments — we can learn the form
74of one value by testing another. In these cases, view refined argument
75patterns must be explicit. For example, a ``Nat`` is either even or
76odd. If it is even it will be the sum of two equal ``Nat``.
77Otherwise, it is the sum of two equal ``Nat`` plus one:
79.. code-block:: idris
81 data Parity : Nat -> Type where
82 Even : Parity (n + n)
83 Odd : Parity (S (n + n))
85We say ``Parity`` is a *view* of ``Nat``. It has a *covering function*
86which tests whether it is even or odd and constructs the predicate
87accordingly.
89.. code-block:: idris
91 parity : (n:Nat) -> Parity n
93We’ll come back to the definition of ``parity`` shortly. We can use it
94to write a function which converts a natural number to a list of
95binary digits (least significant first) as follows, using the ``with``
96rule:
98.. code-block:: idris
100 natToBin : Nat -> List Bool
101 natToBin Z = Nil
102 natToBin k with (parity k)
103 natToBin (j + j) | Even = False :: natToBin j
104 natToBin (S (j + j)) | Odd = True :: natToBin j
106The value of ``parity k`` affects the form of ``k``, because the
107result of ``parity k`` depends on ``k``. So, as well as the patterns
108for the result of the intermediate computation (``Even`` and ``Odd``)
109right of the ``|``, we also write how the results affect the other
110patterns left of the ``|``. That is:
112- When ``parity k`` evaluates to ``Even``, we can refine the original
113 argument ``k`` to a refined pattern ``(j + j)`` according to
114 ``Parity (n + n)`` from the ``Even`` constructor definition. So
115 ``(j + j)`` replaces ``k`` on the left side of ``|``, and the
116 ``Even`` constructor appears on the right side. The natural number
117 ``j`` in the refined pattern can be used on the right side of the
118 ``=`` sign.
120- Otherwise, when ``parity k`` evaluates to ``Odd``, the original
121 argument ``k`` is refined to ``S (j + j)`` according to ``Parity (S
122 (n + n))`` from the ``Odd`` constructor definition, and ``Odd`` now
123 appears on the right side of ``|``, again with the natural number
124 ``j`` used on the right side of the ``=`` sign.
126Note that there is a function in the patterns (``+``) and repeated
127occurrences of ``j`` - this is allowed because another argument has
128determined the form of these patterns.
130We will return to this function in the next section :ref:`sect-parity` to
131complete the definition of ``parity``.
133With and proofs
134===============
135To use a dependent pattern match for theorem proving, it is sometimes necessary
136to explicitly construct the proof resulting from the pattern match.
137To do this, you can postfix the with clause with ``proof p`` and the proof
138generated by the pattern match will be in scope and named ``p``. For example:
140.. code-block:: idris
142 data Foo = FInt Int | FBool Bool
144 optional : Foo -> Maybe Int
145 optional (FInt x) = Just x
146 optional (FBool b) = Nothing
148 isFInt : (foo:Foo) -> Maybe (x : Int ** (optional foo = Just x))
149 isFInt foo with (optional foo) proof p
150 isFInt foo | Nothing = Nothing -- here, p : Nothing = optional foo
151 isFInt foo | (Just x) = Just (x ** Refl) -- here, p : Just x = optional foo
154.. [1] Conor McBride and James McKinna. 2004. The view from the
155 left. J. Funct. Program. 14, 1 (January 2004),
156 69-111. https://doi.org/10.1017/S0956796803004829