git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/libs/base/Control/IOExcept.idr
35 lines 1.1 kB history raw
1module Control.IOExcept
3-- An IO monad with exception handling
5data IOExcept : Type -> Type -> Type where
6 ioM : IO (Either err a) -> IOExcept err a
8instance Functor (IOExcept e) where
9 map f (ioM fn) = ioM (map (map f) fn)
11instance Applicative (IOExcept e) where
12 pure x = ioM (pure (pure x))
13 (ioM f) <$> (ioM a) = ioM (do f' <- f; a' <- a
14 return (f' <$> a'))
16instance Monad (IOExcept e) where
17 (ioM x) >>= k = ioM (do x' <- x;
18 case x' of
19 Right a => let (ioM ka) = k a in
20 ka
21 Left err => return (Left err))
23ioe_lift : IO a -> IOExcept err a
24ioe_lift op = ioM (do op' <- op
25 return (Right op'))
27ioe_fail : err -> IOExcept err a
28ioe_fail e = ioM (return (Left e))
30ioe_run : IOExcept err a -> (err -> IO b) -> (a -> IO b) -> IO b
31ioe_run (ioM act) err ok = do act' <- act
32 case act' of
33 Left e => err e
34 Right v => ok v