monadic `join`

[jamesmckinna]

Apologies if I have missed something down the years, but why does Effect.Monad.RawMonad not also define monadic join

μ : F (F A) → F A
μ = _>>= id

(also: join or μ as preferred identifier for this?)

[gallais]

Remember that the functor is not necessarily an endofunctor level-wise:
(F : Set f → Set g)
We can only have join if f = g.

[jamesmckinna]

Oh dear... I see. And would g ≤ f work also?
But I suppose we could define join for the special case of the smart constructor mkRawMonad version?
ADDED: eg as (I think this could be tidied up a lot, but I get confused about module/record/do-syntax scoping rules)

record RawMonadWithJoin (F : Set f → Set f) : Set (suc f) where

  field
    rawMonad : RawMonad F

  open RawMonad rawMonad public

  join : F (F A) → F A
  join = _>>= id


-- Smart constructors

module _ (F : Set f → Set f)
       (pure : ∀ {A} → A → F A)
       (bind : ∀ {A B} → F A → (A → F B) → F B) where

  open RawMonadWithJoin using (rawMonad)
  open RawMonad using (rawApplicative; _>>=_)
  open RawApplicative hiding (pure)

  mkRawMonad : RawMonad F
  mkRawMonad .rawApplicative = mkRawApplicative F pure
    λ mf mx → bind mf λ f → bind mx λ x → pure (f x)
  mkRawMonad ._>>=_ = bind

  mkRawMonadWithJoin : RawMonadWithJoin F
  mkRawMonadWithJoin .rawMonad = mkRawMonad

[jamesmckinna]

[Moved from the discussion of #2079 ]

Do we need a whole new record or is it sufficient to have a module parametrised by a monad and deriving join from bind?

Good question! ... you're probably right, something along the lines of : in module Effect.Monad

module Join {F : Set f → Set f} {{M : RawMonad F}} where
  join : F (F A) → F A
  join = _>>= id where open RawMonad M

... and then for downstream RawMonad instances monad:

join = Join.join where instance _ = monad

Questions remain (for me) about the design:

• laws?
• separating out 'structure' from 'bundle' (maybe only makes sense once we have laws)
• ...?

REVISED: M above is now an explicit argument, with the boilerplate code now being

join = Join.join monad