[ new ] Monotone predicate monads instances

Identity, Reader, Error, State

Author: ajrouvoet

CHANGELOG.md

@@ -121,9 +121,14 @@ Other minor additions
   record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ)
   ```
 
-* Added new module `Category.Monad.Monotone`:
+* Added new modules `Category.Monad.Monotone(.*)`:
   ```agda
   record RawMPMonad (M : Pt I ℓ) : Set (suc ℓ)
+  Identity : Pt I i
+  record Identity
+  record ReaderMonad E (M : Pred I ℓ → Pt I ℓ) : Set (suc ℓ) where
+  record ErrorMonad (M : Pt I ℓ) : Set (suc ℓ) where
+  record StateMonad (M : Pt I ℓ) : Set (suc ℓ) where
   ```
 
 * Added new functions to `Codata.Colist`:

src/Category/Monad/Monotone/Error.agda

@@ -0,0 +1,48 @@
+open import Relation.Binary hiding (_⇒_)
+
+module Category.Monad.Monotone.Error {ℓ}(pre : Preorder ℓ ℓ ℓ)(Exc : Set ℓ) where
+
+open import Function
+open import Level hiding (lift)
+open import Data.Sum
+
+open import Relation.Unary
+open import Relation.Unary.Closure.Preorder pre
+open import Relation.Unary.PredicateTransformer
+
+open import Category.Monad.Monotone pre
+open import Category.Monad.Monotone.Identity pre
+
+open Preorder pre renaming (Carrier to I)
+
+ErrorT : Pt I ℓ → Pt I ℓ
+ErrorT M P = M (λ i → Exc ⊎ P i)
+
+Error = ErrorT Identity
+
+record ErrorMonad (M : Pt I ℓ) : Set (suc ℓ) where
+  field
+    throw      : ∀ {P i} → Exc → M P i
+    try_catch_ : ∀ {P}   → M P ⊆ (□ (const Exc ⇒ M P)) ⇒ M P
+
+module _ {M} (Mon : RawMPMonad M) where
+  private module M = RawMPMonad Mon
+
+  open RawMPMonad
+  errorT-monad : RawMPMonad (ErrorT M)
+  return errorT-monad px   = M.return (inj₂ px)
+  _≥=_   errorT-monad px f =
+    px M.≥= λ where
+      v (inj₁ e) → M.return (inj₁ e)
+      v (inj₂ x) → f v x
+
+  open ErrorMonad
+  errorT-monad-ops : ErrorMonad (ErrorT M)
+  throw      errorT-monad-ops e   = M.return (inj₁ e)
+  try_catch_ errorT-monad-ops c f =
+    c M.≥= λ where
+      v (inj₁ e) → f v e
+      v (inj₂ x) → M.return (inj₂ x)
+
+  lift-error : ∀ {P} → M P ⊆ ErrorT M P
+  lift-error x = x M.>>= (λ z → M.return (inj₂ z))

src/Category/Monad/Monotone/Identity.agda

@@ -0,0 +1,16 @@
+open import Relation.Binary
+
+module Category.Monad.Monotone.Identity {i}(pre : Preorder i i i) where
+
+open Preorder pre renaming (Carrier to I)
+
+open import Relation.Unary.PredicateTransformer using (Pt)
+open import Category.Monad.Monotone pre
+open RawMPMonad
+
+Identity : Pt I i
+Identity = λ P i → P i
+
+id-monad : RawMPMonad Identity
+return id-monad px = px
+_≥=_ id-monad c f = f refl c

src/Category/Monad/Monotone/Reader.agda

@@ -0,0 +1,54 @@
+open import Relation.Binary using (Preorder)
+
+module Category.Monad.Monotone.Reader {ℓ}(pre : Preorder ℓ ℓ ℓ) where
+
+open import Function
+open import Level
+
+open import Data.Product
+
+open import Relation.Unary.PredicateTransformer using (Pt)
+open import Relation.Unary
+open import Relation.Unary.Closure.Preorder pre
+
+open import Category.Monad
+open import Category.Monad.Monotone.Identity pre
+open import Category.Monad.Monotone pre
+
+open Preorder pre renaming (Carrier to I)
+open Closed ⦃...⦄
+
+ReaderT : Pred I ℓ → Pt I ℓ → Pt I ℓ
+ReaderT E M P = λ i → E i → M P i
+
+Reader : (Pred I ℓ) → Pt I ℓ
+Reader E = ReaderT E Identity
+
+record ReaderMonad E (M : Pred I ℓ → Pt I ℓ) : Set (suc ℓ) where
+  field
+    ask    : ∀ {i}    → M E E i
+    reader : ∀ {P}    → (E ⇒ P) ⊆ M E P
+    local  : ∀ {P E'} → (E ⇒ E') ⊆ (M E' P ⇒ M E P)
+
+  asks : ∀ {A} → (E ⇒ A) ⊆ M E A
+  asks = reader
+
+module _ {M : Pt I ℓ}(Mon : RawMPMonad M) where
+  private module M = RawMPMonad Mon
+
+  module _ {E}⦃ _ : Closed E ⦄ where
+    open RawMPMonad
+    reader-monad : RawMPMonad (ReaderT E M)
+    return reader-monad x e   = M.return x
+    _≥=_   reader-monad m f e =
+      m e M.≥= λ
+        i≤j px → f i≤j px (next e i≤j)
+
+    open ReaderMonad
+    reader-monad-ops : ReaderMonad E (λ E → ReaderT E M)
+    ask    reader-monad-ops e     = M.return e
+    reader reader-monad-ops f e   = M.return (f e)
+    local  reader-monad-ops f c e = c (f e)
+
+  lift-reader : ∀ {P} E → M P ⊆ ReaderT E M P
+  lift-reader _ z _ = z

src/Category/Monad/Monotone/State.agda

@@ -0,0 +1,48 @@
+open import Relation.Binary using (Preorder)
+
+module Category.Monad.Monotone.State {ℓ}(pre : Preorder ℓ ℓ ℓ)
+  (H : Preorder.Carrier pre → Set ℓ)
+  where
+
+open Preorder pre renaming (Carrier to I)
+
+open import Level
+open import Function
+open import Data.Product
+
+open import Relation.Unary
+open import Relation.Unary.PredicateTransformer using (Pt)
+open import Relation.Unary.Closure.Preorder pre
+
+open import Category.Monad
+open import Category.Monad.Monotone pre
+open import Category.Monad.Monotone.Identity pre
+
+MST : (Set ℓ → Set ℓ) → Pt I ℓ
+MST M P = H ⇒ (λ i → M (∃ λ j → i ∼ j × H j × P j))
+
+MSt : Pt I ℓ
+MSt = MST id
+
+record StateMonad (M : Pt I ℓ) : Set (suc ℓ) where
+  field
+    runState : ∀ {P} → □ (H ⇒ (H ∩ P)) ⊆ M P
+
+  get : ∀ {i} → M H i
+  get = runState λ _ μ → μ , μ
+
+module _ {M}(Mon : RawMonad {ℓ} M) where
+  private module M = RawMonad Mon
+
+  open RawMPMonad
+  mst-monad : RawMPMonad (MST M)
+  return mst-monad px  μ = M.return (_ , refl , μ , px)
+  _≥=_   mst-monad c f μ = c μ M.>>= λ where
+    (i₁ , ext₁ , μ₁ , pv) → (f ext₁ pv μ₁) M.>>= λ where
+      (i₂ , ext₂ , μ₂ , pw) → M.return (i₂ , trans ext₁ ext₂ , μ₂ , pw)
+
+  open StateMonad
+  mst-monad-ops : StateMonad (MST M)
+  runState (mst-monad-ops) f μ =
+    let (μ' , p) = f refl μ
+    in M.return (_ , refl , μ' , p)