Checking that a Monad instance is a Monad

Stream: new members

[Lars Ericson]

@David Thrane Christiansen, in this exercise in Functional Programming in Lean, you give an example

instance : Monad Option where
  pure x := some x
  bind opt next := none

Lean accepts this as a Monad instance, but this one violates the Monad contract, which is that

(bind (pure v) = f v ) ∧
(bind v pure = v ) ∧
(bind (bind v f) g  = bind v (fun x => bind (f x) g))

Lean being Lean, shouldn't these 3 properties be checked or require proof be supplied in order to instantiate a Monad? I don't see these three properties directly stated in the code for Monad:

class Monad (m : Type u → Type v) extends Applicative m, Bind m : Type (max (u+1) v) where
  map      f x := bind x (Function.comp pure f)
  seq      f x := bind f fun y => Functor.map y (x ())
  seqLeft  x y := bind x fun a => bind (y ()) (fun _ => pure a)
  seqRight x y := bind x fun _ => y ()

Should the Monad contract be in there so that incorrect instances can't be derived? Is the Monad contract somewhere else in the code? What should I know about separating understanding of Lean as a programming language and Lean as a theorem prover? Is there a crossover between programming and theorem proving that I'm expecting (the idea of programs which are derived in accordance with specifications) which is not actually part of the paradigm?

[Kyle Miller]

There's docs#LawfulMonad for recording that a monad is really a monad

[Kyle Miller]

I think the split between Monad and LawfulMonad is for the functional programming side of things. Another split for example is docs#BEq and docs#LawfulBEq for whether this equality operation actually captures substitution-invariance.

[David Thrane Christiansen]

What Kyle said is totally right - the Lean library provides a version of Monad that requires you to show that you follow the rules, and one that doesn't. I figured I'd supplement with why this exercise is the way it is.

The goal of this book is to be usable as a first introduction to functional programming. My guess is that it doesn't entirely succeed at this, but I really tried not to overwhelm and intimidate readers who haven't done these things before. The reason I chose to spend a fair bit of space on informally reasoning about monad laws, and the reason for this exercise, is to start getting people to start thinking in a way that is conducive to proving things, but that "feels" more like debugging a program.

In particular, I think it's important to learn informal reasoning about code before learning formal reasoning, because it helps reduce the risk of making a bit of progress by just hammering away with induction and simp, and then getting stuck as soon as something more is needed. I was once angrily told "Think before you hack!" in an oral exam by a famous computer scientist - I try to gently pass this important lesson onward.

[Lars Ericson]

Thanks I didn't know about LawfulMonad. I see there is also CategoryTheory.Monad.

If you were to make a follow-on version of the Monad chapter which added in the use of LawfulMonad, for the same set of examples, how much longer would it be? Twice as long? Book length? Intractable?

There are 3 things to think about:

1. Pure functional programming
2. Proving theorems in blackboard math in Lean
3. Providing functional programs with an accompanying proof of correctness, typically by deriving them via stepwise refinement in correctness-preserving ways from specifications. This is shown to some extent in the chapter with a section on the use of _ to fill out programs, except that the use in the chapter doesn't keep a proof that the result is as desired, just that the result is in the right type. The instance in the book of an unlawful Monad shows the difference between being in the right type and being as desired.

Lean is programmed in Lean. 785 lines of code in Lean refer to Monad. There are 112 references to CategoryTheory.Monad and 101 references to LawfulMonad. How much of Lean in Lean in general is functional programming without proof of correctness? The whole interpreter? How hard would it be to convert it all to a "lawful" style, that is, where every functional programming construct uses a Lawful variant?

[Eric Wieser]

What are you counting as a reference? When you write def foo [Monad m] : m Nat, that doesn't mean foo is unlawful; it just means you're still allowed to use it even if m isn't lawful.

[Eric Wieser]

It's only instance : Monad m that you should worry about, and even then only when there isn't a instance : LawfulMonad m that appears later

[Ioannis Konstantoulas]

I have a question regarding this: do we have theorems that say monad transformers transform lawful monads to lawful monads? And if so, for which transformers do we have such theorems?

[Ioannis Konstantoulas]

(same question for functors and applicatives)

[Henrik Böving]

Ioannis Konstantoulas said:

I have a question regarding this: do we have theorems that say monad transformers transform lawful monads to lawful monads? And if so, for which transformers do we have such theorems?

Those wouldn't be theorems they would be LawfulMonad instnaces and if you check the docs you will see we have a bunch of those: https://leanprover-community.github.io/mathlib4_docs/Init/Control/Lawful.html#LawfulMonad including for transformers, e.g. ExceptT: https://leanprover-community.github.io/mathlib4_docs/Init/Control/Lawful.html#ExceptT.instLawfulMonadExceptTInstMonadExceptT

[Lars Ericson]

Suppose I want to take this snippet:

def Reader (ρ : Type) (α : Type) : Type := ρ → α

def read : Reader ρ ρ := fun env => env

def Reader.pure (x : α) : Reader ρ α := fun _ => x

def Reader.bind {ρ : Type} {α : Type} {β : Type}
  (result : ρ → α) (next : α → ρ → β) : ρ → β :=
  fun env => next (result env) env

instance : Monad (Reader ρ) where
  pure x := fun _ => x
  bind x f := fun env => f (x env) env

