MonadError, the errorful Monad transformer

libs/base/Control/Monad/Error.idr

@@ -0,0 +1,49 @@
+module Control.Monad.Error
+import Control.Monad.Trans
+
+public export
+interface Monad m => MonadError e m where
+    throw : e -> m a
+    catch : m a -> ( e -> m a ) -> m a
+
+public export
+data ErrorT : Type -> ( Type -> Type ) -> Type -> Type where
+    RunErrorT : m ( Either e a ) -> ErrorT e m a
+
+public export
+IOError : Type -> Type -> Type
+IOError e a = ErrorT e IO a
+
+public export
+Functor m => Functor( ErrorT e m ) where
+    map f ( RunErrorT op ) = RunErrorT( map ( map f ) op )
+
+public export
+Monad m => Applicative( ErrorT e m ) where
+    pure x = RunErrorT( pure ( Right x ) )
+    RunErrorT f <*> RunErrorT op = RunErrorT $
+        op >>= \ e_val => map ( <*> e_val ) f
+
+public export
+Monad m => Monad( ErrorT e m ) where
+    RunErrorT op >>= f = RunErrorT $ op >>= \ e_val =>
+        case e_val of
+            Left  err => pure( Left err )
+            Right val => let RunErrorT op = f val in op
+
+public export
+Monad m => MonadError e ( ErrorT e m ) where
+    throw = RunErrorT . pure . Left
+    catch( RunErrorT op ) handler = RunErrorT $ op >>= \ e_val => case e_val of
+        Left  err => let RunErrorT op' = handler err in op'
+        Right val => pure( Right val )
+
+public export
+MonadTrans( ErrorT e ) where
+--  lift : Monad m => m a -> ErrorT e m a
+    lift op = RunErrorT( map Right op )
+
+throwIf : MonadError e m => Bool -> Lazy e -> m ()
+throwIf test err = if test
+    then throw err
+    else pure ()

libs/base/Control/Monad/Error/IORef.idr

@@ -0,0 +1,11 @@
+module Control.Monad.Error.IORef
+import Control.Monad.Error
+import Data.IORef
+
+public export
+overIORef : IORef a -> ( a -> IOError e a ) -> IOError e a
+overIORef ref xform = do
+    val <- lift( readIORef ref )
+    newval <- xform val
+    lift( writeIORef ref newval )
+    pure newval

libs/base/base.ipkg

@@ -3,6 +3,8 @@ package base
 modules = Control.Monad.Identity,
           Control.Monad.State,
           Control.Monad.Trans,
+		  Control.Monad.Error,
+		  Control.Monad.Error.IORef,
           Control.WellFounded,
 
           Data.Buffer,

libs/prelude/Prelude.idr

@@ -736,6 +736,16 @@ Monad (Either e) where
     (Left n) >>= _ = Left n
     (Right r) >>= f = f r
 
+public export
+Foldable (Either e) where
+	foldr _ z ( Left  _ ) = z
+	foldr f z ( Right x ) = f x z
+
+public export
+Traversable (Either e) where
+	traverse _ ( Left  e ) = pure( Left e )
+	traverse f ( Right x ) = map Right ( f x )
+
 -----------
 -- LISTS --
 -----------

src/Core/Context.idr

@@ -77,7 +77,7 @@ Show Def where
   show (ExternDef arity) = "<external def with arity " ++ show arity ++ ">"
   show (ForeignDef a cs) = "<foreign def with arity " ++ show a ++
                            " " ++ show cs ++">"
-  show (Builtin {arity} _) = "<builtin with arith " ++ show arity ++ ">"
+  show (Builtin {arity} _) = "<builtin with arity " ++ show arity ++ ">"
   show (Hole _ p) = "Hole" ++ if p then " [impl]" else ""
   show (BySearch c depth def) = "Search in " ++ show def
   show (Guess tm _ cs) = "Guess " ++ show tm ++ " when " ++ show cs