Extending Idris tutorial 4.4.1 to include a Let operation

expr.idr

data Expr = Var String
          | Val Int
          | Add Expr Expr
          | Let (List (String, Int)) Expr

data Eval : Type -> Type where
  MkEval : (List (String, Int) -> Maybe a) -> Eval a

fetch : String -> Eval Int
fetch x = MkEval (\e => fetchVal e) where
  fetchVal : List (String, Int) -> Maybe Int
  fetchVal [] = Nothing
  fetchVal ((v, val) :: xs) = if (x == v)
                                 then (Just val)
                                 else (fetchVal xs)

instance Functor Eval where
  map f (MkEval g) = MkEval (\e => map f (g e))

instance Applicative Eval where
  pure x = MkEval (\e => Just x)
  (<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
    app : Maybe (a -> b) -> Maybe a -> Maybe b
    app (Just fx) (Just gx) = Just (fx gx)
    app _         _         = Nothing

mutual
  eval : Expr -> Eval Int
  eval (Var x)     = fetch x
  eval (Val x)     = [| x |]
  eval (Add x y)   = [| eval x + eval y |]
  eval (Let newEnv x) = MkEval (\env => runEval (newEnv ++ env) x)

  runEval : List (String, Int) -> Expr -> Maybe Int
  runEval env e = case eval e of
                       MkEval envFn => envFn env

usage

*eval> runEval [("A", 2)] (Add (Var "A") (Let [("A", 40)] (Var "A")))
Just 42 : Maybe Int

*eval> runEval [("A", 1)] (Let [("A", 2)] (Let [("A", 3)] (Var "A")))
Just 3 : Maybe Int