git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3876 from Synthetica9/Reader

Added Catchable for ReaderT, WriterT, and RWST

commit3bd96874163f9815be7b74d58f629f947a11b111 authorNiklas Larsson <metaniklas@gmail.com> dateSun 25 Jun 2017, 18:00 (9 years ago) parentc1329d75b1421f
3 files changed+34−2
compare with master
unifiedsplit
CHANGELOG.md+5−1 libs/base/Control/Catchable.idr+22 libs/base/Control/Monad/RWS.idr+7−1
CHANGELOG.md+5−1
@@ -4,7 +4,11 @@
44
55+ Added `Text.Lexer` and `Text.Parser` to `contrib`. These are small libraries
66 for implementing total lexical analysers and parsers.
7−
7++ New instances:
8+ + Added `Catchable` for `ReaderT`, `WriterT`, and `RWST`.
9+ + Added `MonadTrans` for `RWST`.
10++ Added utility functions to `Data.SortedMap` and `Data.SortedSet` (`contrib`),
11+ most notably `merge`, merging two maps by their `Semigroup` op (`<+>`)
812+ Added utility functions to `Data.SortedMap` and `Data.SortedSet` (`contrib`),
913 most notably `merge`, merging two maps by their `Semigroup` op (`<+>`)
1014
libs/base/Control/Catchable.idr+22
@@ -1,6 +1,10 @@
11module Control.Catchable
22
33import Control.IOExcept
4+import Control.Monad.Reader
5+import Control.Monad.Writer
6+import Control.Monad.RWS
7+import Control.Monad.Trans
48
59%access public export
610
@@ -32,3 +36,21 @@ implementation Catchable List () where
3236 catch xs h = xs
3337
3438 throw () = []
39+
40+||| Adapted from https://hackage.haskell.org/package/mtl-2.2.1/docs/src/Control.Monad.Error.Class.html#line-138
41+implementation (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)
45+
46+ throw = lift . throw
47+
48+||| Adapted from https://hackage.haskell.org/package/transformers-0.5.4.0/docs/src/Control.Monad.Trans.Writer.Lazy.html#local-6989586621679059673
49+implementation (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
52+
53+||| Adapted from https://hackage.haskell.org/package/mtl-2.2.1/docs/src/Control.Monad.Error.Class.html#line-138
54+implementation (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
libs/base/Control/Monad/RWS.idr+7−1
@@ -14,7 +14,7 @@ interface (Monoid w, MonadReader r m, MonadWriter w m, MonadState s m) => MonadR
1414record RWST (r : Type) (w : Type) (s : Type) (m : Type -> Type) (a : Type) where
1515 constructor MkRWST
1616 runRWST : r -> s -> m (a, s, w)
17−
17+
1818implementation Monad m => Functor (RWST r w s m) where
1919 map f (MkRWST m) = MkRWST $ \r,s => do (a, s', w) <- m r s
2020 pure (f a, s', w)
@@ -48,6 +48,12 @@ implementation (Monoid w, Monad m) => MonadState s (RWST r w s m) where
4848
4949implementation (Monoid w, Monad m) => MonadRWS r w s (RWST r w s m) where {}
5050
51+||| Adapted from https://hackage.haskell.org/package/transformers-0.5.4.0/docs/src/Control-Monad-Trans-RWS-Lazy.html
52+implementation Monoid w => MonadTrans (RWST r w s) where
53+ lift x = MkRWST $ \ _, s => do
54+ a <- x
55+ pure (a, s, neutral)
56+
5157||| The RWS monad. See the MonadRWS interface
5258RWS : Type -> Type -> Type -> Type -> Type
5359RWS r w s a = RWST r w s Identity a