and make it lawful by replacing Monad with LawfulMonad. If I do that then I get this message:

hw_monad9.lean:12:11
failed to synthesize instance
  Monad (Reader ρ)

on

instance : LawfulMonad (Reader ρ) where

So it seems to want me to say that Reader is a Monad before I can say that it is a LawfulMonad. So I try that:

def Reader (ρ : Type) (α : Type) : Type := ρ → α

def read : Reader ρ ρ := fun env => env

def Reader.pure (x : α) : Reader ρ α := fun _ => x

def Reader.bind {ρ : Type} {α : Type} {β : Type}
  (result : ρ → α) (next : α → ρ → β) : ρ → β :=
  fun env => next (result env) env

instance : Monad (Reader ρ) where
  pure x := fun _ => x
  bind x f := fun env => f (x env) env

instance : LawfulMonad (Reader ρ) where
  pure x := fun _ => x
  bind x f := fun env => f (x env) env

Then I get an error on pure x := fun _ => x saying that

'pure' is not a field of structure 'LawfulMonad'

My next tactic would be "programming by example". So I look at the declaration of LawfulMonad List in file Data/List/Basic.lean around line 516. It has this:

instance : LawfulMonad List := LawfulMonad.mk'
  (id_map := map_id)
  (pure_bind := fun _ _ => List.append_nil _)
  (bind_assoc := List.bind_assoc)
  (bind_pure_comp := fun _ _ => (map_eq_bind _ _).symm)

If I try running that on it's own, I get:

unknown constant 'LawfulMonad.mk''

So unless I am missing an import, even though LawfulMonad.mk' is available in the context of Basic.lean and LawfulMonad is available without import in the context of my example, LawfulMonad.mk' is not. I also can't find it explicitly declared in any file. I only see uses of it:

~/mathlib4/Mathlib$ grep -r LawfulMonad --include \*.lean | grep mk
Data/List/Basic.lean:instance : LawfulMonad List := LawfulMonad.mk'
Data/PFun.lean:instance lawfulMonad : LawfulMonad (PFun α) := LawfulMonad.mk'
Data/LazyList/Basic.lean:instance : LawfulMonad LazyList := LawfulMonad.mk'
Data/Seq/Computation.lean:instance : LawfulMonad Computation := LawfulMonad.mk'
Data/Seq/Seq.lean:instance lawfulMonad : LawfulMonad Seq1 := LawfulMonad.mk'
Data/Semiquot.lean:instance : LawfulMonad Semiquot := LawfulMonad.mk'
Data/Set/Functor.lean:instance : LawfulMonad Set := LawfulMonad.mk'
Data/Multiset/Functor.lean:instance : LawfulMonad Multiset := LawfulMonad.mk'
GroupTheory/FreeGroup.lean:instance : LawfulMonad FreeGroup.{u} := LawfulMonad.mk'
GroupTheory/FreeAbelianGroup.lean:instance : LawfulMonad FreeAbelianGroup.{u} := LawfulMonad.mk'
Algebra/Free.lean:instance : LawfulMonad FreeMagma.{u} := LawfulMonad.mk'
Algebra/Free.lean:instance : LawfulMonad FreeSemigroup.{u} := LawfulMonad.mk'
Probability/ProbabilityMassFunction/Constructions.lean:instance : LawfulMonad Pmf := LawfulMonad.mk'

This is why a worked example of converting a Monad to a LawfulMonad would be helpful in the Functional Programming text. In general my sense is that, wherever possible, unless it slows things down considerably, even (and maybe especially) the lowest levels of the implementation of Lean in Lean should employ Lawful variants wherever feasible. Teaching this to Lean developers (likely readers of Functional Programming in Lean) from the get-go would promote this as a best practice.

[Eric Wieser]

I recommend you write

instance : LawfulMonad (Reader ρ) := _

and use the code action for filling in the fields

[Eric Wieser]

grep is not a reasonable way to find definitions in Lean. The sensible way is to use something that actually understands the lean code, such as VSCode's goto definition, or the docs search (docs#LawfulMonad.mk'). Note that immediately tells you that you were looking in the wrong directory, mk' is defined in Std!

[Lars Ericson]

@Eric Wieser I don't know how to "use the code action" in VS Code. With just the underscore, it says that it wants something of type ⊢ LawfulMonad (Reader ρ), but it doesn't know how to synthesize placeholder context. This just restates the goal on the left-hand-side of the :=.
Screenshot-from-2023-09-24-13-32-28.png

[Kyle Miller]

