@@ -0,0 +1,38 @@
1+module idiom
2+
3+data Expr = Var String
4+ | Val Int
5+ | Add Expr Expr
6+
7+data Eval : Set -> Set where
8+ MkEval : (List (String, Int) -> Maybe a) -> Eval a
9+
10+fetch : String -> Eval Int
11+fetch x = MkEval (\e => fetchVal e) where
12+ fetchVal : List (String, Int) -> Maybe Int
13+ fetchVal [] = Nothing
14+ fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)
15+
16+instance Functor Eval where
17+ fmap f (MkEval g) = MkEval (\e => fmap f (g e))
18+
19+instance Applicative Eval where
20+ pure x = MkEval (\e => Just x)
21+
22+ (<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
23+ app : Maybe (a -> b) -> Maybe a -> Maybe b
24+ app (Just fx) (Just gx) = Just (fx gx)
25+ app _ _ = Nothing
26+
27+eval : Expr -> Eval Int
28+eval (Var x) = fetch x
29+eval (Val x) = [| x |]
30+eval (Add x y) = [| eval x + eval y |]
31+
32+runEval : List (String, Int) -> Expr -> Maybe Int
33+runEval env e = case eval e of
34+ MkEval envFn => envFn env
35+
36+m_add' : Maybe Int -> Maybe Int -> Maybe Int
37+m_add' x y = [| x + y |]
38+