Theory Monad

section ‹Monad Class›

theory Monad
imports Functor
begin

subsection ‹Class definition›

text ‹In Haskell, class \emph{Monad} is defined as follows:›

text_raw ‹
\begin{verbatim}
class Monad m where
  return :: a -> m a
  (>>=) :: m a -> (a -> m b) -> m b
\end{verbatim}
›

text ‹We formalize class ‹monad› in a manner similar to the
‹functor› class: We fix monomorphic versions of the class
constants, replacing type variables with ‹udom›, and assume
monomorphic versions of the class axioms.›

text ‹Because the monad laws imply the composition rule for ‹fmap›, we declare ‹prefunctor› as the superclass, and separately
prove a subclass relationship with ‹functor›.›

class monad = prefunctor +
  fixes returnU :: "udom → udom⋅'a::tycon"
  fixes bindU :: "udom⋅'a → (udom → udom⋅'a) → udom⋅'a"
  assumes fmapU_eq_bindU:
    "⋀f xs. fmapU⋅f⋅xs = bindU⋅xs⋅(Λ x. returnU⋅(f⋅x))"
  assumes bindU_returnU:
    "⋀f x. bindU⋅(returnU⋅x)⋅f = f⋅x"
  assumes bindU_bindU:
    "⋀xs f g. bindU⋅(bindU⋅xs⋅f)⋅g = bindU⋅xs⋅(Λ x. bindU⋅(f⋅x)⋅g)"

instance monad ⊆ "functor"
proof
  fix f g :: "udom → udom" and xs :: "udom⋅'a"
  show "fmapU⋅f⋅(fmapU⋅g⋅xs) = fmapU⋅(Λ x. f⋅(g⋅x))⋅xs"
    by (simp add: fmapU_eq_bindU bindU_bindU bindU_returnU)
qed

text ‹As with ‹fmap›, we define the polymorphic ‹return›
and ‹bind› by coercion from the monomorphic ‹returnU› and
‹bindU›.›

definition return :: "'a → 'a⋅'m::monad"
  where "return = coerce⋅(returnU :: udom → udom⋅'m)"

definition bind :: "'a⋅'m::monad → ('a → 'b⋅'m) → 'b⋅'m"
  where "bind = coerce⋅(bindU :: udom⋅'m → _)"

abbreviation bind_syn :: "'a⋅'m::monad ⇒ ('a → 'b⋅'m) ⇒ 'b⋅'m" (infixl ‹⤜› 55)
  where "m ⤜ f ≡ bind⋅m⋅f"

subsection ‹Naturality of bind and return›

text ‹The three class axioms imply naturality properties of ‹returnU› and ‹bindU›, i.e., that both commute with ‹fmapU›.›

lemma fmapU_returnU [coerce_simp]:
  "fmapU⋅f⋅(returnU⋅x) = returnU⋅(f⋅x)"
by (simp add: fmapU_eq_bindU bindU_returnU)

lemma fmapU_bindU [coerce_simp]:
  "fmapU⋅f⋅(bindU⋅m⋅k) = bindU⋅m⋅(Λ x. fmapU⋅f⋅(k⋅x))"
by (simp add: fmapU_eq_bindU bindU_bindU)

lemma bindU_fmapU:
  "bindU⋅(fmapU⋅f⋅xs)⋅k = bindU⋅xs⋅(Λ x. k⋅(f⋅x))"
by (simp add: fmapU_eq_bindU bindU_returnU bindU_bindU)

subsection ‹Polymorphic versions of class assumptions›

lemma monad_fmap:
  fixes xs :: "'a⋅'m::monad" and f :: "'a → 'b"
  shows "fmap⋅f⋅xs = xs ⤜ (Λ x. return⋅(f⋅x))"
unfolding bind_def return_def fmap_def
by (simp add: coerce_simp fmapU_eq_bindU bindU_returnU)

lemma monad_left_unit [simp]: "(return⋅x ⤜ f) = (f⋅x)"
unfolding bind_def return_def
by (simp add: coerce_simp bindU_returnU)

lemma bind_bind:
  fixes m :: "'a⋅'m::monad"
  shows "((m ⤜ f) ⤜ g) = (m ⤜ (Λ x. f⋅x ⤜ g))"
unfolding bind_def
by (simp add: coerce_simp bindU_bindU)

subsection ‹Derived rules›

text ‹The following properties can be derived using only the
abstract monad laws.›

