git.iko.soy/Idris-dev
on f6edbf0 help sign in
Idris-dev/lib/Control/IOExcept.idr
37 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 map f (ioM fn) = ioM (map (map 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 (ioM x) >>= k = ioM (do x' <- x;
20 case x' of
21 Right a => let (ioM ka) = k a in
22 ka
23 Left err => return (Left err))
25ioe_lift : IO a -> IOExcept err a
26ioe_lift op = ioM (do op' <- op
27 return (Right op'))
29ioe_fail : err -> IOExcept err a
30ioe_fail e = ioM (return (Left e))
32ioe_run : IOExcept err a -> (err -> IO b) -> (a -> IO b) -> IO b
33ioe_run (ioM act) err ok = do act' <- act
34 case act' of
35 Left e => err e
36 Right v => ok v