git.iko.soy/Idris-dev
on d3fa352 help sign in
Idris-dev/libs/base/Control/Catchable.idr
34 lines 836 B history raw
1module Control.Catchable
3import Control.IOExcept
5%access public export
7interface Catchable (m : Type -> Type) t | m where
8 throw : t -> m a
9 catch : m a -> (t -> m a) -> m a
11implementation Catchable Maybe () where
12 catch Nothing h = h ()
13 catch (Just x) h = Just x
15 throw () = Nothing
17implementation Catchable (Either a) a where
18 catch (Left err) h = h err
19 catch (Right x) h = (Right x)
21 throw = Left
23implementation Catchable (IOExcept err) err where
24 catch (IOM prog) h = IOM (do p' <- prog
25 case p' of
26 Left e => let IOM he = h e in he
27 Right val => pure (Right val))
28 throw = ioe_fail
30implementation Catchable List () where
31 catch [] h = h ()
32 catch xs h = xs
34 throw () = []