@@ -388,3 +388,87 @@ m_add' x y = [| x + y |]
388\end{SaveVerbatim}
388\end{SaveVerbatim}
389\useverb{maddc}
389\useverb{maddc}
391+\subsubsection{An error-handling interpreter}
393+Idiom notation is commonly useful when defining evaluators. McBride and
394+Paterson describe such an evaluator~\cite{idioms}, for a language similar to
397+\begin{SaveVerbatim}{idiomexpr}
399+data Expr = Var String -- variables
401+ | Add Expr Expr -- addition
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:
411+\begin{SaveVerbatim}{evalctxt}
413+data Eval : Set -> Set where
414+ MkEval : (List (String, Int) -> Maybe a) -> Eval a
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:
424+\begin{SaveVerbatim}{fetch}
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)
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}:
440+\begin{SaveVerbatim}{}
442+instance Applicative Eval where
443+ pure x = MkEval (\e => Just x)
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)
453+\begin{SaveVerbatim}{grr}
458+Evaluating an expression can now make use of the idiomatic application to handle
461+\begin{SaveVerbatim}{evalexpr}
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 |]
468+runEval : List (String, Int) -> Expr -> Maybe Int
469+runEval env e = case eval e of
470+ MkEval envFn => envFn env