[ new ] Monotone Heap Monad

Includes a necessary Any property.

Author: ajrouvoet

CHANGELOG.md

@@ -129,6 +129,7 @@ Other minor additions
   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`:
@@ -288,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`:

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.Heterogeneous.Properties 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.isEquivalence) (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 {A = T} P.isEquivalence)
+
+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/Data/List/Any/Properties.agda

@@ -579,3 +579,15 @@ module _ {ℓ} {A B : Set ℓ} where
     (Any P xs × Any Q ys)                    ↔⟨ ×↔ ⟩
     Any (λ x → Any (λ y → P x × Q y) ys) xs  ↔⟨ ⊗↔ ⟩
     Any (P ⟨×⟩ Q) (xs ⊗ ys)                  ∎
+
+------------------------------------------------------------------------
+-- Prefix
+
+module _ {a r p} {A : Set a} {R : Rel A r} {P : Pred A p}
+         (resp : P Respects R) where
+
+ open import Data.List.Relation.Prefix.Heterogeneous as Prefix
+
+ prefix⁺ : ∀ {xs ys} → Prefix R xs ys → Any P xs → Any P ys
+ prefix⁺ rs e with toView rs
+ prefix⁺ rs e | ss Prefix.++ ts = ++⁺ˡ (lift-resp resp ss e)