feat(category/monad/cont): monad_cont instances for state_t, reader_t, except_t and option_t (#733)

* feat(category/monad/cont): monad_cont instances for state_t, reader_t,
except_t and option_t

* feat(category/monad/writer): writer monad transformer

Author: cipher1024

src/category/monad/basic.lean

@@ -0,0 +1,9 @@
+
+import tactic.interactive
+
+attribute [extensionality] reader_t.ext state_t.ext except_t.ext option_t.ext
+attribute [functor_norm]   bind_assoc pure_bind bind_pure
+universes u v
+
+lemma map_eq_bind_pure_comp (m : Type u → Type v) [monad m] [is_lawful_monad m] {α β : Type u} (f : α → β) (x : m α) :
+  f <$> x = x >>= pure ∘ f := by rw bind_pure_comp_eq_map

src/category/monad/cont.lean

@@ -9,6 +9,7 @@ http://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Cont.html
 -/
 
 import tactic.ext
+import category.monad.basic category.monad.writer
 
 universes u v w
 
@@ -17,13 +18,12 @@ structure monad_cont.label (α : Type w) (m : Type u → Type v) (β : Type u) :
 
 def monad_cont.goto {α β} {m : Type u → Type v} (f : monad_cont.label α m β) (x : α) := f.apply x
 
-class monad_cont (m : Type u → Type v)
-extends monad m :=
+class monad_cont (m : Type u → Type v) :=
 (call_cc : Π {α β}, ((monad_cont.label α m β) → m α) → m α)
 
 open monad_cont
 
-class is_lawful_monad_cont (m : Type u → Type v) [monad_cont m]
+class is_lawful_monad_cont (m : Type u → Type v) [monad m] [monad_cont m]
 extends is_lawful_monad m :=
 (call_cc_bind_right {α ω γ} (cmd : m α) (next : (label ω m γ) → α → m ω) :
   call_cc (λ f, cmd >>= next f) = cmd >>= λ x, call_cc (λ f, next f x))
@@ -36,6 +36,8 @@ export is_lawful_monad_cont
 
 def cont_t (r : Type u) (m : Type u → Type v) (α : Type w) := (α → m r) → m r
 
+@[reducible] def cont (r : Type u) (α : Type w) := cont_t r id α
+
 namespace cont_t
 
 export monad_cont (label goto)
@@ -55,6 +57,11 @@ def with_cont_t (f : (β → m r) → α → m r) (x : cont_t r m α) : cont_t r
 lemma run_with_cont_t (f : (β → m r) → α → m r) (x : cont_t r m α) :
   run (with_cont_t f x) = run x ∘ f := rfl
 
+@[extensionality]
+protected lemma ext {x y : cont_t r m α}
+  (h : ∀ f, x.run f = y.run f) :
+  x = y := by { ext; apply h }
+
 instance : monad (cont_t r m) :=
 { pure := λ α x f, f x,
   bind := λ α β x f g, x $ λ i, f i g }
@@ -64,12 +71,15 @@ instance : is_lawful_monad (cont_t r m) :=
   pure_bind := by { intros, ext, refl },
   bind_assoc := by { intros, ext, refl } }
 
+def cont_t.monad_lift [monad m] {α} : m α → cont_t r m α :=
+λ x f, x >>= f
+
 instance [monad m] : has_monad_lift m (cont_t r m) :=
-{ monad_lift := λ a x f, x >>= f }
+{ monad_lift := λ α, cont_t.monad_lift }
 
 lemma monad_lift_bind [monad m] [is_lawful_monad m] {α β} (x : m α) (f : α → m β) :
   (monad_lift (x >>= f) : cont_t r m β) = monad_lift x >>= monad_lift ∘ f :=
-by { ext, simp only [monad_lift,has_monad_lift.monad_lift,(∘),(>>=),bind_assoc,id.def] }
+by { ext, simp only [monad_lift,has_monad_lift.monad_lift,(∘),(>>=),bind_assoc,id.def,run,cont_t.monad_lift] }
 
 instance : monad_cont (cont_t r m) :=
 { call_cc := λ α β f g, f ⟨λ x h, g x⟩ g }
@@ -79,4 +89,93 @@ instance : is_lawful_monad_cont (cont_t r m) :=
   call_cc_bind_left := by intros; ext; refl,
   call_cc_dummy := by intros; ext; refl }
 
