git.iko.soy/Idris-dev
on e8a41dc help sign in
Idris-dev/libs/base/Control/IOExcept.idr
29 lines 780 B history raw
1module Control.IOExcept
3-- An IO monad with exception handling
5record IOExcept' (f:FFI) err a where
6 constructor IOM
7 runIOExcept : IO' f (Either err a)
9Functor (IOExcept' f e) where
10 map f (IOM fn) = IOM (map (map f) fn)
12Applicative (IOExcept' f e) where
13 pure x = IOM (pure (pure x))
14 (IOM f) <*> (IOM a) = IOM [| f <*> a |]
16Monad (IOExcept' f e) where
17 (IOM x) >>= f = IOM $ x >>= either (pure . Left) (runIOExcept . f)
19ioe_lift : IO' f a -> IOExcept' f err a
20ioe_lift op = IOM $ map Right op
22ioe_fail : err -> IOExcept' f err a
23ioe_fail e = IOM $ pure (Left e)
25ioe_run : IOExcept' f err a -> (err -> IO' f b) -> (a -> IO' f b) -> IO' f b
26ioe_run (IOM act) err ok = either err ok !act
28IOExcept : Type -> Type -> Type
29IOExcept = IOExcept' FFI_C