@@ -31,6 +31,8 @@ twoPlusTwo = refl
3131
3232\subsection{The Empty Type}
3333
34+\label{sect:empty}
35+
3436There is an empty type, \texttt{\_|\_}, which has no constructors. It is
3537therefore impossible to construct an element of the empty type, at least
3638without using a partially defined or general recursive function (see Section
@@ -40,12 +42,12 @@ to a successor:
4042
4143\begin{SaveVerbatim}{natdisjoint}
4244
43−imp : (n : Nat) -> O = S n -> _|_
44−imp n p = replace {P = impTy} p ()
45+disjoint : (n : Nat) -> O = S n -> _|_
46+disjoint n p = replace {P = disjointTy} p ()
4547 where
46− impTy : Nat -> Set
47− impTy O = ()
48− impTy (S k) = _|_
48+ disjointTy : Nat -> Set
49+ disjointTy O = ()
50+ disjointTy (S k) = _|_
4951
5052\end{SaveVerbatim}
5153\useverb{natdisjoint}
@@ -57,6 +59,16 @@ transform a predicate. Here we use it to transform a value of a type which can e
5759the empty tuple, to a value of a type which can't, by using a proof of something
5860which can't exist.
5961
62+Once we have an element of the empty type, we can prove anything. \texttt{FalseElim}
63+is defined in the library, to assist with proofs by contradiction.
64+
65+\begin{SaveVerbatim}{falseelim}
66+
67+FalseElim : _|_ -> a
68+
69+\end{SaveVerbatim}
70+\useverb{falseelim}
71+
6072\subsection{Simple Theorems}
6173
6274When type checking dependent types, the type itself gets \emph{normalised}. So imagine
@@ -321,3 +333,85 @@ plusredO_S = proof {
321333\noindent
322334Again, we can add this proof to the end of our source file using the \texttt{:addproof}
323335command at the interactive prompt.
336+
337+\subsection{Totality Checking}
338+
339+\label{sect:totality}
340+
341+If we really want to trust our proofs, it is important that they are defined by
342+\emph{total} functions --- that is, a function which is defined for all possible inputs
343+and is guaranteed to terminate. Otherwise we could construct an element of the empty type,
344+from which we could prove anything:
345+
346+\begin{SaveVerbatim}{empties}
347+
348+-- making use of 'head' being partially defined
349+empty1 : _|_
350+empty1 = hd [] where
351+ hd : List a -> a
352+ hd (x :: xs) = x
353+
354+-- not terminating
355+empty2 : _|_
356+empty2 = empty2
357+
358+\end{SaveVerbatim}
359+\useverb{empties}
360+
361+\noindent
362+Internally, \Idris{} checks every definition for totality, and we can check at the prompt
363+with the \texttt{:total} command. We see that neither of the above definitions is total:
364+
365+\begin{SaveVerbatim}{totalcheck}
366+
367+*theorems> :total empty1
368+possibly not total due to: empty1#hd
369+ not total as there are missing cases
370+*theorems> :total empty2
371+possibly not total as it is not well founded
372+
373+\end{SaveVerbatim}
374+\useverb{totalcheck}
375+
376+\noindent
377+Note the use of the word ``possibly'' --- a totality check can, of course, never be certain
378+due to the undecidability of the halting problem. The check is, therefore, conservative.
379+It is also possible (and indeed advisable, in the case of proofs) to mark functions as
380+total so that it will be a compile time error for the totality check to fail:
381+
382+\begin{SaveVerbatim}{emptyfail}
383+
384+total empty2 : _|_
385+empty2 = empty2
386+
387+Type checking ./theorems.idr
388+theorems.idr:25:empty2 is possibly not total as it is not well founded
389+
390+\end{SaveVerbatim}
391+\useverb{emptyfail}
392+
393+\noindent
394+Reassuringly, our proof in Section \ref{sect:empty} that the zero and successor constructors
395+are disjoint is total:
396+
397+\begin{SaveVerbatim}{totdisjoint}
398+
399+*theorems> :total disjoint
400+Total
401+
402+\end{SaveVerbatim}
403+\useverb{totdisjoint}
404+
405+\noindent
406+The totality check is currently very conservative. To be recorded as total, a function must:
407+
408+\begin{itemize}
409+\item Cover all possible inputs
410+\item Be \emph{well-founded} --- i.e. each recursive call must have a decreasing argument
411+\item Not call any non-total functions
412+\item Not use any data types which are not \emph{strictly positive}
413+\item (In version 0.9.1) Not be mutually recursive
414+\end{itemize}
415+
416+\noindent
417+The last of these conditions may be relaxed in the future.