+instance (ε) [monad_except ε m] : monad_except ε (cont_t r m) :=
+{ throw := λ x e f, throw e,
+  catch := λ α act h f, catch (act f) (λ e, h e f) }
+
+instance : monad_run (λ α, (α → m r) → ulift.{u v} (m r)) (cont_t.{u v u} r m) :=
+{ run := λ α f x, ⟨ f x ⟩ }
+
 end cont_t
+
+variables {m : Type u → Type v} [monad m]
+
+def except_t.mk_label {α β ε} : label (except.{u u} ε α) m β → label α (except_t ε m) β
+| ⟨ f ⟩ := ⟨ λ a, monad_lift $ f (except.ok a) ⟩
+
+lemma except_t.goto_mk_label {α β ε : Type*} (x : label (except.{u u} ε α) m β) (i : α) :
+  goto (except_t.mk_label x) i = ⟨ except.ok <$> goto x (except.ok i) ⟩ := by cases x; refl
+
+def except_t.call_cc {ε} [monad_cont m] {α β : Type*} (f : label α (except_t ε m) β → except_t ε m α) : except_t ε m α :=
+except_t.mk (call_cc $ λ x : label _ m β, except_t.run $ f (except_t.mk_label x) : m (except ε α))
+
+instance {ε} [monad_cont m] : monad_cont (except_t ε m) :=
+{ call_cc := λ α β, except_t.call_cc }
+
+instance {ε} [monad_cont m] [is_lawful_monad_cont m] : is_lawful_monad_cont (except_t ε m) :=
+{ call_cc_bind_right := by { intros, simp [call_cc,except_t.call_cc,call_cc_bind_right], ext, dsimp, congr, ext ⟨ ⟩; simp [except_t.bind_cont,@call_cc_dummy m _], },
+  call_cc_bind_left  := by { intros, simp [call_cc,except_t.call_cc,call_cc_bind_right,except_t.goto_mk_label,map_eq_bind_pure_comp,bind_assoc,@call_cc_bind_left m _], ext, refl },
+  call_cc_dummy := by { intros, simp [call_cc,except_t.call_cc,@call_cc_dummy m _], ext, refl }, }
+
+def option_t.mk_label {α β} : label (option.{u} α) m β → label α (option_t m) β
+| ⟨ f ⟩ := ⟨ λ a, monad_lift $ f (some a) ⟩
+
+lemma option_t.goto_mk_label {α β : Type*} (x : label (option.{u} α) m β) (i : α) :
+  goto (option_t.mk_label x) i = ⟨ some <$> goto x (some i) ⟩ := by cases x; refl
+
+def option_t.call_cc [monad_cont m] {α β : Type*} (f : label α (option_t m) β → option_t m α) : option_t m α :=
+option_t.mk (call_cc $ λ x : label _ m β, option_t.run $ f (option_t.mk_label x) : m (option α))
+
+instance [monad_cont m] : monad_cont (option_t m) :=
+{ call_cc := λ α β, option_t.call_cc }
+
+instance [monad_cont m] [is_lawful_monad_cont m] : is_lawful_monad_cont (option_t m) :=
+{ call_cc_bind_right := by { intros, simp [call_cc,option_t.call_cc,call_cc_bind_right], ext, dsimp, congr, ext ⟨ ⟩; simp [option_t.bind_cont,@call_cc_dummy m _], },
+  call_cc_bind_left  := by { intros, simp [call_cc,option_t.call_cc,call_cc_bind_right,option_t.goto_mk_label,map_eq_bind_pure_comp,bind_assoc,@call_cc_bind_left m _], ext, refl },
+  call_cc_dummy := by { intros, simp [call_cc,option_t.call_cc,@call_cc_dummy m _], ext, refl }, }
+
+def writer_t.mk_label {α β ω} [has_one ω] : label (α × ω) m β → label α (writer_t ω m) β
+| ⟨ f ⟩ := ⟨ λ a, monad_lift $ f (a,1) ⟩
+
+lemma writer_t.goto_mk_label {α β ω : Type*} [has_one ω] (x : label (α × ω) m β) (i : α) :
+  goto (writer_t.mk_label x) i = monad_lift (goto x (i,1)) := by cases x; refl
+
+def writer_t.call_cc [monad_cont m] {α β ω : Type*} [has_one ω] (f : label α (writer_t ω m) β → writer_t ω m α) : writer_t ω m α :=
+⟨ call_cc (writer_t.run ∘ f ∘ writer_t.mk_label : label (α × ω) m β → m (α × ω)) ⟩
+
+instance (ω) [monad m] [has_one ω] [monad_cont m] : monad_cont (writer_t ω m) :=
+{ call_cc := λ α β, writer_t.call_cc }
+
+def state_t.mk_label {α β σ : Type u} : label (α × σ) m (β × σ) → label α (state_t σ m) β
+| ⟨ f ⟩ := ⟨ λ a, ⟨ λ s, f (a,s) ⟩ ⟩
+
+lemma state_t.goto_mk_label {α β σ : Type u} (x : label (α × σ) m (β × σ)) (i : α) :
+  goto (state_t.mk_label x) i = ⟨ λ s, (goto x (i,s)) ⟩ := by cases x; refl
+
+def state_t.call_cc {σ}  [monad_cont m] {α β : Type*} (f : label α (state_t σ m) β → state_t σ m α) : state_t σ m α :=
+⟨ λ r, call_cc (λ f', (f $ state_t.mk_label f').run r) ⟩
+
+instance {σ} [monad_cont m] : monad_cont (state_t σ m) :=
+{ call_cc := λ α β, state_t.call_cc }
+
+instance {σ} [monad_cont m] [is_lawful_monad_cont m] : is_lawful_monad_cont (state_t σ m) :=
+{ call_cc_bind_right := by { intros, simp [call_cc,state_t.call_cc,call_cc_bind_right,(>>=),state_t.bind], ext, dsimp, congr, ext ⟨x₀,x₁⟩, refl },
+  call_cc_bind_left  := by { intros, simp [call_cc,state_t.call_cc,call_cc_bind_left,(>>=),state_t.bind,state_t.goto_mk_label], ext, refl },
+  call_cc_dummy := by { intros, simp [call_cc,state_t.call_cc,call_cc_bind_right,(>>=),state_t.bind,@call_cc_dummy m _], ext, refl }, }
+
+def reader_t.mk_label {α β} (ρ) : label α m β → label α (reader_t ρ m) β
+| ⟨ f ⟩ := ⟨ monad_lift ∘ f ⟩
+
+lemma reader_t.goto_mk_label {α ρ β} (x : label α m β) (i : α) :
+  goto (reader_t.mk_label ρ x) i = monad_lift (goto x i) := by cases x; refl
+
+def reader_t.call_cc {ε}  [monad_cont m] {α β : Type*} (f : label α (reader_t ε m) β → reader_t ε m α) : reader_t ε m α :=
+⟨ λ r, call_cc (λ f', (f $ reader_t.mk_label _ f').run r) ⟩
+
+instance {ρ} [monad_cont m] : monad_cont (reader_t ρ m) :=
+{ call_cc := λ α β, reader_t.call_cc }
+
+instance {ρ} [monad_cont m] [is_lawful_monad_cont m] : is_lawful_monad_cont (reader_t ρ m) :=
+{ call_cc_bind_right := by { intros, simp [call_cc,reader_t.call_cc,call_cc_bind_right], ext, refl },
+  call_cc_bind_left  := by { intros, simp [call_cc,reader_t.call_cc,call_cc_bind_left,reader_t.goto_mk_label], ext, refl },
+  call_cc_dummy := by { intros, simp [call_cc,reader_t.call_cc,@call_cc_dummy m _], ext, refl } }