lemma monad_right_unit [simp]: "(m ⤜ return) = m"
 apply (subgoal_tac "fmap⋅ID⋅m = m")
  apply (simp only: monad_fmap)
  apply (simp add: eta_cfun)
 apply simp
done

lemma fmap_return: "fmap⋅f⋅(return⋅x) = return⋅(f⋅x)"
by (simp add: monad_fmap)

lemma fmap_bind: "fmap⋅f⋅(bind⋅xs⋅k) = bind⋅xs⋅(Λ x. fmap⋅f⋅(k⋅x))"
by (simp add: monad_fmap bind_bind)

lemma bind_fmap: "bind⋅(fmap⋅f⋅xs)⋅k = bind⋅xs⋅(Λ x. k⋅(f⋅x))"
by (simp add: monad_fmap bind_bind)

text ‹Bind is strict in its first argument, if its second argument
is a strict function.›

lemma bind_strict:
  assumes "k⋅⊥ = ⊥" shows "⊥ ⤜ k = ⊥"
proof -
  have "⊥ ⤜ k ⊑ return⋅⊥ ⤜ k"
    by (intro monofun_cfun below_refl minimal)
  thus "⊥ ⤜ k = ⊥"
    by (simp add: assms)
qed

lemma congruent_bind:
  "(∀m. m ⤜ k1 = m ⤜ k2) = (k1 = k2)"
 apply (safe, rule cfun_eqI)
 apply (drule_tac x="return⋅x" in spec, simp)
done

subsection ‹Laws for join›

definition join :: "('a⋅'m)⋅'m → 'a⋅'m::monad"
  where "join ≡ Λ m. m ⤜ (Λ x. x)"

lemma join_fmap_fmap: "join⋅(fmap⋅(fmap⋅f)⋅xss) = fmap⋅f⋅(join⋅xss)"
by (simp add: join_def monad_fmap bind_bind)

lemma join_return: "join⋅(return⋅xs) = xs"
by (simp add: join_def)

lemma join_fmap_return: "join⋅(fmap⋅return⋅xs) = xs"
by (simp add: join_def monad_fmap eta_cfun bind_bind)

lemma join_fmap_join: "join⋅(fmap⋅join⋅xsss) = join⋅(join⋅xsss)"
by (simp add: join_def monad_fmap bind_bind)

lemma bind_def2: "m ⤜ k = join⋅(fmap⋅k⋅m)"
by (simp add: join_def monad_fmap eta_cfun bind_bind)

subsection ‹Equivalence of monad laws and fmap/join laws›

lemma "(return⋅x ⤜ f) = (f⋅x)"
by (simp only: bind_def2 fmap_return join_return)

lemma "(m ⤜ return) = m"
by (simp only: bind_def2 join_fmap_return)

lemma "((m ⤜ f) ⤜ g) = (m ⤜ (Λ x. f⋅x ⤜ g))"
 apply (simp only: bind_def2)
 apply (subgoal_tac "join⋅(fmap⋅g⋅(join⋅(fmap⋅f⋅m))) =
    join⋅(fmap⋅join⋅(fmap⋅(fmap⋅g)⋅(fmap⋅f⋅m)))")
  apply (simp add: fmap_fmap)
 apply (simp add: join_fmap_join join_fmap_fmap)
done

subsection ‹Simplification of coercions›

text ‹We configure rewrite rules that push coercions inwards, and
reduce them to coercions on simpler types.›

lemma coerce_return [coerce_simp]:
  "COERCE('a⋅'m,'b⋅'m::monad)⋅(return⋅x) = return⋅(COERCE('a,'b)⋅x)"
by (simp add: coerce_functor fmap_return)

lemma coerce_bind [coerce_simp]:
  fixes m :: "'a⋅'m::monad" and k :: "'a → 'b⋅'m"
  shows "COERCE('b⋅'m,'c⋅'m)⋅(m ⤜ k) = m ⤜ (Λ x. COERCE('b⋅'m,'c⋅'m)⋅(k⋅x))"
by (simp add: coerce_functor fmap_bind)

lemma bind_coerce [coerce_simp]:
  fixes m :: "'a⋅'m::monad" and k :: "'b → 'c⋅'m"
  shows "COERCE('a⋅'m,'b⋅'m)⋅m ⤜ k = m ⤜ (Λ x. k⋅(COERCE('a,'b)⋅x))"
by (simp add: coerce_functor bind_fmap)

end