@@ -355,9 +355,10 @@ m_add' x y = m_app (m_app (Just (+)) x) y
355\useverb{maddb}
355\useverb{maddb}
358−Rather than having to insert \texttt{m\_app} everywhere there is an application, we can
358+Rather than having to insert \texttt{m\_app} everywhere there is an
359−use \remph{idiom brackets} to do the job for us. To do this, we use the \texttt{Applicative}
359+application, we can use \remph{idiom brackets} to do the job for us. To do
360+this, we use the \texttt{Applicative} class, which captures the notion of
360−class, which captures the notion of application for a data type:
361+application for a data type:
362\begin{SaveVerbatim}{applicative}
363\begin{SaveVerbatim}{applicative}
@@ -371,8 +372,8 @@ class Applicative (f : Type -> Type) where
371\useverb{applicative}
372\useverb{applicative}
374−\texttt{Maybe} is made an instance of \texttt{Applicative} as follows, where \texttt{<\$>}
375+\texttt{Maybe} is made an instance of \texttt{Applicative} as follows, where
375−is defined in the same way as \texttt{m\_app} above:
376+\texttt{<\$>} is defined in the same way as \texttt{m\_app} above:
377\begin{SaveVerbatim}{maybeapp}
378\begin{SaveVerbatim}{maybeapp}
@@ -443,15 +444,21 @@ fetch x = MkEval (\e => fetchVal e) where
443\useverb{fetch}
444\useverb{fetch}
446−When defining an evaluator for the language, we will be applying functions in the
447+When defining an evaluator for the language, we will be applying functions in
447−context of an \texttt{Eval}, so it is natural to make \texttt{Eval} an instance
448+the context of an \texttt{Eval}, so it is natural to make \texttt{Eval} an
448−of \texttt{Applicative}:
449+instance of \texttt{Applicative}.
450+Before \texttt{Eval} can be an instance of
451+\texttt{Applicative} it is necessary to make \texttt{Eval} an instance of
450\begin{SaveVerbatim}{}
454\begin{SaveVerbatim}{}
456+instance Functor Eval where
457+ fmap f (MkEval g) = MkEval (\e => fmap f (g e))
452instance Applicative Eval where
459instance Applicative Eval where
453 pure x = MkEval (\e => Just x)
460 pure x = MkEval (\e => Just x)
455 (<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
462 (<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
456 app : Maybe (a -> b) -> Maybe a -> Maybe b
463 app : Maybe (a -> b) -> Maybe a -> Maybe b
457 app (Just fx) (Just gx) = Just (fx gx)
464 app (Just fx) (Just gx) = Just (fx gx)