src/category/monad/writer.lean

@@ -0,0 +1,159 @@
+
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Simon Hudon
+
+The writer monad transformer for passing immutable state.
+-/
+
+import tactic.interactive category.monad.basic
+universes u v w
+
+structure writer_t (ω : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
+(run : m (α × ω))
+
+@[reducible] def writer (ω : Type u) := writer_t ω id
+
+attribute [pp_using_anonymous_constructor] writer_t
+
+namespace writer_t
+section
+  variable  {ω : Type u}
+  variable  {m : Type u → Type v}
+  variable  [monad m]
+  variables {α β : Type u}
+  open function
+
+  @[extensionality]
+  protected lemma ext (x x' : writer_t ω m α)
+    (h : x.run = x'.run) :
+    x = x' := by cases x; cases x'; congr; apply h
+
+  @[inline] protected def tell (w : ω) : writer_t ω m punit :=
+  ⟨pure (punit.star, w)⟩
+
+  @[inline] protected def listen : writer_t ω m α → writer_t ω m (α × ω)
+  | ⟨ cmd ⟩ := ⟨ (λ x : α × ω, ((x.1,x.2),x.2)) <$> cmd ⟩
+
+  @[inline] protected def pass : writer_t ω m (α × (ω → ω)) → writer_t ω m α
+  | ⟨ cmd ⟩ := ⟨ uncurry (uncurry $ λ x (f : ω → ω) w, (x,f w)) <$> cmd ⟩
+
+  @[inline] protected def pure [has_one ω] (a : α) : writer_t ω m α :=
+  ⟨ pure (a,1) ⟩
+
+  @[inline] protected def bind [has_mul ω] (x : writer_t ω m α) (f : α → writer_t ω m β) : writer_t ω m β :=
+  ⟨ do x  ← x.run,
+       x' ← (f x.1).run,
+       pure (x'.1,x.2 * x'.2) ⟩
+
+  instance [has_one ω] [has_mul ω] : monad (writer_t ω m) :=
+  { pure := λ α, writer_t.pure, bind := λ α β, writer_t.bind }
+
+  instance [monoid ω] [is_lawful_monad m] : is_lawful_monad (writer_t ω m) :=
+  { id_map := by { intros, cases x, simp [(<$>),writer_t.bind,writer_t.pure] },
+    pure_bind := by { intros, simp [has_pure.pure,writer_t.pure,(>>=),writer_t.bind], ext; refl },
+    bind_assoc := by { intros, simp [(>>=),writer_t.bind,mul_assoc] with functor_norm } }
+
+  @[inline] protected def lift [has_one ω] (a : m α) : writer_t ω m α :=
+  ⟨ flip prod.mk 1 <$> a ⟩
+
+  instance (m) [monad m] [has_one ω] : has_monad_lift m (writer_t ω m) :=
+  ⟨ λ α, writer_t.lift  ⟩
+
+  @[inline] protected def monad_map {m m'} [monad m] [monad m'] {α} (f : Π {α}, m α → m' α) : writer_t ω m α → writer_t ω m' α :=
+  λ x, ⟨ f x.run ⟩
+
+  instance (m m') [monad m] [monad m'] : monad_functor m m' (writer_t ω m) (writer_t ω m') :=
+  ⟨@writer_t.monad_map ω m m' _ _⟩
+
+  @[inline] protected def adapt {ω' : Type u} [monad m] {α : Type u} (f : ω → ω') : writer_t ω m α → writer_t ω' m α :=
+  λ x, ⟨prod.map id f <$> x.run⟩
+
+  instance (ε) [has_one ω] [monad m] [monad_except ε m] : monad_except ε (writer_t ω m) :=
+  { throw := λ α, writer_t.lift ∘ throw,
+    catch := λ α x c, ⟨catch x.run (λ e, (c e).run)⟩ }
+end
+end writer_t
+
+
+/-- An implementation of [MonadReader](https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Reader-Class.html#t:MonadReader).
+    It does not contain `local` because this function cannot be lifted using `monad_lift`.
+    Instead, the `monad_reader_adapter` class provides the more general `adapt_reader` function.
+
+    Note: This class can be seen as a simplification of the more "principled" definition
+    ```
+    class monad_reader (ρ : out_param (Type u)) (n : Type u → Type u) :=
+    (lift {} {α : Type u} : (∀ {m : Type u → Type u} [monad m], reader_t ρ m α) → n α)
+    ```
+    -/
+class monad_writer (ω : out_param (Type u)) (m : Type u → Type v) :=
+(tell {} (w : ω) : m punit)
+(listen {α} : m α → m (α × ω))
+(pass {α : Type u} : m (α × (ω → ω)) → m α)
+
+export monad_writer
+
+instance {ω : Type u} {m : Type u → Type v} [monad m] : monad_writer ω (writer_t ω m) :=
+{ tell := writer_t.tell,
+  listen := λ α, writer_t.listen,
+  pass := λ α, writer_t.pass }
+
+instance {ω ρ : Type u} {m : Type u → Type v} [monad m] [monad_writer ω m] : monad_writer ω (reader_t ρ m) :=
+{ tell := λ x, monad_lift (tell x : m punit),
+  listen := λ α ⟨ cmd ⟩, ⟨ λ r, listen (cmd r) ⟩,
+  pass := λ α ⟨ cmd ⟩, ⟨ λ r, pass (cmd r) ⟩ }
+
+def swap_right {α β γ} : (α × β) × γ → (α × γ) × β
+| ⟨⟨x,y⟩,z⟩ := ((x,z),y)
+
+instance {ω σ : Type u} {m : Type u → Type v} [monad m] [monad_writer ω m] : monad_writer ω (state_t σ m) :=
+{ tell := λ x, monad_lift (tell x : m punit),
+  listen := λ α ⟨ cmd ⟩, ⟨ λ r, swap_right <$> listen (cmd r) ⟩,
+  pass := λ α ⟨ cmd ⟩, ⟨ λ r, pass (swap_right <$> cmd r) ⟩ }
+open function
+
+def except_t.pass_aux {ε α ω} : except ε (α × (ω → ω)) → except ε α × (ω → ω)
+| (except.error a) := (except.error a,id)
+| (except.ok (x,y)) := (except.ok x,y)
+
+instance {ω ε : Type u} {m : Type u → Type v} [monad m] [monad_writer ω m] : monad_writer ω (except_t ε m) :=
+{ tell := λ x, monad_lift (tell x : m punit),
+  listen := λ α ⟨ cmd ⟩, ⟨ uncurry (λ x y, flip prod.mk y <$> x) <$> listen cmd ⟩,
+  pass := λ α ⟨ cmd ⟩, ⟨ pass (except_t.pass_aux <$> cmd) ⟩ }
+
+def option_t.pass_aux {α ω} : option (α × (ω → ω)) → option α × (ω → ω)
+| none := (none ,id)
+| (some (x,y)) := (some x,y)
+
+instance {ω : Type u} {m : Type u → Type v} [monad m] [monad_writer ω m] : monad_writer ω (option_t m) :=
+{ tell := λ x, monad_lift (tell x : m punit),
+  listen := λ α ⟨ cmd ⟩, ⟨ uncurry (λ x y, flip prod.mk y <$> x) <$> listen cmd ⟩,
+  pass := λ α ⟨ cmd ⟩, ⟨ pass (option_t.pass_aux <$> cmd) ⟩ }
+
+/-- Adapt a monad stack, changing the type of its top-most environment.
+
+    This class is comparable to [Control.Lens.Magnify](https://hackage.haskell.org/package/lens-4.15.4/docs/Control-Lens-Zoom.html#t:Magnify), but does not use lenses (why would it), and is derived automatically for any transformer implementing `monad_functor`.
+
+    Note: This class can be seen as a simplification of the more "principled" definition
+    ```
+    class monad_reader_functor (ρ ρ' : out_param (Type u)) (n n' : Type u → Type u) :=
+    (map {} {α : Type u} : (∀ {m : Type u → Type u} [monad m], reader_t ρ m α → reader_t ρ' m α) → n α → n' α)
+    ```
+    -/
+class monad_writer_adapter (ω ω' : out_param (Type u)) (m m' : Type u → Type v) :=
+(adapt_writer {} {α : Type u} : (ω → ω') → m α → m' α)
+export monad_writer_adapter (adapt_writer)
+
+section
+variables {ω ω' : Type u} {m m' : Type u → Type v}
+
+instance monad_writer_adapter_trans {n n' : Type u → Type v} [monad_functor m m' n n'] [monad_writer_adapter ω ω' m m'] : monad_writer_adapter ω ω' n n' :=
+⟨λ α f, monad_map (λ α, (adapt_writer f : m α → m' α))⟩
+
+instance [monad m] : monad_writer_adapter ω ω' (writer_t ω m) (writer_t ω' m) :=
+⟨λ α, writer_t.adapt⟩
+end
+
+instance (ω : Type u) (m out) [monad_run out m] : monad_run (λ α, out (α × ω)) (writer_t ω m) :=
+⟨λ α x, run $ x.run ⟩