http://coalg.org/calco15/papers/p18-Piróg.pdf

MonadsAsModules.agda

module MonadsAsModules where

import Agda.Primitive using (Level)

id : ∀ {k}{X : Set k} → X → X
id x = x

const : ∀ {a b} {A : Set a} {B : Set b} → A → B → A
const x _ = x

_∘_ : ∀ {i j k}
        {A : Set i}{B : A → Set j}{C : (a : A) → B a → Set k} →
        (f : {a : A}(b : B a) → C a b) →
        (g : (a : A) → B a) →
        (a : A) → C a (g a)
f ∘ g = λ a → f (g a)

flip : ∀ {a b c} {A : Set a} {B : Set b} {C : A → B → Set c} →
       ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
flip f = λ y x → f x y

infixr 9 _∘_

record EndoFunctor (F : Set → Set) : Set₁ where
  constructor MkEndo
  field
    map : ∀ { S T } → (S → T) → F S → F T
open EndoFunctor {{...}} public

record Applicative (F : Set → Set) : Set₁ where
  infixl 4 _⍟_
  field
    pure : ∀ { X } → X → F X
    _⍟_ : ∀ { S T } → F (S → T) → F S → F T

  applicativeEndoFunctor : EndoFunctor F
  applicativeEndoFunctor = record { map = _⍟_ ∘ pure }
open Applicative {{...}} public

record Monad (F : Set → Set) : Set₁ where
  field
    return : ∀ { X } → X → F X
    _>>=_ : ∀ { S T } → F S → (S → F T) → F T
  monadApplicative : Applicative F
  monadApplicative = record
    { pure = return
    ; _⍟_ =  λ ff fs → ff >>= λ f → fs >>= λ s → return (f s)
    }
  monadEndoFunctor : EndoFunctor F
  monadEndoFunctor = Applicative.applicativeEndoFunctor monadApplicative

  μᴹ : ∀ {X} → F (F X) → F X
  μᴹ = flip _>>=_ id
open Monad {{...}} public

record RightModule (S : Set → Set) {{SEF : EndoFunctor S}} (M : Set → Set) {{RMM : Monad M}} : Set₁ where
  field
    μ→ : ∀ {X} → S (M X) → S X
open RightModule {{...}} public

record LeftModule (L : Set → Set) {{SEF : EndoFunctor L}} (M : Set → Set) {{RMM : Monad M}} : Set₁ where
  field
    ←μ : ∀ {X} → M (L X) → L X
open LeftModule {{...}} public

instance
  monadRightModule : ∀ {M : Set → Set}{{MM : Monad M}} → RightModule M {{monadEndoFunctor}} M
  monadRightModule {M}{{MM}} = record { μ→ = μᴹ }

  monadLeftModule : ∀ {M : Set → Set}{{MM : Monad M}} → LeftModule M {{monadEndoFunctor}} M
  monadLeftModule {M}{{MM}} = record { ←μ = μᴹ }

  monadMorphismRightModule : ∀ {M T : Set → Set}{{MM : Monad M}}{{MT : Monad T}} → (∀ {X} → M X → T X) → RightModule T {{monadEndoFunctor}} M
  monadMorphismRightModule {M}{T}{{MM}}{{MT}} m = record { μ→ = μᴹ ∘ (λ a → m (Monad.return MM ((MT Monad.>>= a) m))) }

  monadMorphismLeftModule : ∀ {M T : Set → Set}{{MM : Monad M}}{{MT : Monad T}} → (∀ {X} → M X → T X) → LeftModule T {{monadEndoFunctor}} M
  monadMorphismLeftModule {M}{T}{{MM}}{{MT}} m = record { ←μ = μᴹ ∘ m }