git.iko.soy/Idris-dev
on ea65347 help sign in
Idris-dev/libs/base/Control/IOExcept.idr
31 lines 803 B history raw
1module Control.IOExcept
3%access public export
5-- An IO monad with exception handling
7record IOExcept' (f:FFI) err a where
8 constructor IOM
9 runIOExcept : IO' f (Either err a)
11Functor (IOExcept' f e) where
12 map f (IOM fn) = IOM (map (map f) fn)
14Applicative (IOExcept' f e) where
15 pure x = IOM (pure (pure x))
16 (IOM f) <*> (IOM a) = IOM [| f <*> a |]
18Monad (IOExcept' f e) where
19 (IOM x) >>= f = IOM $ x >>= either (pure . Left) (runIOExcept . f)
21ioe_lift : IO' f a -> IOExcept' f err a
22ioe_lift op = IOM $ map Right op
24ioe_fail : err -> IOExcept' f err a
25ioe_fail e = IOM $ pure (Left e)
27ioe_run : IOExcept' f err a -> (err -> IO' f b) -> (a -> IO' f b) -> IO' f b
28ioe_run (IOM act) err ok = either err ok !act
30IOExcept : Type -> Type -> Type
31IOExcept = IOExcept' FFI_C