\section{Views and the ``\texttt{with}'' rule}
\subsection{Dependent pattern matching}
Since types can depend on values, the form of some arguments can be determined
by the value of others. For example, if we were to write down the implicit
length arguments to \texttt{(++)}, we'd see that the form of the length argument was
determined by whether the vector was empty or not:
\begin{SaveVerbatim}{appdep}
(++) : Vect a n -> Vect a m -> Vect a (n + m)
(++) {n=O} [] [] = []
(++) {n=S k} (x :: xs) ys = x :: xs ++ ys
\end{SaveVerbatim}
\useverb{appdep}
\noindent
If \texttt{n} was a successor in the \texttt{[]} case, or zero in the
\texttt{::} case, the definition
would not be well typed.
\subsection{The \texttt{with} rule --- matching intermediate values}
Very often, we need to match on the result of an intermediate computation.
\Idris{} provides a construct for this, the \texttt{with} rule,
inspired by views in \Epigram~\cite{view-left},
which takes account of the
fact that matching on a value in a dependently typed language can affect what
we know about the forms of other values. In its simplest form, the \texttt{with} rule
adds another argument to the function being defined, e.g. we have already seen
a vector filter function, defined as follows:
\begin{SaveVerbatim}{vfilterdef}
filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)
filter p [] = ( _ ** [] )
filter p (x :: xs) with (filter p xs)
| ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
\end{SaveVerbatim}
\useverb{vfilterdef}
\noindent
Here, the \texttt{with} clause allows us to deconstruct the result of
\texttt{filter p xs}.
Effectively, it adds this value as an extra argument, which we place after the
vertical bar.
If the intermediate computation itself has a dependent type, then the result
can affect the forms of other arguments --- we can learn the form of one value by
testing another. For example, a \texttt{Nat} is either even or odd. If it's even it will
be the sum of two equal \texttt{Nat}s. Otherwise, it is the sum of two equal \texttt{Nat}s
plus one:
\begin{SaveVerbatim}{parity}
data Parity : Nat -> Set where
even : Parity (n + n)
odd : Parity (S (n + n))
\end{SaveVerbatim}
\useverb{parity}
\noindent
We say \texttt{Parity} is a \emph{view} of \texttt{Nat}.
It has a \emph{covering function} which tests whether
it is even or odd and constructs the predicate accordingly.
\begin{SaveVerbatim}{parityty}
parity : (n:Nat) -> Parity n
\end{SaveVerbatim}
\useverb{parityty}
\noindent
We'll come back to the definition of \texttt{parity} shortly. We can use it
to write a function which converts a natural number to a list of binary digits
(least significant first) as follows, using the \texttt{with} rule:
\begin{SaveVerbatim}{natToBin}
natToBin : Nat -> List Bool
natToBin O = Nil
natToBin k with (parity k)
natToBin (j + j) | even = False :: natToBin j
natToBin (S (j + j)) | odd = True :: natToBin j
\end{SaveVerbatim}
\useverb{natToBin}
\noindent
The value of the result of \texttt{parity k} affects the form of \texttt{k},
because the result
of \texttt{parity k} depends on \texttt{k}.
So, as well as the patterns for the result of the
intermediate computation (\texttt{even} and \texttt{odd}) right of the
\texttt{$\mid$}, we also write how
the results affect the other patterns left of the $\mid$. Note that there is a
function in the patterns (\texttt{+}) and repeated occurrences of \texttt{j} ---
this is allowed
because another argument has determined the form of these patterns.
We can test this function at the prompt. 42 is 101010 in binary. The binary digits
are reversed with natToBin:
\begin{SaveVerbatim}{ntbtest}
*views> show (natToBin 42)
"[False, True, False, True, False, True]" : String
\end{SaveVerbatim}
\useverb{ntbtest}