git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/libs/base/Control/Catchable.idr
32 lines 802 B history raw
1module Control.Catchable
3import Control.IOExcept
5class Catchable (m : Type -> Type) t where
6 throw : t -> m a
7 catch : m a -> (t -> m a) -> m a
9instance Catchable Maybe () where
10 catch Nothing h = h ()
11 catch (Just x) h = Just x
13 throw () = Nothing
15instance Catchable (Either a) a where
16 catch (Left err) h = h err
17 catch (Right x) h = (Right x)
19 throw x = Left x
21instance Catchable (IOExcept err) err where
22 catch (ioM prog) h = ioM (do p' <- prog
23 case p' of
24 Left e => let ioM he = h e in he
25 Right val => return (Right val))
26 throw x = ioM (return (Left x))
28instance Catchable List () where
29 catch [] h = h ()
30 catch xs h = xs
32 throw () = []