gistfile1.agda

module MonadLaws where

open import Category.Applicative
open import Category.Applicative.Indexed
open import Category.Functor
open import Category.Monad
open import Category.Monad.Indexed
open import Data.Maybe renaming (monad to monadMaybe)
open import Function
open import Level
open import Relation.Binary.PropositionalEquality as P

private
  postulate
    ext : ∀ {ℓ} → P.Extensionality ℓ ℓ

record PropFunctor {ℓ} (F : Set ℓ → Set ℓ) : Set (suc ℓ) where
  field
    rawFunctor : RawFunctor F
  open RawFunctor rawFunctor
  field
    <$>-id   : ∀ {A} (x : F A) → (id <$> x) ≡ x
    <$>-comp : ∀ {A B C} (f : A → B) (g : B → C) (x : F A)
             → (g ∘′ f) <$> x ≡ (_<$>_ g ∘′ _<$>_ f) x

record PropApplicative {ℓ} (F : Set ℓ → Set ℓ) : Set (suc ℓ) where
  field
    rawApplicative : RawApplicative F
  open RawApplicative rawApplicative
  field
    ⊛-id   : ∀ {A} (x : F A)
           → pure id ⊛ x ≡ x
    ⊛-comp : ∀ {A B C} (u : F (B → C)) (v : F (A → B)) (w : F A)
           → pure _∘′_ ⊛ u ⊛ v ⊛ w ≡ u ⊛ (v ⊛ w)
    ⊛-homo : ∀ {A B} (f : A → B) x
           → pure f ⊛ pure x ≡ pure (f x)
    ⊛-ichg : ∀ {A B} (u : F (A → B)) y
           → u ⊛ pure y ≡ pure (λ f → f y) ⊛ u

record PropMonad {ℓ} (F : Set ℓ → Set ℓ) : Set (suc ℓ) where
  field
    rawMonad : RawMonad F
  open RawMonad rawMonad
  field
    unitˡ : ∀ {A}     (m : F A)     → (m >>= return)   ≡ m
    unitʳ : ∀ {A B x} (f : A → F B) → (return x >>= f) ≡ f x
    >>=-assoc : ∀ {A B C} m (f : A → F B) (g : B → F C)
              → ((m >>= f) >>= g) ≡ (m >>= (λ x → f x >>= g))

propMonadMaybe : ∀ {ℓ} → PropMonad {ℓ} Maybe
propMonadMaybe {ℓ} = record
  { rawMonad = monadMaybe
  ; unitˡ = left-unit
  ; unitʳ = λ _ → refl
  ; >>=-assoc = assoc
  }
  where
    left-unit : ∀ {A : Set ℓ} (m : Maybe A)
              → maybe (λ x → just x) nothing m ≡ m
    left-unit (just x) = refl
    left-unit nothing = refl
    assoc : {A B C : Set ℓ} (m : Maybe A) (f : A → Maybe B) (g : B → Maybe C)
          → maybe′ g nothing (maybe f nothing m) ≡
            maybe′ (λ x → maybe g nothing (f x)) nothing m
    assoc (just x) _ _ = refl
    assoc nothing  _ _ = refl

propMonad→propApplicative : ∀ {ℓ} {F : Set ℓ → Set ℓ}
                          → PropMonad {ℓ} F → PropApplicative {ℓ} F
