git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/libs/base/Control/Catchable.idr
56 lines 2.0 kB history raw
1module Control.Catchable
3import Control.IOExcept
4import Control.Monad.Reader
5import Control.Monad.Writer
6import Control.Monad.RWS
7import Control.Monad.Trans
9%access public export
11interface Catchable (m : Type -> Type) t | m where
12 throw : t -> m a
13 catch : m a -> (t -> m a) -> m a
15implementation Catchable Maybe () where
16 catch Nothing h = h ()
17 catch (Just x) h = Just x
19 throw () = Nothing
21implementation Catchable (Either a) a where
22 catch (Left err) h = h err
23 catch (Right x) h = (Right x)
25 throw = Left
27implementation Catchable (IOExcept err) err where
28 catch (IOM prog) h = IOM (do p' <- prog
29 case p' of
30 Left e => let IOM he = h e in he
31 Right val => pure (Right val))
32 throw = ioe_fail
34implementation Catchable List () where
35 catch [] h = h ()
36 catch xs h = xs
38 throw () = []
40||| Adapted from https://hackage.haskell.org/package/mtl-2.2.1/docs/src/Control.Monad.Error.Class.html#line-138
41implementation (Monad m, Catchable m t) => Catchable (ReaderT r m) t where
42 -- TODO: rewrite this with apply2way combinator when implemented
43 catch m h = RD $ \ r => catch (runReaderT m r) (\ e => runReaderT (h e) r)
44 -- catch m h = RD $ \ r => catch (runReaderT m r) (\ e => runReaderT (h e) r)
46 throw = lift . throw
48||| Adapted from https://hackage.haskell.org/package/transformers-0.5.4.0/docs/src/Control.Monad.Trans.Writer.Lazy.html#local-6989586621679059673
49implementation (Monad m, Monoid w, Catchable m t) => Catchable (WriterT w m) t where
50 catch m h = WR $ runWriterT m `catch` runWriterT . h
51 throw = lift . throw
53||| Adapted from https://hackage.haskell.org/package/mtl-2.2.1/docs/src/Control.Monad.Error.Class.html#line-138
54implementation (Monad m, Monoid w, Catchable m t) => Catchable (RWST r w s m) t where
55 catch m h = MkRWST $ \ r, s => runRWST m r s `catch` \ e => runRWST (h e) r s
56 throw = lift . throw