@@ -1,11 +1,79 @@
11\section{Miscellany}
22
33In this section we discuss a variety of additional features: extensible syntax,
4−literate programming, interfacing with external libraries through the
4+auto implicit and default
5+arguments, literate programming, interfacing with external libraries through the
56foriegn function interface, and the universe hierarchy.
67
78\input{syntax}
89
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+
977\subsection{Literate programming}
1078
1179Like Haskell, \Idris{} supports \emph{literate} programming. If a file has an