Function Monad

Stream: general

[Kevin Fisher]

So, I know in Haskell we have a function monad:

instance Monad ((->) r) where
     return x = \_ -> x
     h >>= f = \w -> f (h w) w

Does such a thing exist in Lean?

I ask because I'm trying to define the following function pointfree:

def double (α β : Type) (f : α → α → β) (x : α) : β := f x x

I know in Haskell I can use the function monad like so:

double :: (a -> a -> b) -> a -> b
double = join

But using joinM or Monad.join doesn't seem to work in Lean.

[Kyle Miller]

I don't think there's a monad instance on the function type itself, but at least there's the Reader monad, which is the same thing but with a name.

def double (α β : Type) : (α → α → β) → α → β :=
  show ReaderM α (ReaderM α β) → ReaderM α β from
    joinM

[Kyle Miller]

This doesn't work:

instance (ρ : Type _) : Monad (ρ → ·) := inferInstanceAs <| Monad (ReaderM ρ)

def double (α β : Type) : (α → α → β) → α → β :=
  joinM -- fails

[Kevin Fisher]

Hm, I wonder why it's not defined. Does it break one of the monad laws or something?

[Kyle Miller]

A proximal reason is that it just doesn't work (like in my second code block)

But, for a design reason, I think it's better when monads are explicit. If you have α → α → β, is this α → α → β, α → ReaderM α β, ReaderM α (α → β), or ReaderM α (ReaderM α β)? Lean's hard enough, let's not make it impossible to guess in what way a value is meant to be a monad too :-)

[Kevin Fisher]

Fair enough, it is pretty magical in Haskell. Guess I'll have to read up about reader monads then

[Kyle Miller]

Given that you seem to know about the function monad, and that ReaderM α β is literally α → β by definition, I think you don't need to do any reading here. ReaderM α is exactly the function monad, but explicitly written.

[Kyle Miller]

The main operation it gives is read. Reading through the Lean definitions is a bit complicated, because it's meant to be convenient for a number of monads, but for the case of ReaderM we could define it as

def read {ρ : Type _} : ReaderM ρ ρ := id

It "reads" the state (hence why it is called "reader monad").

[Matt Diamond]

hmm...

import Mathlib

instance Function.instMonad (α : Type) : Monad (α → ·) where
  pure x := fun _ => x
  bind f g := fun x => g (f x) x

instance (α : Type) : LawfulMonad (α → ·) :=
LawfulMonad.mk'
  (m := (α → ·))
  (id_map := by aesop)
  (pure_bind := by aesop)
  (bind_assoc := by aesop)

[Kyle Miller]

This shouldn't be surprising @Matt Diamond, you redefined the ReaderM monad. Your func α is ReaderM α :-)

example (ρ : Type) : Function.instMonad ρ = (inferInstance : Monad (ReaderM ρ)) := rfl

[Kyle Miller]

(I commented before your edit)

[Matt Diamond]

your comment is still true, right? (oh you just meant you were referring to func?)

[Kyle Miller]

The monad definition in #general > Function Monad @ 💬 is also same as the one you give post-edit btw.

[Kyle Miller]

Yeah, I'm saying no need to define func, since that's already ReaderM.

[Matt Diamond]

just to be clear @Kevin Fisher, this does work (if you include my monad definition above):

def double (α β : Type) : (α → α → β) → α → β := Monad.join (m := (α → .))

Edit: Oh, I see what Kyle is saying... this works out of the box:

def double (α β : Type) : (α → α → β) → α → β := Monad.join (m := ReaderM _)

so it looks like you can use Monad.join after all... it just needs a type hint