git.iko.soy/Idris-dev
on master help sign in
Document auto implicits
34331d9Edwin Brady
tutorial/idris-tutorial.tex+1−1
compare with master
unifiedsplit
@@ -17,7 +17,7 @@
17
17
18\maketitle
18\maketitle
19
19
20−%\tableofcontents
20+\tableofcontents
21
21
22\input{intro}
22\input{intro}
23\input{starting}
23\input{starting}
tutorial/intro.tex+2−1
@@ -61,7 +61,8 @@ verifying systems software.
61
61
62\subsection{Example Code}
62\subsection{Example Code}
63
63
64+This tutorial includes some example code, which has been tested with \Idris{} version
64−This tutorial includes some example code. The files are available in the \Idris{} distribution,
65+0.9.1. The files are available in the \Idris{} distribution,
65so that you can try them out easily,
66so that you can try them out easily,
66under \texttt{tutorial/examples}. However, it is strongly recommended that you
67under \texttt{tutorial/examples}. However, it is strongly recommended that you
67type them in yourself, rather than simply loading and reading them.
68type them in yourself, rather than simply loading and reading them.
tutorial/miscellany.tex+69−1
@@ -1,11 +1,79 @@
1\section{Miscellany}
1\section{Miscellany}
2
2
3In this section we discuss a variety of additional features: extensible syntax,
3In this section we discuss a variety of additional features: extensible syntax,
4+auto implicit and default
4−literate programming, interfacing with external libraries through the
5+arguments, literate programming, interfacing with external libraries through the
5foriegn function interface, and the universe hierarchy.
6foriegn function interface, and the universe hierarchy.
6
7
7\input{syntax}
8\input{syntax}
8
9
10+\subsection{Auto implicit arguments}
11+
12+We have already seen implicit arguments, which allows arguments to be omitted when
13+they can be inferred by the type checker, e.g.
14+
15+\useverb{vlookupimpty}
16+
17+\noindent
18+In other situations, it may be possible to infer arguments not by type checking but
19+by searching the context for an appropriate value, or constructing a proof. For example,
20+the following definition of \texttt{head} which requires a proof that the list is
21+non-empty
22+
23+\begin{SaveVerbatim}{safehead}
24+
25+isCons : List a -> Bool
26+isCons [] = False
27+isCons (x :: xs) = True
28+
29+head : (xs : List a) -> (isCons xs = True) -> a
30+head (x :: xs) _ = x
31+
32+\end{SaveVerbatim}
33+\useverb{safehead}
34+
35+\noindent
36+If the list is statically known to be non-empty, either because its value is known or
37+because a proof already exists in the context, the proof can be constructed
38+automatically. Auto implicit arguments allow this to happen silently. We define
39+\texttt{head} as follows:
40+
41+\begin{SaveVerbatim}{headauto}
42+
43+head : (xs : List a) -> {auto p : isCons xs = True} -> a
44+head (x :: xs) = x
45+
46+\end{SaveVerbatim}
47+\useverb{headauto}
48+
49+\noindent
50+The \texttt{auto} annotation on the implicit argument means that \Idris{} will
51+attempt to fill in the implicit argument using the \texttt{trivial} tactic, which
52+searches through the context for a proof, and tries to solve with \texttt{refl}
53+if a proof is not found.
54+Now when \texttt{head} is applied, the proof can be omitted. In the case that a proof
55+is not found, it can be provided explicitly as normal:
56+
57+\begin{SaveVerbatim}{headapp}
58+
59+head xs {p = ?headProof}
60+
61+\end{SaveVerbatim}
62+\useverb{headapp}
63+
64+\noindent
65+More generally, we can fill in implicit arguments with a default value by annotating
66+them with \texttt{default}. The definition above is equivalent to:
67+
68+\begin{SaveVerbatim}{defimp}
69+
70+head : (xs : List a) ->
71+ {default proof { trivial; } p : isCons xs = True} -> a
72+head (x :: xs) = x
73+
74+\end{SaveVerbatim}
75+\useverb{defimp}
76+
9\subsection{Literate programming}
77\subsection{Literate programming}
10
78
11Like Haskell, \Idris{} supports \emph{literate} programming. If a file has an
79Like Haskell, \Idris{} supports \emph{literate} programming. If a file has an