git.iko.soy/Idris-dev
on master help sign in
Turn IOException into a record to avoid the let-binding patmatch.
80d88b1Leif Warner
libs/base/Control/IOExcept.idr+4−7
compare with master
unifiedsplit
@@ -2,8 +2,9 @@ module Control.IOExcept
2
2
3-- An IO monad with exception handling
3-- An IO monad with exception handling
4
4
5−data IOExcept : Type -> Type -> Type where
5+record IOExcept err a where
6+ constructor IOM
6− IOM : IO (Either err a) -> IOExcept err a
7+ runIOExcept : IO (Either err a)
7
8
8instance Functor (IOExcept e) where
9instance Functor (IOExcept e) where
9 map f (IOM fn) = IOM (map (map f) fn)
10 map f (IOM fn) = IOM (map (map f) fn)
@@ -13,11 +14,7 @@ instance Applicative (IOExcept e) where
13 (IOM f) <*> (IOM a) = IOM [| f <*> a |]
14 (IOM f) <*> (IOM a) = IOM [| f <*> a |]
14
15
15instance Monad (IOExcept e) where
16instance Monad (IOExcept e) where
16− (IOM x) >>= k = IOM (do x' <- x;
17+ (IOM x) >>= f = IOM $ x >>= either (pure . Left) (runIOExcept . f)
17− case x' of
18− Right a => let (IOM ka) = k a in
19− ka
20− Left err => return (Left err))
21
18
22ioe_lift : IO a -> IOExcept err a
19ioe_lift : IO a -> IOExcept err a
23ioe_lift op = IOM $ map Right op
20ioe_lift op = IOM $ map Right op