propMonad→propApplicative {ℓ} {F} mon = record
  { rawApplicative = RawIMonad.rawIApplicative (PropMonad.rawMonad mon)
  ; ⊛-id = app-id
  ; ⊛-comp = app-comp
  ; ⊛-homo = app-homo
  ; ⊛-ichg = app-ichg
  }
  where
    open RawMonad (PropMonad.rawMonad mon)
    open PropMonad mon
    app-id : ∀ {A} (x : F A) → pure id ⊛ x ≡ x
    app-id x = unitʳ _ ⟨ trans ⟩ unitˡ _

    app-comp : ∀ {A B C} (f : F (B → C)) (g : F (A → B)) (x : F A)
             → pure _∘′_ ⊛ f ⊛ g ⊛ x ≡ f ⊛ (g ⊛ x)
    app-comp f g x
      = >>=-assoc _ _ _ ⟨ trans ⟩
        >>=-assoc _ _ _ ⟨ trans ⟩
        unitʳ _         ⟨ trans ⟩
        >>=-assoc _ _ _ ⟨ trans ⟩
        cong (_>>=_ f)
          (ext $ λ f′ →
             unitʳ _                     ⟨ trans ⟩
             >>=-assoc _ _ _             ⟨ trans ⟩
             cong (_>>=_ g)
               (ext $ λ g′ →
                  unitʳ _                                     ⟨ trans ⟩
                  cong (_>>=_ x) (ext $ λ x′ → sym (unitʳ _)) ⟨ trans ⟩
                  sym (>>=-assoc _ _ _)) ⟨ trans ⟩
             sym (>>=-assoc _ _ _))

    app-homo : ∀ {A B} (f : A → B) (x : A)
             → pure f ⊛ pure x ≡ pure (f x)
    app-homo f x = unitʳ _ ⟨ trans ⟩ unitʳ _

    app-ichg : ∀ {A B} (u : F (A → B)) (y : A)
             → u ⊛ (pure y) ≡ pure (λ f → f y) ⊛ u
    app-ichg u y
      = cong (_>>=_ u) (ext $ λ u′ → unitʳ (pure ∘′ u′)) ⟨ trans ⟩
        sym (unitʳ _)

propMonad→propFunctor : ∀ {ℓ} {F : Set ℓ → Set ℓ}
                      → PropMonad F → PropFunctor F
propMonad→propFunctor {ℓ} {F} mon = record
  { rawFunctor = RawIApplicative.rawFunctor
                   (RawIMonad.rawIApplicative (PropMonad.rawMonad mon))
  ; <$>-id   = op-id
  ; <$>-comp = op-comp
  }
  where
    open RawMonad (PropMonad.rawMonad mon)
    open PropMonad mon
    op-id : ∀ {A : Set ℓ} (x : F A) → id  <$> x ≡ x
    op-id _ = unitʳ _ ⟨ trans ⟩ unitˡ _
    op-comp : ∀ {A B C : Set ℓ} (f : A → B) (g : B → C) (x : F A)
            → (g ∘′ f) <$> x ≡ (_<$>_ g ∘′ _<$>_ f) x
    op-comp f g x
      = unitʳ _                                    ⟨ trans ⟩
        cong (_>>=_ x) (ext $ λ _ → sym (unitʳ _)) ⟨ trans ⟩
        sym (unitʳ _         ⟨ trans ⟩
             >>=-assoc _ _ _ ⟨ trans ⟩
             unitʳ _         ⟨ trans ⟩
             >>=-assoc _ _ _)

propApplicative→propFunctor : ∀ {ℓ} {F : Set ℓ → Set ℓ}
                            → PropApplicative F → PropFunctor F
propApplicative→propFunctor {ℓ} {F} app = record
  { rawFunctor = RawIApplicative.rawFunctor
                   (PropApplicative.rawApplicative app)
  ; <$>-id = op-id
  ; <$>-comp = op-comp
  }
  where
    open RawApplicative (PropApplicative.rawApplicative app)
    open PropApplicative app
    op-id : ∀ {A} (x : F A) → (id <$> x) ≡ x
    op-id = ⊛-id

    op-comp : ∀ {A B C} (f : A → B) (g : B → C) (x : F A)
            → (g ∘′ f) <$> x ≡ (_<$>_ g ∘′ _<$>_ f) x
    op-comp f g x
      = cong (λ u → u ⊛ x)
          (sym (⊛-homo (λ z → z f) (_∘′_ g))                     ⟨ trans ⟩
           cong (_⊛_ (pure (λ f′ → f′ f))) (sym (⊛-homo _∘′_ g)) ⟨ trans ⟩
           sym (⊛-ichg _ f)) ⟨ trans ⟩
        ⊛-comp _ _ x

propApplicativeMaybe : ∀ {ℓ} → PropApplicative {ℓ} Maybe
propApplicativeMaybe = propMonad→propApplicative propMonadMaybe

propFunctorMaybe : ∀ {ℓ} → PropFunctor {ℓ} Maybe
propFunctorMaybe = propApplicative→propFunctor propApplicativeMaybe