git.iko.soy/Idris-dev
on bc0ebee help sign in
Idris-dev/tutorial/views.tex
117 lines 3.8 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{SaveVerbatim}{appdep}
12(++) : Vect n a -> Vect m a -> Vect (n + m) a
13(++) {n=Z} [] ys = ys
14(++) {n=S k} (x :: xs) ys = x :: xs ++ ys
16\end{SaveVerbatim}
17\useverb{appdep}
19\noindent
20If \texttt{n} was a successor in the \texttt{[]} case, or zero in the
21\texttt{::} case, the definition
22would not be well typed.
24\subsection{The \texttt{with} rule --- matching intermediate values}
26Very often, we need to match on the result of an intermediate computation.
27\Idris{} provides a construct for this, the \texttt{with} rule,
28inspired by views in \Epigram~\cite{view-left},
29which takes account of the
30fact that matching on a value in a dependently typed language can affect what
31we know about the forms of other values. In its simplest form, the \texttt{with} rule
32adds another argument to the function being defined, e.g. we have already seen
33a vector filter function, defined as follows:
35\begin{SaveVerbatim}{vfilterdef}
37filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
38filter p [] = ( _ ** [] )
39filter p (x :: xs) with (filter p xs)
40 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
42\end{SaveVerbatim}
43\useverb{vfilterdef}
45\noindent
46Here, the \texttt{with} clause allows us to deconstruct the result of
47\texttt{filter p xs}.
48Effectively, it adds this value as an extra argument, which we place after the
49vertical bar.
51If the intermediate computation itself has a dependent type, then the result
52can affect the forms of other arguments --- we can learn the form of one value by
53testing another. For example, a \texttt{Nat} is either even or odd. If it's even it will
54be the sum of two equal \texttt{Nat}s. Otherwise, it is the sum of two equal \texttt{Nat}s
55plus one:
57\begin{SaveVerbatim}{parity}
59data Parity : Nat -> Type where
60 even : Parity (n + n)
61 odd : Parity (S (n + n))
63\end{SaveVerbatim}
64\useverb{parity}
66\noindent
67We say \texttt{Parity} is a \emph{view} of \texttt{Nat}.
68It has a \emph{covering function} which tests whether
69it is even or odd and constructs the predicate accordingly.
71\begin{SaveVerbatim}{parityty}
73parity : (n:Nat) -> Parity n
75\end{SaveVerbatim}
76\useverb{parityty}
78\noindent
79We'll come back to the definition of \texttt{parity} shortly. We can use it
80to write a function which converts a natural number to a list of binary digits
81(least significant first) as follows, using the \texttt{with} rule:
83\begin{SaveVerbatim}{natToBin}
85natToBin : Nat -> List Bool
86natToBin Z = Nil
87natToBin k with (parity k)
88 natToBin (j + j) | even = False :: natToBin j
89 natToBin (S (j + j)) | odd = True :: natToBin j
91\end{SaveVerbatim}
92\useverb{natToBin}
94\noindent
95The value of the result of \texttt{parity k} affects the form of \texttt{k},
96because the result
97of \texttt{parity k} depends on \texttt{k}.
98So, as well as the patterns for the result of the
99intermediate computation (\texttt{even} and \texttt{odd}) right of the
100\texttt{$\mid$}, we also write how
101the results affect the other patterns left of the $\mid$. Note that there is a
102function in the patterns (\texttt{+}) and repeated occurrences of \texttt{j} ---
103this is allowed
104because another argument has determined the form of these patterns.
106We can test this function at the prompt. 42 is 101010 in binary. The binary digits
107are reversed with natToBin:
109\begin{SaveVerbatim}{ntbtest}
111*views> show (natToBin 42)
112"[False, True, False, True, False, True]" : String
114\end{SaveVerbatim}
115\useverb{ntbtest}