git.iko.soy/Idris-dev
on d1663cc help sign in
Idris-dev/tutorial/content/views.tex
96 lines 3.5 kB history raw
1\section{Views and the ``\texttt{with}'' rule}
3\subsection{Dependent pattern matching}
5Since types can depend on values, the form of some arguments can be determined
6by the value of others. For example, if we were to write down the implicit
7length arguments to \texttt{(++)}, we'd see that the form of the length argument was
8determined by whether the vector was empty or not:
10\begin{code}
11(++) : Vect n a -> Vect m a -> Vect (n + m) a
12(++) {n=Z} [] ys = ys
13(++) {n=S k} (x :: xs) ys = x :: xs ++ ys
14\end{code}
16\noindent
17If \texttt{n} was a successor in the \texttt{[]} case, or zero in the
18\texttt{::} case, the definition
19would not be well typed.
21\subsection{The \texttt{with} rule --- matching intermediate values}
23Very often, we need to match on the result of an intermediate computation.
24\Idris{} provides a construct for this, the \texttt{with} rule,
25inspired by views in \Epigram~\cite{view-left},
26which takes account of the
27fact that matching on a value in a dependently typed language can affect what
28we know about the forms of other values. In its simplest form, the \texttt{with} rule
29adds another argument to the function being defined, e.g. we have already seen
30a vector filter function, defined as follows:
32\begin{code}
33filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
34filter p [] = ( _ ** [] )
35filter p (x :: xs) with (filter p xs)
36 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
37\end{code}
39\noindent
40Here, the \texttt{with} clause allows us to deconstruct the result of
41\texttt{filter p xs}.
42Effectively, it adds this value as an extra argument, which we place after the
43vertical bar.
45If the intermediate computation itself has a dependent type, then the result
46can affect the forms of other arguments --- we can learn the form of one value by
47testing another. For example, a \texttt{Nat} is either even or odd. If it's even it will
48be the sum of two equal \texttt{Nat}s. Otherwise, it is the sum of two equal \texttt{Nat}s
49plus one:
51\begin{code}
52data Parity : Nat -> Type where
53 even : Parity (n + n)
54 odd : Parity (S (n + n))
55\end{code}
57\noindent
58We say \texttt{Parity} is a \emph{view} of \texttt{Nat}.
59It has a \emph{covering function} which tests whether
60it is even or odd and constructs the predicate accordingly.
62\begin{code}
63parity : (n:Nat) -> Parity n
64\end{code}
66\label{sect:nattobin}
68\noindent
69We'll come back to the definition of \texttt{parity} shortly. We can use it
70to write a function which converts a natural number to a list of binary digits
71(least significant first) as follows, using the \texttt{with} rule:
73\begin{code}
74natToBin : Nat -> List Bool
75natToBin Z = Nil
76natToBin k with (parity k)
77 natToBin (j + j) | even = False :: natToBin j
78 natToBin (S (j + j)) | odd = True :: natToBin j
79\end{code}
81\noindent
82The value of the result of \texttt{parity k} affects the form of \texttt{k},
83because the result
84of \texttt{parity k} depends on \texttt{k}.
85So, as well as the patterns for the result of the
86intermediate computation (\texttt{even} and \texttt{odd}) right of the
87\texttt{$\mid$}, we also write how
88the results affect the other patterns left of the $\mid$. Note that there is a
89function in the patterns (\texttt{+}) and repeated occurrences of \texttt{j} ---
90this is allowed
91because another argument has determined the form of these patterns.
93We will return to this function in Section \ref{sect:provisional} to complete
94the definition of \texttt{parity}.