git.iko.soy/Idris-dev
on ff0fbfa help sign in
Idris-dev/lib/Control/IOExcept.idr
38 lines 1.2 kB history raw
1module Control.IOExcept
3import Prelude
5-- An IO monad with exception handling
7data IOExcept : Type -> Type -> Type where
8 ioM : IO (Either err a) -> IOExcept err a
10instance Functor (IOExcept e) where
11 fmap f (ioM fn) = ioM (fmap (fmap f) fn)
13instance Applicative (IOExcept e) where
14 pure x = ioM (pure (pure x))
15 (ioM f) <$> (ioM a) = ioM (do f' <- f; a' <- a
16 return (f' <$> a'))
18instance Monad (IOExcept e) where
19 return = pure
20 (ioM x) >>= k = ioM (do x' <- x;
21 case x' of
22 Right a => let (ioM ka) = k a in
23 ka
24 Left err => return (Left err))
26ioe_lift : IO a -> IOExcept err a
27ioe_lift op = ioM (do op' <- op
28 return (Right op'))
30ioe_fail : err -> IOExcept err a
31ioe_fail e = ioM (return (Left e))
33ioe_run : IOExcept err a -> (err -> IO b) -> (a -> IO b) -> IO b
34ioe_run (ioM act) err ok = do act' <- act
35 case act' of
36 Left e => err e
37 Right v => ok v