/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon, E.W.Ayers
-/
import Mathlib.Algebra.Group.Defs

/-!
# Writer monads

This file introduces monads for managing immutable, appendable state.
Common applications are logging monads where the monad logs messages as the
computation progresses.

## References
- https://hackage.haskell.org/package/mtl-2.2.1/docs/Control-Monad-Writer-Class.html
- [Original Mark P Jones article introducing `Writer`](https://web.cecs.pdx.edu/~mpj/pubs/springschool.html)

-/

def 
WriterT: Type u → (Type u → Type v) → Type u → Type v
WriterT (
ω: Type u
ω : 
Type u: Type (u+1)
Type u) (
M: Type u → Type v
M : 
Type u: Type (u+1)
Type u → 
Type v: Type (v+1)
Type v) (
α: Type u
α : 
Type u: Type (u+1)
Type u) : 
Type v: Type (v+1)
Type v :=
  
M: Type u → Type v
M (
α: Type u
α × 
ω: Type u
ω)

@[reducible]
def 
Writer: Type u_1 → Type u_1 → Type u_1
Writer 
ω: ?m.28
ω := 
WriterT: Type ?u.36 → (Type ?u.36 → Type ?u.35) → Type ?u.36 → Type ?u.35
WriterT 
ω: ?m.28
ω 
Id: Type ?u.41 → Type ?u.41
Id

class 
MonadWriter: outParam (Type u) → (Type u → Type v) → Type (max(u+1)v)
MonadWriter (
ω: outParam (Type u)
ω : 
outParam: Sort ?u.51 → Sort ?u.51
outParam (
Type u: Type (u+1)
Type u)) (
M: Type u → Type v
M : 
Type u: Type (u+1)
Type u → 
Type v: Type (v+1)
Type v) where
  
tell: {ω : outParam (Type u)} → {M : Type u → Type v} → [self : MonadWriter ω M] → ω → M PUnit
tell : 
ω: outParam (Type u)
ω → 
M: Type u → Type v
M 
PUnit: Sort ?u.62
PUnit
  
listen: {ω : outParam (Type u)} → {M : Type u → Type v} → [self : MonadWriter ω M] → {α : Type u} → M α → M (α × ω)
listen {
α: ?m.65
α} : 
M: Type u → Type v
M 
α: ?m.65
α → 
M: Type u → Type v
M (
α: ?m.65
α × 
ω: outParam (Type u)
ω)
  
pass: {ω : outParam (Type u)} → {M : Type u → Type v} → [self : MonadWriter ω M] → {α : Type u} → M (α × (ω → ω)) → M α
pass {
α: ?m.74
α} : 
M: Type u → Type v
M (
α: ?m.74
α × (
ω: outParam (Type u)
ω → 
ω: outParam (Type u)
ω)) → 
M: Type u → Type v
M 
α: ?m.74
α

export MonadWriter (tell listen pass)

variable {
M: Type u → Type v
M : 
Type u: Type (u+1)
Type u → 
Type v: Type (v+1)
Type v} [
Monad: (Type ?u.96 → Type ?u.95) → Type (max(?u.96+1)?u.95)
Monad 
M: Type u → Type v
M]

instance: {M : Type u → Type v} → {ω ρ : Type u} → [inst : MonadWriter ω M] → MonadWriter ω (ReaderT ρ M)
instance [
MonadWriter: outParam (Type ?u.137) → (Type ?u.137 → Type ?u.136) → Type (max(?u.137+1)?u.136)
MonadWriter 
ω: ?m.116
ω 
M: Type u → Type v
M] : 
MonadWriter: outParam (Type ?u.144) → (Type ?u.144 → Type ?u.143) → Type (max(?u.144+1)?u.143)
MonadWriter 
ω: ?m.116
ω (
ReaderT: Type ?u.146 → (Type ?u.146 → Type ?u.145) → Type ?u.146 → Type (max?u.146?u.145)
ReaderT 
ρ: ?m.133
ρ 
M: Type u → Type v
M) where
  tell 
w: ?m.168
w :=  (
tell: {ω : outParam (Type ?u.173)} → {M : Type ?u.173 → Type ?u.172} → [self : MonadWriter ω M] → ω → M PUnit
tell 
w: ?m.168
w : 
M: Type u → Type v
M 
_: Type u
_)
  listen 
x: ?m.259
x 
r: ?m.262
r := 
listen: {ω : outParam (Type ?u.265)} →
  {M : Type ?u.265 → Type ?u.264} → [self : MonadWriter ω M] → {α : Type ?u.265} → M α → M (α × ω)
listen <| 
x: ?m.259
x 
r: ?m.262
r
  pass 
x: ?m.288
x 
r: ?m.291
r := 
pass: {ω : outParam (Type ?u.294)} →
  {M : Type ?u.294 → Type ?u.293} → [self : MonadWriter ω M] → {α : Type ?u.294} → M (α × (ω → ω)) → M α
pass <| 
x: ?m.288
x 
r: ?m.291
r

instance: {M : Type u → Type v} → [inst : Monad M] → {ω σ : Type u} → [inst : MonadWriter ω M] → MonadWriter ω (StateT σ M)
instance [
MonadWriter: outParam (Type ?u.701) → (Type ?u.701 → Type ?u.700) → Type (max(?u.701+1)?u.700)
MonadWriter 
ω: ?m.680
ω 
M: Type u → Type v
M] : 
MonadWriter: outParam (Type ?u.708) → (Type ?u.708 → Type ?u.707) → Type (max(?u.708+1)?u.707)
MonadWriter 
ω: ?m.680
ω (
StateT: Type ?u.710 → (Type ?u.710 → Type ?u.709) → Type ?u.710 → Type (max?u.710?u.709)
StateT 
σ: ?m.697
σ 
M: Type u → Type v
M) where
  tell 
w: ?m.732
w := (
tell: {ω : outParam (Type ?u.737)} → {M : Type ?u.737 → Type ?u.736} → [self : MonadWriter ω M] → ω → M PUnit
tell 
w: ?m.732
w : 
M: Type u → Type v
M 
_: Type u
_)
  listen 
x: ?m.832
x 
s: ?m.835
s := (fun ((
a: α✝
a,
w: σ
w), 
s: ω
s) ↦ ((
a: α✝
a,
s: ω
s), 
w: σ
w)) <$> 
listen: {ω : outParam (Type ?u.862)} →
  {M : Type ?u.862 → Type ?u.861} → [self : MonadWriter ω M] → {α : Type ?u.862} → M α → M (α × ω)
listen (
x: ?m.832
x 
s: ?m.835
s)
  pass 
x: ?m.913
x 
s: ?m.916
s := 
pass: {ω : outParam (Type ?u.919)} →
  {M : Type ?u.919 → Type ?u.918} → [self : MonadWriter ω M] → {α : Type ?u.919} → M (α × (ω → ω)) → M α
pass <| (fun ((
a: α✝
a, 
f: ω → ω
f), 
s: σ
s) ↦ ((
a: α✝
a, 
s: σ
s), 
f: ω → ω
f)) <$> (
x: ?m.913
x 
s: ?m.916
s)

namespace WriterT

protected def 
mk: {M : Type u → Type v} → {α ω : Type u} → M (α × ω) → WriterT ω M α
mk {
ω: Type u
ω : 
Type u: Type (u+1)
Type u} (
cmd: M (α × ω)
cmd :  
M: Type u → Type v
M (
α: ?m.2118
α × 
ω: Type u
ω)) : 
WriterT: Type ?u.2128 → (Type ?u.2128 → Type ?u.2127) → Type ?u.2128 → Type ?u.2127
WriterT 
ω: Type u
ω 
M: Type u → Type v
M 
α: ?m.2118
α:= 
cmd: M (α × ω)
cmd
protected def 
run: {α ω : Type u} → WriterT ω M α → M (α × ω)
run {
ω: Type u
ω : 
Type u: Type (u+1)
Type u} (
cmd: WriterT ω M α
cmd : 
WriterT: Type ?u.2222 → (Type ?u.2222 → Type ?u.2221) → Type ?u.2222 → Type ?u.2221
WriterT 
ω: Type u
ω 
M: Type u → Type v
M 
α: ?m.2216
α) : 
M: Type u → Type v
M (
α: ?m.2216
α × 
ω: Type u
ω) := 
cmd: WriterT ω M α
cmd
protected def 
runThe: {α : Type u} → (ω : Type u) → WriterT ω M α → M (α × ω)
runThe (
ω: Type u
ω : 
Type u: Type (u+1)
Type u) (
cmd: WriterT ω M α
cmd : 
WriterT: Type ?u.2321 → (Type ?u.2321 → Type ?u.2320) → Type ?u.2321 → Type ?u.2320
WriterT 
ω: Type u
ω 
M: Type u → Type v
M 
α: ?m.2315
α) : 
M: Type u → Type v
M (
α: ?m.2315
α × 
ω: Type u
ω) := 
cmd: WriterT ω M α
cmd

variable {
ω: Type u
ω : 
Type u: Type (u+1)
Type u} {
α: Type u
α 
β: Type u
β : 
Type u: Type (u+1)
Type u}

/-- Creates an instance of Monad, with an explicitly given empty and append operation.

Previously, this would have used an instance of `[Monoid ω]` as input.
In practice, however, WriterT is used for logging and creating lists so restricting to
monoids with `Mul` and `One` can make `WriterT` cumbersome to use.

This is used to derive instances for both `[EmptyCollection ω] [Append ω]` and `[Monoid ω]`.
-/
def 
monad: ω → (ω → ω → ω) → Monad (WriterT ω M)
monad (
empty: ω
empty : 
ω: Type u
ω) (
append: ω → ω → ω
append : 
ω: Type u
ω → 
ω: Type u
ω → 
ω: Type u
ω) : 
Monad: (Type ?u.2438 → Type ?u.2437) → Type (max(?u.2438+1)?u.2437)
Monad (
WriterT: Type ?u.2440 → (Type ?u.2440 → Type ?u.2439) → Type ?u.2440 → Type ?u.2439
WriterT 
ω: Type u
ω 
M: Type u → Type v
M) where
  map := fun 
f: ?m.2473
f (
cmd: M ?m.2477
cmd : 
M: Type u → Type v
M 
_: Type u
_) ↦ 
WriterT.mk: {M : Type ?u.2481 → Type ?u.2480} → {α ω : Type ?u.2481} → M (α × ω) → WriterT ω M α
WriterT.mk $ (fun (
a: α✝
a,
w: ω
w) ↦ (
f: ?m.2473
f 
a: α✝
a, 
w: ω
w)) <$> 
cmd: M ?m.2477
cmd
  pure := fun 
a: ?m.2561
a ↦ 
pure: {f : Type ?u.2564 → Type ?u.2563} → [self : Pure f] → {α : Type ?u.2564} → α → f α
pure (f := 
M: Type u → Type v
M) (
a: ?m.2561
a, 
empty: ω
empty)
  bind := fun (
cmd: M ?m.2684
cmd : 
M: Type u → Type v
M 
_: Type u
_) 
f: ?m.2687
f ↦
    
WriterT.mk: {M : Type ?u.2692 → Type ?u.2691} → {α ω : Type ?u.2692} → M (α × ω) → WriterT ω M α
WriterT.mk $ 
cmd: M ?m.2684
cmd >>= fun (
a: α✝
a, 
w₁: ω
w₁) ↦
      (fun (
b: β✝
b, 
w₂: ω
w₂) ↦ (
b: β✝
b, 
append: ω → ω → ω
append 
w₁: ω
w₁ 
w₂: ω
w₂)) <$> (
f: ?m.2687
f 
a: α✝
a)

/-- Lift an `M` to a `WriterT ω M`, using the given `empty` as the monoid unit. -/
protected def 
liftTell: ω → MonadLift M (WriterT ω M)
liftTell (
empty: ω
empty : 
ω: Type u
ω) : 
MonadLift: semiOutParam (Type ?u.4437 → Type ?u.4436) →
  (Type ?u.4437 → Type ?u.4435) → Type (max(max(?u.4437+1)?u.4436)?u.4435)
MonadLift 
M: Type u → Type v
M (
WriterT: Type ?u.4442 → (Type ?u.4442 → Type ?u.4441) → Type ?u.4442 → Type ?u.4441
WriterT 
ω: Type u
ω 
M: Type u → Type v
M) where
  monadLift := fun 
cmd: ?m.4467
cmd ↦ 
WriterT.mk: {M : Type ?u.4470 → Type ?u.4469} → {α ω : Type ?u.4470} → M (α × ω) → WriterT ω M α
WriterT.mk $ (fun 
a: ?m.4497
a ↦ (
a: ?m.4497
a, 
empty: ω
empty)) <$> 
cmd: ?m.4467
cmd

instance: {M : Type u → Type v} →
  [inst : Monad M] → {ω : Type u} → [inst : EmptyCollection ω] → [inst : Append ω] → Monad (WriterT ω M)
instance [
EmptyCollection: Type ?u.4646 → Type ?u.4646
EmptyCollection 
ω: Type u
ω] [
Append: Type ?u.4649 → Type ?u.4649
Append 
ω: Type u
ω] : 
Monad: (Type ?u.4653 → Type ?u.4652) → Type (max(?u.4653+1)?u.4652)
Monad (
WriterT: Type ?u.4655 → (Type ?u.4655 → Type ?u.4654) → Type ?u.4655 → Type ?u.4654
WriterT 
ω: Type u
ω 
M: Type u → Type v
M) := 
monad: {M : Type ?u.4668 → Type ?u.4667} → [inst : Monad M] → {ω : Type ?u.4668} → ω → (ω → ω → ω) → Monad (WriterT ω M)
monad 
∅: ?m.4702
∅ 
(· ++ ·): ω → ω → ω
(· ++ ·)
instance: {M : Type u → Type v} → [inst : Monad M] → {ω : Type u} → [inst : EmptyCollection ω] → MonadLift M (WriterT ω M)
instance [
EmptyCollection: Type ?u.4920 → Type ?u.4920
EmptyCollection 
ω: Type u
ω] : 
MonadLift: semiOutParam (Type ?u.4925 → Type ?u.4924) →
  (Type ?u.4925 → Type ?u.4923) → Type (max(max(?u.4925+1)?u.4924)?u.4923)
MonadLift 
M: Type u → Type v
M (
WriterT: Type ?u.4930 → (Type ?u.4930 → Type ?u.4929) → Type ?u.4930 → Type ?u.4929
WriterT 
ω: Type u
ω 
M: Type u → Type v
M) := 
WriterT.liftTell: {M : Type ?u.4942 → Type ?u.4941} → [inst : Monad M] → {ω : Type ?u.4942} → ω → MonadLift M (WriterT ω M)
WriterT.liftTell 
∅: ?m.4981
∅
instance: {M : Type u → Type v} → [inst : Monad M] → {ω : Type u} → [inst : Monoid ω] → Monad (WriterT ω M)
instance [
Monoid: Type ?u.5111 → Type ?u.5111
Monoid 
ω: Type u
ω] : 
Monad: (Type ?u.5115 → Type ?u.5114) → Type (max(?u.5115+1)?u.5114)
Monad (
WriterT: Type ?u.5117 → (Type ?u.5117 → Type ?u.5116) → Type ?u.5117 → Type ?u.5116
WriterT 
ω: Type u
ω 
M: Type u → Type v
M) := 
monad: {M : Type ?u.5129 → Type ?u.5128} → [inst : Monad M] → {ω : Type ?u.5129} → ω → (ω → ω → ω) → Monad (WriterT ω M)
monad 
1: ?m.5165
1 
(· * ·): ω → ω → ω
(· * ·)
instance: {M : Type u → Type v} → [inst : Monad M] → {ω : Type u} → [inst : Monoid ω] → MonadLift M (WriterT ω M)
instance [
Monoid: Type ?u.5470 → Type ?u.5470
Monoid 
ω: Type u
ω] : 
MonadLift: semiOutParam (Type ?u.5475 → Type ?u.5474) →
  (Type ?u.5475 → Type ?u.5473) → Type (max(max(?u.5475+1)?u.5474)?u.5473)
MonadLift 
M: Type u → Type v
M (
WriterT: Type ?u.5480 → (Type ?u.5480 → Type ?u.5479) → Type ?u.5480 → Type ?u.5479
WriterT 
ω: Type u
ω 
M: Type u → Type v
M) := 
WriterT.liftTell: {M : Type ?u.5492 → Type ?u.5491} → [inst : Monad M] → {ω : Type ?u.5492} → ω → MonadLift M (WriterT ω M)
WriterT.liftTell 
1: ?m.5533
1

instance: {M : Type u → Type v} → [inst : Monad M] → {ω : Type u} → MonadWriter ω (WriterT ω M)
instance : 
MonadWriter: outParam (Type ?u.5700) → (Type ?u.5700 → Type ?u.5699) → Type (max(?u.5700+1)?u.5699)
MonadWriter 
ω: Type u
ω (
WriterT: Type ?u.5702 → (Type ?u.5702 → Type ?u.5701) → Type ?u.5702 → Type ?u.5701
WriterT 
ω: Type u
ω 
M: Type u → Type v
M) where
  tell := fun 
w: ?m.5721
w ↦ 
WriterT.mk: {M : Type ?u.5724 → Type ?u.5723} → {α ω : Type ?u.5724} → M (α × ω) → WriterT ω M α
WriterT.mk $ 
pure: {f : Type ?u.5734 → Type ?u.5733} → [self : Pure f] → {α : Type ?u.5734} → α → f α
pure (
⟨⟩: PUnit
⟨⟩, 
w: ?m.5721
w)
  listen := fun 
cmd: ?m.5799
cmd ↦ 
WriterT.mk: {M : Type ?u.5802 → Type ?u.5801} → {α ω : Type ?u.5802} → M (α × ω) → WriterT ω M α
WriterT.mk $ (fun (
a: α✝
a,
w: ω
w) ↦ ((
a: α✝
a,
w: ω
w), 
w: ω
w)) <$> 
cmd: ?m.5799
cmd
  pass := fun 
cmd: ?m.5862
cmd ↦ 
WriterT.mk: {M : Type ?u.5865 → Type ?u.5864} → {α ω : Type ?u.5865} → M (α × ω) → WriterT ω M α
WriterT.mk $ (fun ((
a: α✝
a,
f: ω → ω
f), 
w: ω
w) ↦ (
a: α✝
a, 
f: ω → ω
f 
w: ω
w)) <$> 
cmd: ?m.5862
cmd

instance: {M : Type u → Type v} → {ω : Type u} → {ε : Type u_1} → [inst : MonadExcept ε M] → MonadExcept ε (WriterT ω M)
instance [
MonadExcept: outParam (Type ?u.6660) → (Type ?u.6659 → Type ?u.6658) → Type (max(max?u.6660(?u.6659+1))?u.6658)
MonadExcept 
ε: ?m.6655
ε 
M: Type u → Type v
M] : 
MonadExcept: outParam (Type ?u.6668) → (Type ?u.6667 → Type ?u.6666) → Type (max(max?u.6668(?u.6667+1))?u.6666)
MonadExcept 
ε: ?m.6655
ε (
WriterT: Type ?u.6670 → (Type ?u.6670 → Type ?u.6669) → Type ?u.6670 → Type ?u.6669
WriterT 
ω: Type u
ω 
M: Type u → Type v
M) where
  throw := fun 
e: ?m.6693
e ↦ 
WriterT.mk: {M : Type ?u.6696 → Type ?u.6695} → {α ω : Type ?u.6696} → M (α × ω) → WriterT ω M α
WriterT.mk $ 
throw: {ε : outParam (Type ?u.6707)} →
  {m : Type ?u.6706 → Type ?u.6705} → [self : MonadExcept ε m] → {α : Type ?u.6706} → ε → m α
throw 
e: ?m.6693
e
  tryCatch := fun 
cmd: ?m.6737
cmd 
c: ?m.6740
c ↦ 
WriterT.mk: {M : Type ?u.6745 → Type ?u.6744} → {α ω : Type ?u.6745} → M (α × ω) → WriterT ω M α
WriterT.mk $ 
tryCatch: {ε : outParam (Type ?u.6752)} →
  {m : Type ?u.6751 → Type ?u.6750} → [self : MonadExcept ε m] → {α : Type ?u.6751} → m α → (ε → m α) → m α
tryCatch 
cmd: ?m.6737
cmd fun 
e: ?m.6767
e ↦ (
c: ?m.6740
c 
e: ?m.6767
e).
run: {M : Type ?u.6770 → Type ?u.6769} → {α ω : Type ?u.6770} → WriterT ω M α → M (α × ω)
run

instance: {M : Type u → Type v} → {ω : Type u} → [inst : MonadLiftT M (WriterT ω M)] → MonadControl M (WriterT ω M)
instance [
MonadLiftT: (Type ?u.7065 → Type ?u.7064) → (Type ?u.7065 → Type ?u.7063) → Type (max(max(?u.7065+1)?u.7064)?u.7063)
MonadLiftT 
M: Type u → Type v
M (
WriterT: Type ?u.7070 → (Type ?u.7070 → Type ?u.7069) → Type ?u.7070 → Type ?u.7069
WriterT 
ω: Type u
ω 
M: Type u → Type v
M)] : 
MonadControl: semiOutParam (Type ?u.7083 → Type ?u.7082) →
  (Type ?u.7083 → Type ?u.7081) → Type (max(max(?u.7083+1)?u.7082)?u.7081)
MonadControl 
M: Type u → Type v
M (
WriterT: Type ?u.7088 → (Type ?u.7088 → Type ?u.7087) → Type ?u.7088 → Type ?u.7087
WriterT 
ω: Type u
ω 
M: Type u → Type v
M) where
  stM := fun 
α: ?m.7112
α ↦ 
α: ?m.7112
α × 
ω: Type u
ω
  liftWith 
f: ?m.7120
f := 
liftM: {m : Type ?u.7127 → Type ?u.7126} →
  {n : Type ?u.7127 → Type ?u.7125} → [self : MonadLiftT m n] → {α : Type ?u.7127} → m α → n α
liftM <| 
f: ?m.7120
f fun 
x: ?m.7147
x ↦ 
x: ?m.7147
x.
run: {M : Type ?u.7150 → Type ?u.7149} → {α ω : Type ?u.7150} → WriterT ω M α → M (α × ω)
run
  restoreM := 
WriterT.mk: {M : Type ?u.7195 → Type ?u.7194} → {α ω : Type ?u.7195} → M (α × ω) → WriterT ω M α
WriterT.mk

instance: {M : Type u → Type v} → {ω : Type u} → MonadFunctor M (WriterT ω M)
instance : 
MonadFunctor: semiOutParam (Type ?u.7378 → Type ?u.7377) →
  (Type ?u.7378 → Type ?u.7376) → Type (max(max(?u.7378+1)?u.7377)?u.7376)
MonadFunctor 
M: Type u → Type v
M (
WriterT: Type ?u.7383 → (Type ?u.7383 → Type ?u.7382) → Type ?u.7383 → Type ?u.7382
WriterT 
ω: Type u
ω 
M: Type u → Type v
M) where
  monadMap := fun 
k: ?m.7407
k (
w: M ?m.7412
w : 
M: Type u → Type v
M 
_: Type u
_) ↦ 
WriterT.mk: {M : Type ?u.7416 → Type ?u.7415} → {α ω : Type ?u.7416} → M (α × ω) → WriterT ω M α
WriterT.mk $ 
k: ?m.7407
k 
w: M ?m.7412
w

end WriterT