@@ -388,3 +388,87 @@ m_add' x y = [| x + y |]
388388\end{SaveVerbatim}
389389\useverb{maddc}
390390
391+\subsubsection{An error-handling interpreter}
392+
393+Idiom notation is commonly useful when defining evaluators. McBride and
394+Paterson describe such an evaluator~\cite{idioms}, for a language similar to
395+the following:
396+
397+\begin{SaveVerbatim}{idiomexpr}
398+
399+data Expr = Var String -- variables
400+ | Val Int -- values
401+ | Add Expr Expr -- addition
402+
403+\end{SaveVerbatim}
404+\useverb{idiomexpr}
405+
406+\noindent
407+Evaluation will take place relative to a context mapping variables (represented as
408+\texttt{String}s) to integer values, and can possibly fail. We define a data type
409+\texttt{Eval} to wrap an evaluator:
410+
411+\begin{SaveVerbatim}{evalctxt}
412+
413+data Eval : Set -> Set where
414+ MkEval : (List (String, Int) -> Maybe a) -> Eval a
415+
416+\end{SaveVerbatim}
417+\useverb{evalctxt}
418+
419+\noindent
420+Wrapping the evaluator in a data type means we will be able to make it an instance
421+of a type class later. We begin by defining a function to retrieve values from
422+the context during evaluation:
423+
424+\begin{SaveVerbatim}{fetch}
425+
426+fetch : String -> Eval Int
427+fetch x = MkEval (\e => fetchVal e) where
428+ fetchVal : List (String, Int) -> Maybe Int
429+ fetchVal [] = Nothing
430+ fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)
431+
432+\end{SaveVerbatim}
433+\useverb{fetch}
434+
435+\noindent
436+When defining an evaluator for the language, we will be applying functions in the
437+context of an \texttt{Eval}, so it is natural to make \texttt{Eval} an instance
438+of \texttt{Applicative}:
439+
440+\begin{SaveVerbatim}{}
441+
442+instance Applicative Eval where
443+ pure x = MkEval (\e => Just x)
444+
445+ (<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
446+ app : Maybe (a -> b) -> Maybe a -> Maybe b
447+ app (Just fx) (Just gx) = Just (fx gx)
448+ app _ _ = Nothing
449+
450+\end{SaveVerbatim}
451+\useverb{}
452+
453+\begin{SaveVerbatim}{grr}
454+<$>
455+\end{SaveVerbatim}
456+
457+\noindent
458+Evaluating an expression can now make use of the idiomatic application to handle
459+errors:
460+
461+\begin{SaveVerbatim}{evalexpr}
462+
463+eval : Expr -> Eval Int
464+eval (Var x) = fetch x
465+eval (Val x) = [| x |]
466+eval (Add x y) = [| eval x + eval y |]
467+
468+runEval : List (String, Int) -> Expr -> Maybe Int
469+runEval env e = case eval e of
470+ MkEval envFn => envFn env
471+
472+\end{SaveVerbatim}
473+\useverb{evalexpr}
474+