pass does nothing in instances of MonadWriter for stateT and eitherT #153
Description
pass can be used to suppress the output of a writer computation by mapping the output to the empty list:
Example writer_pass_applies_function_to_log :
let m : writer (@Monoid_list_app nat) unit :=
pass (bind (tell (cons 1 nil)) (fun _ =>
ret (tt, fun _ => nil)))
in
nil = PPair.psnd (runWriter m).
Proof. reflexivity. Qed.But pass does nothing when it's used with a stateT or eitherT that contains a writer. The output from the tell [1] persists through the call to pass:
Example stateT_writer_pass_applies_function_to_log :
let m : stateT nat (writer (@Monoid_list_app nat)) unit :=
pass (bind (tell (cons 1 nil)) (fun _ =>
ret (tt, fun _ => nil)))
in
nil = PPair.psnd (runWriter (runStateT m 0)).
Proof. simpl. (* nil = 1 :: nil *) Abort.
Example eitherT_writer_pass_applies_function_to_log :
let m : eitherT nat (writer (@Monoid_list_app nat)) unit :=
pass (bind (tell (cons 1 nil)) (fun _ =>
ret (tt, fun _ => nil)))
in
nil = PPair.psnd (runWriter (unEitherT m)).
Proof. simpl. (* nil = 1 :: nil *) Abort.