Theory Writer_Monad

section ‹Writer monad›

theory Writer_Monad
imports Monad
begin

subsection ‹Monoid class›

class monoid = "domain" +
  fixes mempty :: "'a"
  fixes mappend :: "'a → 'a → 'a"
  assumes mempty_left: "⋀ys. mappend⋅mempty⋅ys = ys"
  assumes mempty_right: "⋀xs. mappend⋅xs⋅mempty = xs"
  assumes mappend_assoc:
    "⋀xs ys zs. mappend⋅(mappend⋅xs⋅ys)⋅zs = mappend⋅xs⋅(mappend⋅ys⋅zs)"

subsection ‹Writer monad type›

text ‹Below is the standard Haskell definition of a writer monad
type; it is an isomorphic copy of the lazy pair type \texttt{(a, w)}.
›

text_raw ‹
\begin{verbatim}
newtype Writer w a = Writer { runWriter :: (a, w) }
\end{verbatim}
›

text ‹Since HOLCF does not have a pre-defined lazy pair type, we
will base this formalization on an equivalent, more direct definition:
›

text_raw ‹
\begin{verbatim}
data Writer w a = Writer w a
\end{verbatim}
›

text ‹We can directly translate the above Haskell type definition
using ‹tycondef›. \medskip›

tycondef 'a⋅'w writer = Writer (lazy "'w") (lazy "'a")

lemma coerce_writer_abs [simp]: "coerce⋅(writer_abs⋅x) = writer_abs⋅(coerce⋅x)"
apply (simp add: writer_abs_def coerce_def)
apply (simp add: emb_prj_emb prj_emb_prj DEFL_eq_writer)
done

lemma coerce_Writer [simp]:
  "coerce⋅(Writer⋅w⋅x) = Writer⋅(coerce⋅w)⋅(coerce⋅x)"
unfolding Writer_def by simp

lemma fmapU_writer_simps [simp]:
  "fmapU⋅f⋅(⊥::udom⋅'w writer) = ⊥"
  "fmapU⋅f⋅(Writer⋅w⋅x) = Writer⋅w⋅(f⋅x)"
unfolding fmapU_writer_def writer_map_def fix_const
apply simp
apply (simp add: Writer_def)
done

subsection ‹Class instance proofs›

instance writer :: ("domain") "functor"
proof
  fix f g :: "udom → udom" and xs :: "udom⋅'a writer"
  show "fmapU⋅f⋅(fmapU⋅g⋅xs) = fmapU⋅(Λ x. f⋅(g⋅x))⋅xs"
    by (induct xs rule: writer.induct) simp_all
qed

instantiation writer :: (monoid) monad
begin

fixrec bindU_writer ::
    "udom⋅'a writer → (udom → udom⋅'a writer) → udom⋅'a writer"
  where "bindU_writer⋅(Writer⋅w⋅x)⋅f =
    (case f⋅x of Writer⋅w'⋅y ⇒ Writer⋅(mappend⋅w⋅w')⋅y)"

lemma bindU_writer_strict [simp]: "bindU⋅⊥⋅k = (⊥::udom⋅'a writer)"
by fixrec_simp

definition
  "returnU = Writer⋅mempty"

instance proof
  fix f :: "udom → udom" and m :: "udom⋅'a writer"
  show "fmapU⋅f⋅m = bindU⋅m⋅(Λ x. returnU⋅(f⋅x))"
    by (induct m rule: writer.induct)
       (simp_all add: returnU_writer_def mempty_right)
next
  fix f :: "udom → udom⋅'a writer" and x :: "udom"
  show "bindU⋅(returnU⋅x)⋅f = f⋅x"
    by (cases "f⋅x" rule: writer.exhaust)
       (simp_all add: returnU_writer_def mempty_left)
next
  fix m :: "udom⋅'a writer" and f g :: "udom → udom⋅'a writer"
  show "bindU⋅(bindU⋅m⋅f)⋅g = bindU⋅m⋅(Λ x. bindU⋅(f⋅x)⋅g)"
    apply (induct m rule: writer.induct, simp)
    apply (case_tac "f⋅a" rule: writer.exhaust, simp)
    apply (case_tac "g⋅aa" rule: writer.exhaust, simp)
    apply (simp add: mappend_assoc)
    done
qed

end

subsection ‹Transfer properties to polymorphic versions›

lemma fmap_writer_simps [simp]:
  "fmap⋅f⋅(⊥::'a⋅'w writer) = ⊥"
  "fmap⋅f⋅(Writer⋅w⋅x :: 'a⋅'w writer) = Writer⋅w⋅(f⋅x)"
unfolding fmap_def [where 'f="'w writer"]
by (simp_all add: coerce_simp)

lemma return_writer_def: "return = Writer⋅mempty"
unfolding return_def returnU_writer_def
by (simp add: coerce_simp eta_cfun)

lemma bind_writer_simps [simp]:
  "bind⋅(⊥ :: 'a⋅'w::monoid writer)⋅f = ⊥"
  "bind⋅(Writer⋅w⋅x :: 'a⋅'w::monoid writer)⋅k =
    (case k⋅x of Writer⋅w'⋅y ⇒ Writer⋅(mappend⋅w⋅w')⋅y)"
unfolding bind_def
apply (simp add: coerce_simp)
apply (cases "k⋅x" rule: writer.exhaust)
apply (simp_all add: coerce_simp)
done

lemma join_writer_simps [simp]:
  "join⋅⊥ = (⊥ :: 'a⋅'w::monoid writer)"
  "join⋅(Writer⋅w⋅(Writer⋅w'⋅x)) = Writer⋅(mappend⋅w⋅w')⋅x"
unfolding join_def by simp_all

subsection ‹Extra operations›

definition tell :: "'w → unit⋅('w::monoid writer)"
  where "tell = (Λ w. Writer⋅w⋅())"

end