Synthesize typeclass instance

Stream: new members

[Rudy Peterson]

Hello,

I am trying to define a Reader Monad and show it satisfies the monad laws:

class MonadLaws (M : Type -> Type) [Monad M] where

  pureL : ∀ {α β : Type} (a : α) (f : α -> M β),
    pure a >>= f = f a

  pureR : ∀ {α : Type} (m : M α),
    m >>= pure = m

  bindAssoc : ∀ {α β γ} (m : M α) (f : α -> M β) (g : β -> M γ),
    m >>= f >>= g = m >>= (fun a => f a >>= g)

def ReaderMonad (M : Type -> Type) (ρ α : Type) : Type := ρ -> M α

instance ReaderMonad.Monad (M : Type -> Type) [Monad M] (ρ : Type) : Monad (ReaderMonad M ρ) where
  pure a := fun _ => pure a
  bind m f := fun r => m r >>= fun a => f a r

instance ReaderMonad.MonadLaws (M : Type -> Type) [Monad M] [MonadLaws M] (ρ : Type) : MonadLaws (ReaderMonad M ρ) where
  pureL a f := by sorry
  pureR m := by sorry
  bindAssoc m f g := by sorry

However in my declaration for ReaderMonad.MonadLaws I get an error for [Monad M]:

▶ 66:52-66:59: error:
failed to synthesize
  _root_.Monad M
Additional diagnostic information may be available using the `set_option diagnostics true` command.

This error vanishes when I remove the dot from the name of ReaderMonad.Monad as:

instance ReaderMonadMonad (M : Type -> Type) [Monad M] (ρ : Type) : Monad (ReaderMonad M ρ) where
  pure a := fun _ => pure a
  bind m f := fun r => m r >>= fun a => f a r

Why is this happening? How can I get my code to work when there is still a dot in the name? I tried passing explicit typeclass arguments to MonadLaws but it did not help.

Thanks!

[Matt Diamond]

It looks like this is a namespace issue: since you're defining ReaderMonad.MonadLaws in the ReaderMonad namespace, it's confusing Monad with ReaderMonad.Monad. (Notice that the error also goes away if you remove the dot from the name of ReaderMonad.MonadLaws, bringing it out of the ReaderMonad namespace.)

It's a bit ugly, but one way to get around this is to change [Monad M] to [_root_.Monad M], explicitly specifying which Monad you're talking about.

[Matt Diamond]

A better way might be to rename ReaderMonad.Monad to ReaderMonad.instMonad, which is the naming convention that Lean follows (see e.g. docs#ReaderT.instMonad).

[Matt Diamond]

(maybe you're already aware but just wanted to note that Lean has docs#LawfulMonad and docs#LawfulMonad.mk')

[Kevin Buzzard]

Matt Diamond said:

A better way might be to rename ReaderMonad.Monad to ReaderMonad.instMonad, which is the naming convention that Lean follows (see e.g. docs#ReaderT.instMonad).

Or ReaderMonad.monad (the convention is capital letters for types, small for terms).

[Rudy Peterson]

Thanks!

I tried continuing and have the following:

instance ReaderMonad.instMonadLaws (M : Type -> Type) [iM : Monad M] [iML : MonadLaws M] (ρ : Type) : MonadLaws (ReaderMonad M ρ) where
  pureL a f := by
    funext r
    dsimp [bind, pure]
    rw [iML.pureL]

  pureR m := by
    funext r
    dsimp [bind, pure]
    rw [iML.pureR]

  bindAssoc m f g := by
    funext r
    dsimp [bind]
    rw [iML.bindAssoc]

def ReaderOption := ReaderMonad Option

instance ReaderOption.instMonad (ρ : Type) : Monad (ReaderOption ρ) := ReaderMonad.instMonad Option ρ

instance ReaderOption.instMonadLaws (ρ : Type) : MonadLaws (ReaderOption ρ) := ReaderMonad.instMonadLaws Option ρ

However, in my editor (doom emacs using lean4-mode) the entire declaration for ReaderMonad.instMonadLaws has yellow highlighting on the side, and lean rejects my definition for ReaderOption.instMonadLaws entirely with:

Messages below:
86:79:
failed to synthesize
  MonadLaws Option
Additional diagnostic information may be available using the `set_option diagnostics true` command.

How do I get it to find ReaderOption.instMonad?

Thanks!

[Eric Wieser]

Replacing def with abbrev might help

[Rudy Peterson]

Thanks for the suggestion! It still rejects it though:

abbrev ReaderOption := ReaderMonad Option

instance ReaderOption.instMonad (ρ : Type) : Monad (ReaderOption ρ) := ReaderMonad.instMonad Option ρ

instance ReaderOption.instMonadLaws (ρ : Type) : MonadLaws (ReaderOption ρ) := ReaderMonad.instMonadLaws Option ρ

[Eric Wieser]

Rudy Peterson said:

How do I get it to find ReaderOption.instMonad?

This is the wrong question, the thing you're looking for is MonadLaws Option but your suggested solution ReaderOption.instMonad is of type : Monad (ReaderOption ρ)

[Eric Wieser]

You need to prove that Option satisfies your MonadLaws

[Rudy Peterson]

Ah I see, somewhere above I had a:

def Option.instMonadLaws : MonadLaws Option where
  pureL a f := by rfl
  pureR m := by
    cases m
    case none   => rfl
    case some a => rfl
  bindAssoc m f g := by
    cases m
    case none   => rfl
    case some a => rfl

But when I change def to instance it is able to find it.