[ add ] partial elements in Effect.Monad.Partial module

CHANGELOG.md

@@ -270,6 +270,8 @@ New modules
   Data.Tree.Rose.Show
   ```
 
+* `Effect.Monad.Partial` based on domain `Dom` and injection `dom`.
+
 Additions to existing modules
 -----------------------------
 

src/Effect/Monad/Partial.agda

@@ -0,0 +1,63 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The partial monad cf. https://1lab.dev/Data.Partial.Base.html
+--
+-- Modulo proof-relevance, this defines the free pointed DCPO,
+-- whereas delay-like monads, as in `Effect.Monad.Partiality`,
+-- are aiming to define the free ωCPO.
+-- NB. in each case, there are additional 'up to' considerations
+-- wrt 'appropriate' setoid equality/quotient/bisimilarity.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Effect.Monad.Partial where
+
+open import Level using (Level; suc; zero;_⊔_)
+open import Data.Product using (_×_; Σ; Σ-syntax; _,_)
+open import Data.Empty.Polymorphic using (⊥-elim; ⊥)
+open import Data.Unit.Polymorphic using (⊤)
+
+private
+  variable
+    a ℓ ℓ' : Level
+    A B : Set a
+
+
+------------------------------------------------------------------------
+-- Object part: type definition
+
+record ↯ (A : Set a) (ℓ : Level) : Set (a ⊔ suc ℓ) where
+  field
+    Dom : Set ℓ
+    dom : Dom → A
+
+open ↯
+
+------------------------------------------------------------------------
+-- Arrow part: Functor, Applicative, Monad component definition
+
+↯-map : (A → B) → ↯ A ℓ → ↯ B ℓ
+↯-map f a↯ .Dom = a↯ .Dom
+↯-map f a↯ .dom d = f (a↯ .dom d)
+
+↯-ap : ↯ (A → B) ℓ → ↯ A ℓ' → ↯ B (ℓ ⊔ ℓ')
+↯-ap a→b↯ a↯ .Dom = a→b↯ .Dom × a↯ .Dom
+↯-ap a→b↯ a↯ .dom (f↓ , a↓) = a→b↯ .dom f↓ (a↯ .dom a↓)
+
+↯-bind : ↯ A ℓ → (A → ↯ B ℓ') → ↯ B (ℓ ⊔ ℓ')
+↯-bind a↯ f .Dom = Σ[ a↓ ∈ a↯ .Dom ] f (a↯ .dom a↓) .Dom
+↯-bind a↯ f .dom (a↓ , fa↓) = f (a↯ .dom a↓) .dom fa↓
+
+------------------------------------------------------------------------
+-- Specific constructions
+
+never : ↯ A ℓ
+never {ℓ = ℓ} .Dom = ⊥ {ℓ = ℓ}
+never .dom = ⊥-elim
+
+always : A → ↯ A ℓ
+always {ℓ = ℓ} a .Dom = ⊤ {ℓ = ℓ}
+always a .dom _ = a
+