2e55414 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1838 from L8D/master

Add type class and instances for monad transformers

commit2e55414ad9195008dd53358305967613f909c8d8 authorDavid Christiansen <david@davidchristiansen.dk> dateSat 10 Jan 2015, 17:29 (12 years ago) parent41862e4 ac2a6f2

4 files changed+18

compare with master

unifiedsplit

libs/base/Control/Monad/Reader.idr+4 libs/base/Control/Monad/State.idr+5 libs/base/Control/Monad/Trans.idr+4 libs/base/Control/Monad/Writer.idr+5

libs/base/Control/Monad/Reader.idr+4

@@ -2,6 +2,7 @@ module Control.Monad.Reader

33import Builtins

44import Control.Monad.Identity

5+import Control.Monad.Trans

67%access public

@@ -41,6 +42,9 @@ instance Monad m => MonadReader r (ReaderT r m) where

4142 ask = RD return

4243 local f (RD m) = RD $ m . f

4344

45+instance MonadTrans (ReaderT r) where

46+ lift x = RD (const x)

47+

4448||| Evaluate a function in the context of a Reader monad

4549asks : MonadReader r m => (r -> a) -> m a

4650asks f = do r <- ask

libs/base/Control/Monad/State.idr+5

@@ -1,6 +1,7 @@

11module Control.Monad.State

33import Control.Monad.Identity

4+import Control.Monad.Trans

56%access public

@@ -37,6 +38,10 @@ instance Monad m => MonadState s (StateT s m) where

3738 get = ST (\x => return (x, x))

3839 put x = ST (\y => return ((), x))

3940

41+instance MonadTrans (StateT s) where

42+ lift x = ST (\st => do r <- x

43+ return (r, st))

44+

4045||| Apply a function to modify the context of this computation

4146modify : MonadState s m => (s -> s) -> m ()

4247modify f = do s <- get

libs/base/Control/Monad/Trans.idrnew file+4

@@ -0,0 +1,4 @@

1+module Control.Monad.Trans

3+class MonadTrans (t : (Type -> Type) -> Type -> Type) where

4+ lift : Monad m => m a -> t m a

libs/base/Control/Monad/Writer.idr+5

@@ -2,6 +2,7 @@ module Control.Monad.Writer

33import Builtins

44import Control.Monad.Identity

5+import Control.Monad.Trans

67%access public

@@ -44,6 +45,10 @@ instance (Monoid w, Monad m) => MonadWriter w (WriterT w m) where

4445 pass (WR m) = WR $ do ((a, f), w) <- m

4546 return (a, f w)

4647

48+instance Monoid w => MonadTrans (WriterT w) where

49+ lift x = WR $ do r <- x

50+ return (r, neutral)

51+

4752||| Run an action in the Writer monad and transform the written output

4853listens : MonadWriter w m => (w -> b) -> m a -> m (a, b)

4954listens f m = listens' f (listen m) where