[ new ] Monotone Predicate Monads

CHANGELOG.md

@@ -88,6 +88,8 @@ Other major changes
   generalization of the notion of "first element in the list to satisfy a
   predicate".
 
+* Added new modules `Data.List.Relation.Prefix.Heterogeneous(.Properties)`
+
 * Added new module `Data.Vec.Any.Properties`
 
 * Added new module `Relation.Binary.Properties.BoundedLattice`
@@ -119,6 +121,17 @@ Other minor additions
   record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ)
   ```
 
+* 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
+  record HeapMonad  (M : Pt I ℓ) : Set (suc ℓ) where
+  ```
+
 * Added new functions to `Codata.Colist`:
   ```agda
   fromCowriter : Cowriter W A i → Colist W i
@@ -161,6 +174,13 @@ Other minor additions
   mapM      : (Q ⊆ M ∘′ P) → All Q ⊆ (M ∘′ All P)
   forA      : All Q xs → (Q ⊆ F ∘′ P) → F (All P xs)
   forM      : All Q xs → (Q ⊆ M ∘′ P) → M (All P xs)
+
+  _++_      : ∀ {l m} → All P l → All P m → All P (l List.++ m)
+  _∷ʳ_      : ∀ {l : List A}{x} → All P l → P x → All P (l List.∷ʳ x)
+
+  updateAt  : ∀ {x xs} → x ∈ xs → (P x → P x) → All P xs → All P xs
+  _[_]%=_   : ∀ {x xs} → All P xs → x ∈ xs → (P x → P x) → All P xs
+  _[_]≔_    : ∀ {x xs} → All P xs → x ∈ xs → P x → All P xs
   ```
 
 * Added new operators to `Data.List.Base`:
@@ -175,9 +195,10 @@ Other minor additions
   respects : P Respects _≈_ → (All P) Respects _≋_
   ```
 
-* Added new proof to `Data.List.Membership.Propositional.Properties`:
+* Added new proofs to `Data.List.Membership.Propositional.Properties`:
   ```agda
   ∈-allFin : (k : Fin n) → k ∈ allFin n
+  []∈inits : [] ∈ inits as
   ```
 
 * Added new function to `Data.List.Membership.(Setoid/Propositional)`:
@@ -268,6 +289,7 @@ Other minor additions
   fromList⁻    : Any P (fromList xs) → List.Any P xs
   toList⁺      : Any P xs → List.Any P (toList xs)
   toList⁻      : List.Any P (toList xs) → Any P xs
+  prefix⁺      : ∀ {xs ys} → Prefix R xs ys → Any P xs → Any P ys
   ```
 
 * Added new functions to `Data.Vec.Membership.Propositional.Properties`:
@@ -281,6 +303,11 @@ Other minor additions
   wlog : Total _R_ → Symmetric Q → (∀ a b → a R b → Q a b) → ∀ a b → Q a b
   ```
 
+* Added new definition to `Relation.Binary.Core`:
+  ```agda
+  Antisym R S E = ∀ {i j} → R i j → S j i → E i j
+  ```
+
 * Added new proofs to `Relation.Binary.Lattice`:
   ```agda
   Lattice.setoid        : Setoid c ℓ

src/Category/Monad/Monotone.agda

@@ -0,0 +1,66 @@
+open import Relation.Binary using (Preorder)
+
+module Category.Monad.Monotone {ℓ}(pre : Preorder ℓ ℓ ℓ) where
+
+open Preorder pre renaming (Carrier to I)
+
+open import Level
+open import Function
+
+open import Data.Product hiding (map)
+
+open import Relation.Unary
+open import Relation.Unary.PredicateTransformer using (Pt)
+open import Relation.Unary.Closure.Preorder pre hiding (map)
+
+open import Category.Monad.Predicate
+
+open Closed ⦃...⦄
+
+record RawMPMonad (M : Pt I ℓ) : Set (suc ℓ) where
+
+  infixl 1 _≥=_
+  field
+    return : ∀ {P} → P ⊆ M P
+    _≥=_   : ∀ {P Q} → M P ⊆ (□ (P ⇒ M Q) ⇒ M Q)
+
+  {- predicate monad -}
+  module _ {P : Pred I ℓ} where
+
+    map : ∀ {Q} → M P ⊆ (□ (P ⇒ Q) ⇒ M Q)
+    map m f = m ≥= (λ w p → return (f w p))
+
+    _>>=_ : ∀ {Q : Pred I ℓ} → M P ⊆ (λ i → (P ⊆ M Q) → M Q i)
+    c >>= f = c ≥= λ i≤j pj → f pj
+
+    -- infix monadic strength
+    infixl 10 _^_
+    _^_ : ∀ {Q : Pred I ℓ}⦃ m : Closed Q ⦄ → M P ⊆ (Q ⇒ M (P ∩ Q))
+    c ^ qi = c ≥= λ {j} x≤j pj → return (pj , next qi x≤j)
+
+    -- prefix monadic strength; useful when Q cannot be inferred
+    ts : ∀ Q ⦃ m : Closed Q ⦄ → M P ⊆ (Q ⇒ M (P ∩ Q))
+    ts _ c qi = c ^ qi
+
+  pmonad : RawPMonad {ℓ = ℓ} M
+  pmonad = record
+    { return? = return
+    ; _=<?_ = λ f px → px >>= f }
+
+  {- sequencing -}
+  module _ {A : Set ℓ}{P : A → Pred I ℓ} ⦃ mp : ∀ {a} → Closed (P a) ⦄  where
+    open import Data.List.All
+
+    instance
+      _ = ∼-closed
+
+    sequence′ : ∀ {as}{i k} → i ∼ k →
+                All (λ a → □ (M (P a)) i) as → M (λ j → All (λ a → P a j) as) k
+    sequence′ _ [] = return []
+    sequence′ le (x ∷ xs) = do
+      px  , le  ← x le ^ le
+      pxs , px  ← sequence′ le xs ^ px
+      return (px ∷ pxs)
+
+    sequence : ∀ {as i} → All (λ a → □ (M (P a)) i) as → M (λ j → All (λ a → P a j) as) i
+    sequence = sequence′ refl

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/Heap.agda