If you put your cursor before the _, there should be a blue lightbulb that appears at the beginning of the line. (There might be some command to get a list of available code actions, but I don't know about this yet.)

[Lars Ericson]

@Kyle Miller , placing the cursor to the right of the _ reiterates what is shown in the InfoView, namely that it doesn't know how to synthesize the placeholder context, which I'm guessing means that it doesn't have a code suggestion:
Screenshot-from-2023-09-24-14-43-28.png

[Kyle Miller]

This is the blue lightbulb that I see:

image.png

Maybe you're not importing any of Std or Mathlib?

[Kyle Miller]

I actually have no idea what this symbol is supposed to be, but it's blue

[Eric Wieser]

This almost certainly needs import Std

[Lars Ericson]

I have a problem with import Std, maybe I need to reinstall Lean, my copy is too old? I'm not sure how to update other than reinstall. I am on Ubuntu:
Screenshot-from-2023-09-24-14-53-24.png

[Yaël Dillies]

What's the end of the error message? The start is (usually) a bunch of junk.

[Lars Ericson]

It is

error: stdout:
./lake-packages/std/././Std/Linter/UnnecessarySeqFocus.lean:64:6: error: unknown constant 'Parser.Tactic.Conv.«convNext__=>_»'
error: external command `/home/catskills/.elan/toolchains/leanprover--lean4---nightly-2023-05-16/bin/lean` exited with code 1

[Kyle Miller]

Even with the part of the error that's visible, it looks like your Lean version isn't the one that your Std is expecting, but that's just a guess.

[Kyle Miller]

One thing you need to be sure of is that your lean-toolchain file is referring to a compatible version of Lean. You could take a look at the one at lake-packages/std/lean-toolchain

[Kyle Miller]

If you're using mathlib, there's also the one at lake-packages/mathlib/lean-toolchain

[Lars Ericson]

The instructions for Ubuntu install are

• Launch VS Code.
• Click on the extension icon (image of icon) (or (image of icon) in older versions) in the side bar on the left edge of the screen (or press ShiftCtrlX) and search for leanprover.
• Select the lean4 extension (unique name leanprover.lean4).

That gives me an "Uninstall" option so I will try that and then reinstall.

[Kyle Miller]

You might be able to just copy the contents from the lake-packages/std/lean-toolchain and replace lean-toolchain. Then when you restart Lean from vs code, it will download the compatible version.

[Kyle Miller]

(I don't think uninstalling and reinstalling the Lean 4 extension will change anything for you.)

[Lars Ericson]

The uninstall didn't help, I'm still in a stuck state. What are the shell lake or elan commands to reinstall the latest Lean 4 standard and MathLib files?
Uploading Screenshot from 2023-09-24 15-03-35.png…

[Lars Ericson]

Screenshot-from-2023-09-24-15-03-35.png

[Lars Ericson]

Is it this:

wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile

[Kyle Miller]

Kyle Miller said:

You might be able to just copy the contents from the lake-packages/std/lean-toolchain and replace lean-toolchain. Then when you restart Lean from vs code, it will download the compatible version.

Did you try this?

[Kyle Miller]

Lars Ericson said:

Is it this:

wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile

No, no need to run that again. That command is just to (1) install elan and (2) make sure you have VS Code installed.

[Lars Ericson]

I took a brute force approach. I removed .elan and .mathlib and uninstalled elan and restarted code. That forced a reinstall of .elan. That got me an infoview but it still didn't know Std package. Then I did this:

lake +leanprover/lean4:nightly-2023-02-04 new lean_homework math

This got me here, I will try the suggested lake update next:
Screenshot-from-2023-09-24-15-29-46.png

[Yaël Dillies]

Do not run lake update

[Yaël Dillies]

The safe(r) version of that is lake update YourProjectName

[Yaël Dillies]

But the error clearly tells you the problem: your project is missing a lake-manifest.json. Here's the one from my LeanCamCombi project, which you could copy in and hope that works.

[Lars Ericson]

So now I get the blue lightbulb. Thanks!
Screenshot-from-2023-09-24-15-40-44.png

[Kyle Miller]

This could have probably been resolved in one step, by making sure your lean-toolchain file had the correct Lean version, but glad you found a way to get import Std to work in the end!

[Yaël Dillies]

What exactly does "making sure" mean here? I've heard the phrase a lot, but I still don't know what it means concretely.

[Lars Ericson]

I don't have much state to carry over, and I don't know lake/elan at all or the underlying structure of Lean projects and Std and Mathlib libraries, and Lean 4 is frequently updated. The simplest solution is to delete everything and do an install from scratch, which doesn't take that long.

[Kyle Miller]

Yaël Dillies said:

What exactly does "making sure" mean here? I've heard the phrase a lot, but I still don't know what it means concretely.

It means making sure that lean-toolchain is lake-packages/mathlib/lean-toolchain for example. At least that's what I do. This isn't something that lake manages, as far as I'm aware.

[Lars Ericson]

Note that following the example of the instances in the docs is not the right direction, i.e. this doesn't get me a blue lightbulb (I get a yellow one):

instance : LawfulMonad (Reader ρ) := LawfulMonad.mk' _

failing with

type mismatch
  fun id_map pure_bind bind_assoc => LawfulMonad.mk' ?m.1464 id_map pure_bind bind_assoc
has type
  (∀ {α : Type ?u.1463} (x : ?m.1464 α), id <$> x = x) →
    (∀ {α β : Type ?u.1463} (x : α) (f : α → ?m.1464 β), pure x >>= f = f x) →
      (∀ {α β γ : Type ?u.1463} (x : ?m.1464 α) (f : α → ?m.1464 β) (g : β → ?m.1464 γ),
          x >>= f >>= g = x >>= fun x => f x >>= g) →
        LawfulMonad ?m.1464 : Prop
but is expected to have type
  LawfulMonad (Reader ρ) : Prop

Staring with instance : LawfulMonad (Reader ρ) := _, Ihe blue lightbulb suggests filling out the instance of a LawfulMonad instead:

instance : LawfulMonad (Reader ρ) where
  map_const := _
  id_map := _
  comp_map := _
  seqLeft_eq := _
  seqRight_eq := _
  pure_seq := _
  map_pure := _
  seq_pure := _
  seq_assoc := _
  bind_pure_comp := _
  bind_map := _
  pure_bind := _
  bind_assoc := _

I should be able to useReader.pure and Reader.bind to make apure_bind, then I just need to fill out 12 more functions.

[Eric Wieser]

The error message is telling you that mk' expects more arguments, which you can provide with _s

[Lars Ericson]

@Eric Wieser , adding underscores until it is full, it is telling me that the first thing it wants is a proof for the id_map proposition asserting ⊢ ∀ {α : Type} (x : Reader ρ α), id <$> x = x. I define this verbatim with sorry:

theorem idMap: ∀ {α : Type} (x : Reader ρ α), id <$> x = x := sorry

This has type

idMap (ρ : Type) {α : Type} (x : Reader ρ α) : id <$> x = x

which is not exactly what I'm proving, or maybe it is. However, it doesn't fit in

instance : LawfulMonad (Reader ρ) :=
  @LawfulMonad.mk' idMap _ _ _ _ _ _ _ _ _

The error message is

application type mismatch
  @LawfulMonad.mk' idMap
argument
  idMap
has type
  ∀ (ρ : Type) {α : Type} (x : Reader ρ α), id <$> x = x : Prop
but is expected to have type
  Type ?u.1615 → Type ?u.1614 : Type (max (?u.1614 + 1) (?u.1615 + 1))

To fill out the LawfulMonad, I want to define propositions proved with sorry to match the requested slots, which are id_map, pure_bind, bind_assoc, map_const, seqLeft_eq, seqRight_eq and bind_map. However, based on my first attempt, I'm not sure how to go about this. Here is the full example:
Screenshot-from-2023-09-24-21-27-02.png

[Eric Wieser]

Why did you add the @?

[Lars Ericson]

@Eric Wieser I added the @ to try to nail down the arguments one by one. Without it, Lean fills in implicit arguments and may shift argument positions that I find makes it harder to figure out what is going on. In this case I was unable to create a matching type even though I used the exact type that it requested.

[Eric Wieser]

The best strategy to count arguments in my opinion is:

• don't use @. You'll get an error on the function name.
• keep writing _s until lean draws a red squiggle on the underscores instead of the name; now you're done!

[Lars Ericson]

If I remove the @ and use underscores, the name starts with red squiggles. If I add up to 3 _s, it is still red squiggles:
Screenshot-from-2023-09-30-11-05-50.png

If I add one more _, the first _ and the name lose their red squiggles, but I am left with 3 underscores with red squiggles:
Screenshot-from-2023-09-30-11-07-08.png

It seems like it needs the arguments that it is red-squiggling because it gives each one a name, as we can see in the InfoView, it gives me names and expectations for 9 _s:
Screenshot-from-2023-09-30-11-14-24.png

It is giving me expectations for the red squiggle items, each of which is named, starting with id_map. The first, undecorated _ has no expectation, it just has a type of Type \to Type:

All Messages (8)
hw_monad9.lean:18:20
don't know how to synthesize placeholder for argument 'id_map'
context:
ρ: Type
⊢ ∀ {α : Type} (x : Reader ρ α), id <$> x = x
hw_monad9.lean:18:22
don't know how to synthesize placeholder for argument 'pure_bind'
context:
ρ: Type
⊢ ∀ {α β : Type} (x : α) (f : α → Reader ρ β), pure x >>= f = f x
hw_monad9.lean:18:24
don't know how to synthesize placeholder for argument 'bind_assoc'
context:
ρ: Type
⊢ ∀ {α β γ : Type} (x : Reader ρ α) (f : α → Reader ρ β) (g : β → Reader ρ γ), x >>= f >>= g = x >>= fun x => f x >>= g
hw_monad9.lean:18:26
don't know how to synthesize placeholder for argument 'map_const'
context:
ρ: Type
⊢ ∀ {α β : Type} (x : α) (y : Reader ρ β), Functor.mapConst x y = Function.const β x <$> y
hw_monad9.lean:18:28
don't know how to synthesize placeholder for argument 'seqLeft_eq'
context:
ρ: Type
⊢ ∀ {α β : Type} (x : Reader ρ α) (y : Reader ρ β),
  (SeqLeft.seqLeft x fun x => y) = do
    let a ← x
    let _ ← y
    pure a
hw_monad9.lean:18:30
don't know how to synthesize placeholder for argument 'seqRight_eq'
context:
ρ: Type
⊢ ∀ {α β : Type} (x : Reader ρ α) (y : Reader ρ β),
  (SeqRight.seqRight x fun x => y) = do
    let _ ← x
    y
hw_monad9.lean:18:32
don't know how to synthesize placeholder for argument 'bind_pure_comp'
context:
ρ: Type
⊢ ∀ {α β : Type} (f : α → β) (x : Reader ρ α),
  (do
      let y ← x
      pure (f y)) =
    f <$> x
hw_monad9.lean:18:34
don't know how to synthesize placeholder for argument 'bind_map'
context:
ρ: Type
⊢ ∀ {α β : Type} (f : Reader ρ (α → β)) (x : Reader ρ α),
  (do
      let x_1 ← f
      x_1 <$> x) =
    Seq.seq f fun x_1 => x

[Lars Ericson]

I have no idea how to proceed. I will look at code examples for LawfulMonad.mk' in the MathLib source. There are more instances there than I see in the doc#LawfulMonad.

[Sky Wilshaw]

The last five parameters are autoParams. This means that you're allowed to omit them, and Lean will work them out for you.

[Sky Wilshaw]

So you only need to provide proofs for id_map, pure_bind, and bind_assoc.

[Sky Wilshaw]

One way to do this would be

instance : LawfulMonad (Reader \rho) := by
  refine LawfulMonad.mk _ ?id_map ?pure_bind ?bind_assoc
  case id_map =>
    sorry
  case pure_bind =>
    sorry
  case bind_assoc =>
    sorry

[Sky Wilshaw]

Note that the first _ is just the type of the monad, i.e. Reader \rho. Lean can figure this out so you don't need to fill the hole yourself.

[Eric Wieser]

This is all a lot easier in tactic mode (though not idiomatic); you could have just used apply LawfulMonad.mk' and it would have played the underscore game for you

[Lars Ericson]

Thank you @Sky Wilshaw . That doesn't quite get me to a happy proof-by-sorry state, i.e. one in which there are no messages except "proof by sorry". Here is what I see:
Screenshot-from-2023-09-30-11-33-38.png

Looking for other examples, the following files have LawfulMonad instances:

$ grep -r LawfulMonad --include \*.lean | grep "instance :"

lake-packages/mathlib/Mathlib/Data/Part.lean:instance : LawfulMonad
lake-packages/mathlib/Mathlib/Data/Quot.lean:instance : LawfulMonad Trunc where
lake-packages/mathlib/Mathlib/Data/Seq/Computation.lean:instance : LawfulMonad Computation := LawfulMonad.mk'
lake-packages/mathlib/Mathlib/Data/Semiquot.lean:instance : LawfulMonad Semiquot := LawfulMonad.mk'
lake-packages/mathlib/Mathlib/Data/Set/Functor.lean:instance : LawfulMonad Set := LawfulMonad.mk'
lake-packages/mathlib/Mathlib/Data/Multiset/Functor.lean:instance : LawfulMonad Multiset := LawfulMonad.mk'
lake-packages/mathlib/Mathlib/Data/Finset/Functor.lean:instance : LawfulMonad Finset :=
lake-packages/mathlib/Mathlib/GroupTheory/FreeGroup.lean:instance : LawfulMonad FreeGroup.{u} := LawfulMonad.mk'
lake-packages/mathlib/Mathlib/GroupTheory/FreeAbelianGroup.lean:instance : LawfulMonad FreeAbelianGroup.{u} := LawfulMonad.mk'
lake-packages/mathlib/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean:instance : LawfulMonad Pmf := LawfulMonad.mk'
lake-packages/mathlib/Mathlib/Control/Monad/Cont.lean:instance : LawfulMonad (ContT r m) := LawfulMonad.mk'
lake-packages/mathlib/Mathlib/Control/Monad/Cont.lean:instance : LawfulMonadCont (ContT r m) where
lake-packages/mathlib/Mathlib/Control/Basic.lean:instance : LawfulMonad (Sum.{v, u} e) where
lake-packages/mathlib/Mathlib/Control/ULift.lean:instance : LawfulMonad PLift where
lake-packages/mathlib/Mathlib/Control/ULift.lean:instance : LawfulMonad ULift where
lake-packages/std/Std/Classes/LawfulMonad.lean:instance : LawfulMonad (Except ε) := LawfulMonad.mk'
lake-packages/std/Std/Classes/LawfulMonad.lean:instance : LawfulMonad Option := LawfulMonad.mk'

For example, here is LazyList:

instance : LawfulMonad LazyList := LawfulMonad.mk'
  (bind_pure_comp := by
    intro _ _ f xs
    simp only [bind, Functor.map, pure, singleton]
    induction' xs using LazyList.rec with _ _ _ _ ih
    · rfl
    · simp only [bind._eq_2, append, traverse._eq_2, Id.map_eq, cons.injEq, true_and]; congr
    · ext; apply ih)
  (pure_bind := by
    intros
    simp only [bind, pure, singleton, LazyList.bind]
    apply append_nil)
  (bind_assoc := by
    intro _ _ _ xs _ _
    induction' xs using LazyList.rec with _ _ _ _ ih
    · rfl
    · simp only [bind, LazyList.bind, append_bind]; congr
    · congr; funext; apply ih)
  (id_map := by
    intro _ xs
    induction' xs using LazyList.rec with _ _ _ _ ih
    · rfl
    · simpa only [Functor.map, traverse._eq_2, id_eq, Id.map_eq, Seq.seq, cons.injEq, true_and]
    · ext; apply ih)

From this the pattern would be:

instance : LawfulMonad (Reader ρ) := LawfulMonad.mk'
  (bind_pure_comp := by sorry)
  (pure_bind := by sorry)
  (bind_assoc := by sorry)
  (id_map := by sorry)

That works:
Screenshot-from-2023-09-30-11-34-53.png

[Sky Wilshaw]

Ah, sorry, missed a prime on mk'.

[Sky Wilshaw]

Both ways should work, and the one you found seems more commonly used.

[Lars Ericson]

@Eric Wieser , using apply gives me 8 goals rather than 4 for the version above, but at least the red squiggle problem mostly goes away (it is squiggling the by to tell me that I have more work to do):
Screenshot-from-2023-09-30-11-40-55.png

[Sky Wilshaw]

Sky Wilshaw said:

Ah, sorry, missed a prime on mk'.

Incidentally, it's easier to help if you copy+paste a working #mwe rather than a screenshot, because then we can test your code.

[Sky Wilshaw]

(and test our suggestions)

[Lars Ericson]

Thank you @Sky Wilshaw this is the #mwe:

import Std

def Reader (ρ : Type) (α : Type) : Type := ρ → α

def read : Reader ρ ρ := fun env => env

def Reader.pure (x : α) : Reader ρ α := fun _ => x

def Reader.bind {ρ : Type} {α : Type} {β : Type}
  (result : ρ → α) (next : α → ρ → β) : ρ → β :=
  fun env => next (result env) env

instance : Monad (Reader ρ) where
  pure x := fun _ => x
  bind x f := fun env => f (x env) env

instance : LawfulMonad (Reader ρ) := LawfulMonad.mk'
  (bind_pure_comp := sorry)
  (pure_bind := fun a f => rfl)
  (bind_assoc := fun x f g => sorry)
  (id_map := fun x => sorry)

Also this is a nice way to present examples, except it requires a tiny url due to presence of parentheses.

[Alex J. Best]

Anyone can click on the button in the top right of your code block to "view in lean 4 playground" and it will open the required lean 4 online interface for them

[Lars Ericson]

Going back to the motivating problem, in the text, a lawful monad is described as one which satisfies the "monad contract":

• LI: pure should be a left identity of bind: bind (pure v) = f v
• RI: pure should be a right identity of bind: bind v pure = v
• Assoc: bind should be associative: bind (bind v f) g = bind v (fun x => bind (f x) g)

In MathLib, the LawfulMonad.mk' contract is a little different. One instance shows four conditions are required:

instance : LawfulMonad Option := LawfulMonad.mk'
  (id_map := fun x => by cases x <;> rfl)
  (pure_bind := fun x f => rfl)
  (bind_assoc := fun x f g => by cases x <;> rfl)
  (bind_pure_comp := fun f x => by cases x <;> rfl)

Another instance only requires three:

instance : LawfulMonad (Except ε) := LawfulMonad.mk'
  (id_map := fun x => by cases x <;> rfl)
  (pure_bind := fun a f => rfl)
  (bind_assoc := fun a f g => by cases a <;> rfl)

This instance requires bind_map as well:

instance : LawfulMonad Set := LawfulMonad.mk'
  (id_map := image_id)
  (pure_bind := biUnion_singleton)
  (bind_assoc := fun _ _ _ => by simp only [bind_def, biUnion_iUnion])
  (bind_pure_comp := fun _ _ => (image_eq_iUnion _ _).symm)
  (bind_map := fun _ _ => seq_def.symm)

So bind_pure_comp and bind_map come with proofs which doesn't always work (more of a tactic?), and when they don't, it suffices to substitute a working proof (something I didn't know). There are additional properties to the LawfulMonad.mk' supplied with proofs that might not work, namely seqLeft_eq, seqRight_eq, in which case we would need to supply them.

So, the five essential elements of the LawfulMonad.mk' contract are:

• id_map: ∀ {α} (x : m α), id <$> x = x
• pure_bind: ∀ {α β} (x : α) (f : α → m β), ((pure x) >>= f)= (f x))
• bind_assoc: ∀ {α β γ} (x : m α) (f : α → m β) (g : β → m γ), ((x >>= f) >>= g) = (x >>= (fun x => (f x >>= g)))
• bind_pure_comp: ∀ {α β} (f : α → β) (x : m α), (x >>= (fun y => pure (f y))) = (f <$> x)
• bind_map : ∀ {α β} (f : m (α → β)) (x : m α), f >>= (. <$> x) = f <*> x

Pairing these up with the book's monad contract:

• bind_assoc: ∀ {α β γ} (x : m α) (f : α → m β) (g : β → m γ), ((x >>= f) >>= g) = (x >>= (fun x => (f x >>= g)))
• Assoc: bind should be associative: bind (bind v f) g = bind v (fun x => bind (f x) g)

and

• RI: pure should be a right identity of bind: bind v pure = v
• id_map: ∀ {α} (x : m α), id <$> x = x

and

• LI: pure should be a left identity of bind: bind (pure v) = f v
• pure_bind: ∀ {α β} (x : α) (f : α → m β), ((pure x) >>= f)= (f x))

and these are extra:

• bind_pure_comp: ∀ {α β} (f : α → β) (x : m α), (x >>= (fun y => pure (f y))) = (f <$> x)
• bind_map : ∀ {α β} (f : m (α → β)) (x : m α), f >>= (. <$> x) = f <*> x

I don't really have a clue how to prove these properties from scratch. In desperation, I look at all examples in Mathlib of proofs these properties:

(pure_bind := by intros; simp [Bind.bind, Pure.pure, WriterT.mk])
(pure_bind := fun x f => funext fun a => Part.bind_some _ (f x))
(pure_bind := by intros; simp only [bind, pure, singleton, LazyList.bind]; apply append_nil)
(pure_bind := @ret_bind)
(pure_bind := fun {α β} x f => ext.2 <| by simp)
(pure_bind := fun _ _ ↦ by simp only [pure_def, bind_def, singleton_bind])
(pure_bind := fun x f => pure_bind f x)
(pure_bind := fun x f ↦ pure_bind f x)
(pure_bind := fun f x ↦ rfl)
(pure_bind := pure_bind)
(pure_bind := fun _ _ => List.append_nil _)
(pure_bind := by intros; apply OptionT.ext; simp)
(pure_bind := by intros; ext; rfl)
(pure_bind := by intros; simp [Bind.bind, Pure.pure, WriterT.mk])

(id_map := by intros; simp [Functor.map, WriterT.mk])
(id_map := fun f => by funext a; dsimp [Functor.map, PFun.map]; cases f a; rfl)
(id_map := by intro _ xs; induction' xs using LazyList.rec with _ _ _ _ ih; · rfl; · simpa only [Functor.map, traverse._eq_2, id_eq, Id.map_eq, Seq.seq, cons.injEq, true_and]; · ext; apply ih)
(id_map := @map_id)
(id_map := fun {α} q => ext.2 <| by simp)
(id_map := fun _ ↦ by simp only [fmap_def, id_eq, map_id'])
(id_map := fun x => FreeGroup.induction_on x (map_one id) (fun x => map_pure id x) (fun x ih => by rw [map_inv, ih]); fun x y ihx ihy => by rw [map_mul, ihx, ihy])
(id_map := fun x ↦ FreeAbelianGroup.induction_on' x (FreeAbelianGroup.map_zero id) (map_pure id); (fun x ih ↦ by rw [FreeAbelianGroup.map_neg, ih]); fun x y ihx ihy ↦ by rw [FreeAbelianGroup.map_add, ihx, ihy])
(id_map := fun x ↦ FreeMagma.recOnPure x (fun _ ↦ rfl) fun x y ih1 ih2 ↦ by rw [map_mul', ih1, ih2]);(id_map := id_map);(id_map := map_id);(id_map := by;intros;apply OptionT.ext;simp only [OptionT.run_map];rw [map_congr, id_map];intro a;cases a <;> rfl)
(id_map := by intros; rfl)
(id_map := by intros; simp [Functor.map, WriterT.mk])

(bind_assoc := by intros; simp [Bind.bind, mul_assoc, WriterT.mk, ← bind_pure_comp])
(bind_assoc := fun f g k => funext fun a => (f a).bind_assoc (fun b => g b a) fun b => k b a)
(bind_assoc := by intro _ _ _ xs _ _; induction' xs using LazyList.rec with _ _ _ _ ih; · rfl; · simp only [bind, LazyList.bind, append_bind]; congr;  · congr; funext; apply ih)
(bind_assoc := @bind_assoc)
(bind_assoc := fun {α β} γ s f g => ext.2 <| by simp only [bind_def, mem_bind]; exact fun c => ⟨fun ⟨b, ⟨a, as, bf⟩, cg⟩ => ⟨a, as, b, bf, cg⟩,; fun ⟨a, as, b, bf, cg⟩ => ⟨b, ⟨a, as, bf⟩, cg⟩⟩)
(bind_assoc := @bind_assoc)
(bind_assoc := fun x => FreeGroup.induction_on x(by intros; iterate 3 rw [one_bind])(fun x => by intros; iterate 2 rw [pure_bind])(fun x ih => by intros;(iterate 3 rw [inv_bind]); rw [ih])(fun x y ihx ihy => by intros;(iterate 3 rw [mul_bind]); rw [ihx, ihy]))
(bind_assoc := fun x f g ↦ FreeAbelianGroup.induction_on' x (by iterate 3 rw [zero_bind]) (fun x ↦ by iterate 2 rw [pure_bind]) (fun x ih ↦ by iterate 3 rw [neg_bind] <;> try rw [ih]) fun x y ihx ihy ↦ by iterate 3 rw [add_bind] <;> try rw [ihx, ihy])
(bind_assoc := fun x f g ↦ FreeMagma.recOnPure x (fun x ↦ rfl) fun x y ih1 ih2 ↦ by rw [mul_bind, mul_bind, mul_bind, ih1, ih2])
(bind_assoc := bind_bind)
(bind_assoc := List.bind_assoc)
(bind_assoc := by  intros; apply OptionT.ext; simp only [OptionT.run_bind, bind_assoc] rw [bind_congr] intro a; cases a <;> simp)
(bind_assoc := by intros; ext; rfl)
(bind_assoc := by intros; simp [Bind.bind, mul_assoc, WriterT.mk, ← bind_pure_comp])

(bind_pure_comp := by intros; simp [Bind.bind, Functor.map, Pure.pure, WriterT.mk, bind_pure_comp])
(bind_pure_comp := fun f x => funext fun a => Part.bind_some_eq_map _ _)
(bind_pure_comp := by intro _ _ f xs; simp only [bind, Functor.map, pure, singleton]; induction' xs using LazyList.rec with _ _ _ _ ih; · rfl; · simp only [bind._eq_2, append, traverse._eq_2, Id.map_eq, cons.injEq, true_and]; congr;  · ext; apply ih)
(bind_pure_comp := @bind_pure)
(bind_pure_comp := fun {α β} f s => ext.2 <| by simp [eq_comm])
(bind_pure_comp := fun _ _ ↦ by simp only [pure_def, bind_def, bind_singleton, fmap_def])
(bind_pure_comp  := fun f x => FreeGroup.induction_on x (by rw [one_bind, map_one]) (fun x => by rw [pure_bind, map_pure]); (fun x ih => by rw [inv_bind, map_inv, ih]) fun x y ihx ihy => by; rw [mul_bind, map_mul, ihx, ihy])
(bind_pure_comp := fun f x => rfl)
(bind_pure_comp := fun _ _ => (map_eq_bind _ _).symm)
(bind_pure_comp := by intros; simp [Bind.bind, Functor.map, Pure.pure, WriterT.mk, bind_pure_comp])

I use the simplest method for the first 3, and I guess I don't need a proof of bind_pure_comp. It just works:

import Std

def Reader (ρ : Type) (α : Type) : Type := ρ → α

def read : Reader ρ ρ := fun env => env

def Reader.pure (x : α) : Reader ρ α := fun _ => x

def Reader.bind {ρ : Type} {α : Type} {β : Type}
  (result : ρ → α) (next : α → ρ → β) : ρ → β :=
  fun env => next (result env) env

instance : Monad (Reader ρ) where
  pure x := fun _ => x
  bind x f := fun env => f (x env) env

instance : LawfulMonad (Reader ρ) := LawfulMonad.mk'
  (pure_bind := fun a f => rfl)
  (id_map := by intros; rfl)
  (bind_assoc := by intros; rfl)

I have no idea what these 3 proofs do. They just work.

I have no idea when the default proofs of the other properties such as bind_pure_comp and bind_map might be insufficient, and why.

My editorial takeaway is that, while it doesn't add a substantial amount of additional code in this example, it does seem like developers implementing the more operational aspects of Lean in Lean, or developers tempted to use Lean as a programming language for some other application, would have a very hard time making all of their implementation code "lawful", in the sense of proving that every piece of implementation code satisfied some initial pre-coding-phase functional specification.

[Lars Ericson]

So anyway, I would mark this Resolved, but I can't:
Screenshot-from-2023-10-01-12-19-45.png

[Henrik Böving]

Dont worry about it we generally don't use the resolve feature much here

[Mario Carneiro]

(in fact you should not use it, it breaks links)

[Mario Carneiro]

The reason there are additional fields is because Lean's Monad typeclass allows you to customize the map function, rather than assuming it is defined in terms of bind and pure. If you do such customization, you have to prove this as an equality instead, that's the bind_pure_comp theorem. If you don't do any customization, those three axioms you mention are sufficient:

import Std

def M (α : Type) : Type := sorry

def M.pure {α} (x : α) : M α := sorry
def M.bind {α : Type} {β : Type} (result : M α) (next : α → M β) : M β  := sorry

instance : Monad M where
  pure := M.pure
  bind := M.bind

instance : LawfulMonad M := LawfulMonad.mk'
  (pure_bind := fun a f => show M.bind (M.pure a) f = f a from sorry)
  (bind_assoc := fun v f g => show bind (bind v f) g = bind v (fun x => bind (f x) g) from sorry)
  (id_map := fun x => show M.bind x M.pure = x from sorry)

[Lars Ericson]

@Mario Carneiro the fact that the supplied proof of a field in a structure after the := is a default that can be overriden is something I learned only in this exercise. It's an interesting feature, good to know. I'm not sure where it should go in a full Lean curriculum. My self-training curriculum for now is in this order:

• Functional Programming in Lean
• Theorem Proving in Lean 4
• The mechanics of proof
• Mathematics in Lean
• LTCM 2020 Exercises

[Eric Wieser]

That last step makes no sense, the code you link to is lean 3!

[Lars Ericson]

Is there a Lean 4 version of the LTCM exercises? That would be an exercise in itself.

[Eric Wieser]

Well, there's LFTCM2023

[Jireh Loreaux]

@Lars Ericson default definitions are covered in #fpil, namely https://lean-lang.org/functional_programming_in_lean/functor-applicative-monad/inheritance.html?highlight=default#default-declarations

[Jireh Loreaux]

Lars Ericson said:

I have no idea what these 3 proofs do. They just work.

Just hover on the tactics and it will explain what they do.

My editorial takeaway is that, while it doesn't add a substantial amount of additional code in this example, it does seem like developers implementing the more operational aspects of Lean in Lean, or developers tempted to use Lean as a programming language for some other application, would have a very hard time making all of their implementation code "lawful", in the sense of proving that every piece of implementation code satisfied some initial pre-coding-phase functional specification.

I'm sure part of the reason docs#Monad doesn't include the lawful properties is so that developers aren't forced to provide the proofs when they don't want to. Making all their implementation code lawful could indeed be a burden, but I think it's not fair to say the proofs in the above example are hard (it's just that they're true by definition after all).