Library ExtLib.Data.Monads.WriterMonad
Require Import ExtLib.Structures.Monads.
Require Import ExtLib.Structures.Monoid.
Require Import ExtLib.Data.PPair.
Require Import ExtLib.Data.Monads.IdentityMonad.
Require Import Coq.Program.Basics.
Set Implicit Arguments.
Set Maximal Implicit Insertion.
Set Universe Polymorphism.
Set Printing Universes.
Section WriterType.
Polymorphic Universe s d c.
Variable S : Type@{s}.
Record writerT (Monoid_S : Monoid@{s} S) (m : Type@{d} -> Type@{c})
(t : Type@{d}) : Type := mkWriterT
{ runWriterT : m (pprod t S)%type }.
Variable Monoid_S : Monoid S.
Variable m : Type@{d} -> Type@{c}.
Context {M : Monad m}.
Arguments mkWriterT _ [_ _] _.
Definition execWriterT {T} (c : writerT Monoid_S m T) : m S :=
bind (runWriterT c) (fun (x : pprod T S) => ret (psnd x)).
Definition evalWriterT {T} (c : writerT Monoid_S m T) : m T :=
bind (runWriterT c) (fun (x : pprod T S) => ret (pfst x)).
Local Notation "( x , y )" := (ppair x y).
Global Instance Monad_writerT : Monad (writerT Monoid_S m) :=
{ ret := fun _ x => mkWriterT _ (@ret _ M _ (x, monoid_unit Monoid_S))
; bind := fun _ _ c1 c2 =>
mkWriterT _ (
@bind _ M _ _ (runWriterT c1) (fun v =>
bind (runWriterT (c2 (pfst v))) (fun v' =>
ret (pfst v', monoid_plus Monoid_S (psnd v) (psnd v')))))
}.
Global Instance Writer_writerT : MonadWriter Monoid_S (writerT Monoid_S m) :=
{ tell := fun x => mkWriterT _ (ret (tt, x))
; listen := fun _ c => mkWriterT _ (bind (runWriterT c)
(fun x => ret (pair (pfst x) (psnd x), psnd x)))
; pass := fun _ c => mkWriterT _ (bind (runWriterT c)
(fun x => ret (let '(ppair (pair x ss) s) := x in (x, ss s))))
}.
Global Instance MonadT_writerT : MonadT (writerT Monoid_S m) m :=
{ lift := fun _ c => mkWriterT _ (bind c (fun x => ret (x, monoid_unit Monoid_S)))
}.
Global Instance Reader_writerT {S'} (MR : MonadReader S' m) : MonadReader S' (writerT Monoid_S m) :=
{ ask := mkWriterT _ (bind ask (fun v => @ret _ M _ (v, monoid_unit Monoid_S)))
; local := fun _ f c =>
mkWriterT _ (local f (runWriterT c))
}.
Global Instance State_writerT {S'} (MR : MonadState S' m) : MonadState S' (writerT Monoid_S m) :=
{ get := lift get
; put := fun v => lift (put v)
}.
Global Instance Zero_writerT (MZ : MonadZero m) : MonadZero (writerT Monoid_S m) :=
{ mzero := fun _ => lift mzero }.
Global Instance Exception_writerT {E} (ME : MonadExc E m) : MonadExc E (writerT Monoid_S m) :=
{ raise := fun _ v => lift (raise v)
; catch := fun _ c h => mkWriterT _ (catch (runWriterT c) (fun x => runWriterT (h x)))
}.
Global Instance Writer_writerT_pass {T} {MonT : Monoid T} {M : Monad m} {MW : MonadWriter MonT m}
: MonadWriter MonT (writerT Monoid_S m) :=
{ tell := fun x => mkWriterT _ (bind (tell x)
(fun x => ret (x, monoid_unit Monoid_S)))
; listen := fun _ c => mkWriterT _ (bind (m:=m) (@listen _ _ _ MW _ (runWriterT c))
(fun x => let '(pair (ppair a t) s) := x in
ret (m:=m) (pair a s,t)))
; pass := fun _ c => mkWriterT _ (@pass _ _ _ MW _
(bind (m:=m) (runWriterT c)
(fun x => let '(ppair (pair a t) s) := x in
ret (m:=m) (pair (ppair a s) t))))
}.
End WriterType.
Arguments mkWriterT {_} _ {_ _} _.
Arguments runWriterT {S} {Monoid_S} {m} {t} _.
Arguments evalWriterT {S} {Monoid_S} {m} {M} {T} _.
Arguments execWriterT {S} {Monoid_S} {m} {M} {T} _.
Local Open Scope program_scope.
Section MapWriterT.
Variable W W': Type.
Variable Monoid_W : Monoid W.
Variable Monoid_W' : Monoid W'.
Variable m n : Type -> Type.
Variable A B: Type.
Require Import ExtLib.Structures.Monoid.
Require Import ExtLib.Data.PPair.
Require Import ExtLib.Data.Monads.IdentityMonad.
Require Import Coq.Program.Basics.
Set Implicit Arguments.
Set Maximal Implicit Insertion.
Set Universe Polymorphism.
Set Printing Universes.
Section WriterType.
Polymorphic Universe s d c.
Variable S : Type@{s}.
Record writerT (Monoid_S : Monoid@{s} S) (m : Type@{d} -> Type@{c})
(t : Type@{d}) : Type := mkWriterT
{ runWriterT : m (pprod t S)%type }.
Variable Monoid_S : Monoid S.
Variable m : Type@{d} -> Type@{c}.
Context {M : Monad m}.
Arguments mkWriterT _ [_ _] _.
Definition execWriterT {T} (c : writerT Monoid_S m T) : m S :=
bind (runWriterT c) (fun (x : pprod T S) => ret (psnd x)).
Definition evalWriterT {T} (c : writerT Monoid_S m T) : m T :=
bind (runWriterT c) (fun (x : pprod T S) => ret (pfst x)).
Local Notation "( x , y )" := (ppair x y).
Global Instance Monad_writerT : Monad (writerT Monoid_S m) :=
{ ret := fun _ x => mkWriterT _ (@ret _ M _ (x, monoid_unit Monoid_S))
; bind := fun _ _ c1 c2 =>
mkWriterT _ (
@bind _ M _ _ (runWriterT c1) (fun v =>
bind (runWriterT (c2 (pfst v))) (fun v' =>
ret (pfst v', monoid_plus Monoid_S (psnd v) (psnd v')))))
}.
Global Instance Writer_writerT : MonadWriter Monoid_S (writerT Monoid_S m) :=
{ tell := fun x => mkWriterT _ (ret (tt, x))
; listen := fun _ c => mkWriterT _ (bind (runWriterT c)
(fun x => ret (pair (pfst x) (psnd x), psnd x)))
; pass := fun _ c => mkWriterT _ (bind (runWriterT c)
(fun x => ret (let '(ppair (pair x ss) s) := x in (x, ss s))))
}.
Global Instance MonadT_writerT : MonadT (writerT Monoid_S m) m :=
{ lift := fun _ c => mkWriterT _ (bind c (fun x => ret (x, monoid_unit Monoid_S)))
}.
Global Instance Reader_writerT {S'} (MR : MonadReader S' m) : MonadReader S' (writerT Monoid_S m) :=
{ ask := mkWriterT _ (bind ask (fun v => @ret _ M _ (v, monoid_unit Monoid_S)))
; local := fun _ f c =>
mkWriterT _ (local f (runWriterT c))
}.
Global Instance State_writerT {S'} (MR : MonadState S' m) : MonadState S' (writerT Monoid_S m) :=
{ get := lift get
; put := fun v => lift (put v)
}.
Global Instance Zero_writerT (MZ : MonadZero m) : MonadZero (writerT Monoid_S m) :=
{ mzero := fun _ => lift mzero }.
Global Instance Exception_writerT {E} (ME : MonadExc E m) : MonadExc E (writerT Monoid_S m) :=
{ raise := fun _ v => lift (raise v)
; catch := fun _ c h => mkWriterT _ (catch (runWriterT c) (fun x => runWriterT (h x)))
}.
Global Instance Writer_writerT_pass {T} {MonT : Monoid T} {M : Monad m} {MW : MonadWriter MonT m}
: MonadWriter MonT (writerT Monoid_S m) :=
{ tell := fun x => mkWriterT _ (bind (tell x)
(fun x => ret (x, monoid_unit Monoid_S)))
; listen := fun _ c => mkWriterT _ (bind (m:=m) (@listen _ _ _ MW _ (runWriterT c))
(fun x => let '(pair (ppair a t) s) := x in
ret (m:=m) (pair a s,t)))
; pass := fun _ c => mkWriterT _ (@pass _ _ _ MW _
(bind (m:=m) (runWriterT c)
(fun x => let '(ppair (pair a t) s) := x in
ret (m:=m) (pair (ppair a s) t))))
}.
End WriterType.
Arguments mkWriterT {_} _ {_ _} _.
Arguments runWriterT {S} {Monoid_S} {m} {t} _.
Arguments evalWriterT {S} {Monoid_S} {m} {M} {T} _.
Arguments execWriterT {S} {Monoid_S} {m} {M} {T} _.
Local Open Scope program_scope.
Section MapWriterT.
Variable W W': Type.
Variable Monoid_W : Monoid W.
Variable Monoid_W' : Monoid W'.
Variable m n : Type -> Type.
Variable A B: Type.
Map both the return value and output of a computation using the given function.
[ 'runWriterT' ('mapWriterT' f m) = f ('runWriterT' m) ]
Definition mapWriterT (f: m (pprod A W) -> n (pprod B W'))
: writerT Monoid_W m A -> writerT Monoid_W' n B :=
mkWriterT Monoid_W' ∘ f ∘ runWriterT.
End MapWriterT.
Section CastWriterT.
Variable W : Type.
Variable Monoid_W Monoid_W': Monoid W.
Variable m : Type -> Type.
Variable A : Type.
Definition castWriterT
: writerT Monoid_W m A -> writerT Monoid_W' m A :=
mkWriterT Monoid_W' ∘ runWriterT.
End CastWriterT.
: writerT Monoid_W m A -> writerT Monoid_W' n B :=
mkWriterT Monoid_W' ∘ f ∘ runWriterT.
End MapWriterT.
Section CastWriterT.
Variable W : Type.
Variable Monoid_W Monoid_W': Monoid W.
Variable m : Type -> Type.
Variable A : Type.
Definition castWriterT
: writerT Monoid_W m A -> writerT Monoid_W' m A :=
mkWriterT Monoid_W' ∘ runWriterT.
End CastWriterT.
Simple wrapper around `writerT` specializing the underlying monad to `Identity`
which yields the `writer` monad.
Section WriterMonad.
Variable W: Type.
Variable Monoid_W : Monoid W.
Variable A: Type.
Definition writer : Type -> Type :=
writerT Monoid_W ident.
Definition runWriter : writer A -> pprod A W :=
unIdent ∘ (@runWriterT W Monoid_W ident A).
Definition execWriter : writer A -> W :=
psnd ∘ runWriter.
Definition evalWriter : writer A -> A :=
pfst ∘ runWriter.
End WriterMonad.
Section MapWriter.
Variable W W' : Type.
Variable Monoid_W: Monoid W.
Variable Monoid_W': Monoid W'.
Variable A B: Type.
Variable W: Type.
Variable Monoid_W : Monoid W.
Variable A: Type.
Definition writer : Type -> Type :=
writerT Monoid_W ident.
Definition runWriter : writer A -> pprod A W :=
unIdent ∘ (@runWriterT W Monoid_W ident A).
Definition execWriter : writer A -> W :=
psnd ∘ runWriter.
Definition evalWriter : writer A -> A :=
pfst ∘ runWriter.
End WriterMonad.
Section MapWriter.
Variable W W' : Type.
Variable Monoid_W: Monoid W.
Variable Monoid_W': Monoid W'.
Variable A B: Type.
Map both the return value and output of a computation using the given function.
[ 'runWriter' ('mapWriter' f m) = f ('runWriter' m) ]
Definition mapWriter (f: pprod A W -> pprod B W')
: writer Monoid_W A -> writer Monoid_W' B :=
mapWriterT Monoid_W' ident B (mkIdent ∘ f ∘ unIdent).
End MapWriter.
Section CastWriter.
Variable W : Type.
Variable Monoid_W Monoid_W': Monoid W.
Variable A : Type.
Definition castWriter
: writer Monoid_W A -> writer Monoid_W' A :=
castWriterT Monoid_W' (m:=ident).
End CastWriter.
: writer Monoid_W A -> writer Monoid_W' B :=
mapWriterT Monoid_W' ident B (mkIdent ∘ f ∘ unIdent).
End MapWriter.
Section CastWriter.
Variable W : Type.
Variable Monoid_W Monoid_W': Monoid W.
Variable A : Type.
Definition castWriter
: writer Monoid_W A -> writer Monoid_W' A :=
castWriterT Monoid_W' (m:=ident).
End CastWriter.