@@ -0,0 +1,47 @@
+import Relation.Unary.Closure.Preorder as Closure
+open import Relation.Binary using (Preorder)
+
+module Category.Monad.Monotone.Heap
+  -- ordered heap types
+  {ℓ}(pre : Preorder ℓ ℓ ℓ)
+  -- types
+  (T : Set ℓ)
+  -- weakenable values
+  (V : T → Preorder.Carrier pre → Set ℓ) ⦃ wkV : ∀ {a} → Closure.Closed pre (V a) ⦄
+  -- heaps indexed by the heap type
+  (H : Preorder.Carrier pre → Set ℓ)
+  -- weakenable heap type membership
+  (_∈_ : T → Preorder.Carrier pre → Set ℓ) ⦃ wk∈ : ∀ {a} → Closure.Closed pre (_∈_ a) ⦄ where
+
+open Preorder pre renaming (Carrier to I)
+
+open import Level
+open import Data.Unit using (⊤; tt)
+open import Data.Product
+
+open import Relation.Unary hiding (_∈_)
+open import Relation.Unary.PredicateTransformer using (Pt)
+open import Relation.Unary.Closure.Preorder pre
+
+open import Category.Monad.Monotone pre
+open import Category.Monad.Monotone.State pre H
+
+open Closed ⦃...⦄
+
+record HeapMonad (M : Pt I ℓ) : Set (suc ℓ) where
+  field
+    super : StateMonad M
+
+  open StateMonad super public
+
+  field
+    store  : ∀ {a} → V a ⊆ M (λ W → a ∈ W)
+    modify : ∀ {a} → _∈_ a ⊆ V a ⇒ M (V a)
+    deref  : ∀ {a} → _∈_ a ⊆ M (V a)
+
+  module HeapMonadOps (m : RawMPMonad M) where
+    open RawMPMonad m
+    open import Data.List.All as All
+
+    storeₙ  : ∀ {W as} → All (λ a → V a W) as → M (λ W' → All (λ a → a ∈ W') as) W
+    storeₙ vs = sequence (All.map (λ v {x} ext → store (next v ext)) vs)

src/Category/Monad/Monotone/Heap/HList.agda

@@ -0,0 +1,75 @@
+-- An example implementation of the monotone HeapMonad
+-- using heterogeneous lists as a memory model.
+
+import Relation.Unary.Closure.Preorder as Closure
+import Relation.Binary.PropositionalEquality as P
+open import Data.List.Relation.Prefix.Setoid using (preorder)
+open import Data.List
+
+module Category.Monad.Monotone.Heap.HList
+  (T : Set)
+  (V : T → List T → Set)
+  ⦃ wkV : ∀ {a} → Closure.Closed (preorder (P.setoid T)) (V a) ⦄ where
+
+open import Function
+open import Data.Product
+open import Data.List.All as All
+open import Data.List.All.Properties
+open import Data.List.Any
+open import Data.List.Any.Properties
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Relation.Prefix.Heterogeneous
+import Data.List.Relation.Pointwise as PW
+
+open import Relation.Unary using (Pred)
+open import Relation.Binary using (Preorder)
+
+open import Category.Monad using (RawMonad)
+
+ord : Preorder _ _ _
+ord = preorder (P.setoid T)
+
+open Preorder ord renaming (refl to ∼-refl)
+open import Relation.Unary.Closure.Preorder ord
+open Closed ⦃...⦄
+
+instance
+  _ = ∼-closed
+
+  ∈-closed : ∀ {x} → Closed (x ∈_)
+  ∈-closed = record
+    { next = λ x∈xs xs∼ys → prefix⁺ (flip P.trans) xs∼ys x∈xs }
+
+  All-closed : ∀ {ys} → Closed (λ xs → All (λ y → V y xs) ys)
+  All-closed = record
+    { next = λ pys xs∼zs → All.map (λ p → next p xs∼zs) pys }
+
+HeapT : Set
+HeapT = List T
+
+Heap : Pred HeapT _
+Heap = λ W → All (λ a → V a W) W
+
+open import Category.Monad.Monotone ord
+open import Category.Monad.Monotone.State ord Heap
+open import Category.Monad.Monotone.Heap ord T V Heap _∈_
+
+module _ {M : Set → Set}(mon : RawMonad M) where
+  private module M = RawMonad mon
+
+  open HeapMonad
+  hlist-heap-monad : HeapMonad (MST M)
+  super  hlist-heap-monad             = mst-monad-ops mon
+  store  hlist-heap-monad {x}{xs} v μ =
+    let ext = fromView (PW.refl P.refl PrefixView.++ [ x ])
+    in M.return (
+      xs ∷ʳ x ,
+      ext ,
+      ∷ʳ⁺ (next μ ext) (next v ext) ,
+      ++⁺ʳ xs (here P.refl))
+  modify hlist-heap-monad ptr v μ     =
+    M.return (-, ∼-refl , μ [ ptr ]≔ v , All.lookup μ ptr)
+  deref  hlist-heap-monad ptr μ       =
+    M.return (-, ∼-refl , μ , All.lookup μ ptr)
+
+  open HeapMonadOps hlist-heap-monad public

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