@@ -0,0 +1,53 @@
1+module main;
2+
3+instance Applicative Maybe where {
4+ (Just f) <$> (Just a) = Just (f a);
5+ Nothing <$> Nothing = Nothing;
6+
7+ pure x = Just x;
8+}
9+
10+data Expr = Var String
11+ | Val Int
12+ | Add Expr Expr;
13+
14+
15+data Eval : Set -> Set where
16+ MkEval : (List (String, Int) -> Maybe a) -> Eval a;
17+
18+fetch : String -> Eval Int;
19+fetch x = MkEval (\e => fetchVal e) where {
20+ fetchVal : List (String, Int) -> Maybe Int;
21+ fetchVal [] = Nothing;
22+ fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs);
23+}
24+
25+instance Applicative Eval where {
26+ pure x = MkEval (\e => Just x);
27+
28+ (<$>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where {
29+ appAux : Maybe (a -> b) -> Maybe a -> Maybe b;
30+ appAux (Just fx) (Just gx) = Just (fx gx);
31+ appAux _ _ = Nothing;
32+ }
33+}
34+
35+eval : Expr -> Eval Int;
36+eval (Var x) = fetch x;
37+eval (Val x) = [| x |];
38+eval (Add x y) = [| eval x + eval y |];
39+
40+runEval : List (String, Int) -> Expr -> Maybe Int;
41+runEval env e with eval e {
42+ | MkEval envFn = envFn env;
43+}
44+
45+main : IO ();
46+main = do { print [| (*2) (Just 4) |];
47+ print [| plus (Just 4) (Just 5) |];
48+ print (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))));
49+ print (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))));
50+ };
51+
52+
53+