From 67094341fae6c48c36665f962b3cae8bdcc0497d Mon Sep 17 00:00:00 2001 From: e-mniang Date: Wed, 30 Jul 2025 13:29:08 -0400 Subject: [PATCH 01/16] Starting --- src/partialMapClassifierDraft.agda | 63 ++++++++++++++++++++++++++++++ 1 file changed, 63 insertions(+) create mode 100644 src/partialMapClassifierDraft.agda diff --git a/src/partialMapClassifierDraft.agda b/src/partialMapClassifierDraft.agda new file mode 100644 index 0000000000..ef774fb7e4 --- /dev/null +++ b/src/partialMapClassifierDraft.agda @@ -0,0 +1,63 @@ +module partialMapClassifierDraft where + +open import Level + +open import Data.Product +open import Data.Empty +open import Data.Unit +open import Relation.Binary.PropositionalEquality +open import Function.Bundles using (_↔_; Inverse) + +-- The type of partial elements +record ↯ {ℓ} (A : Set ℓ) (ℓ' : Level) : Set (ℓ ⊔ suc ℓ') where + field + Dom : Set ℓ' + elt : Dom → A + +open ↯ + +private variable + ℓ ℓ' : Level + A B : Set ℓ + + +-- Examples : +never : ↯ A zero +never .Dom = ⊥ +never .elt = ⊥-elim + +always : A → ↯ A zero +always a .Dom = ⊤ +always a .elt _ = a + +-- The bind propertie +bind : ↯ A ℓ → (A → ↯ B ℓ') → ↯ B (ℓ ⊔ ℓ') +bind a↯ f .Dom = Σ[ a↓ ∈ a↯ .Dom ] f (a↯ .elt a↓) .Dom +bind a↯ f .elt (a↓ , fa↓) = f (a↯ .elt a↓) .elt fa↓ + +-- +part-map : (A → B) → ↯ A ℓ → ↯ B ℓ +part-map f a↯ .Dom = a↯ .Dom +part-map f a↯ .elt d = f (a↯ .elt d) + +-- +part-ap : ↯ (A → B) ℓ → ↯ A ℓ → ↯ B ℓ +part-ap a→b↯ a↯ .Dom = a→b↯ .Dom × a↯ .Dom +part-ap a→b↯ a↯ .elt (f↓ , a↓) = a→b↯ .elt f↓ (a↯ .elt a↓) + +-- With different level : +part-ap-diff : ↯ (A → B) ℓ → ↯ A ℓ' → ↯ B (ℓ ⊔ ℓ') +part-ap-diff a→b↯ a↯ .Dom = a→b↯ .Dom × a↯ .Dom +part-ap-diff a→b↯ a↯ .elt (f↓ , a↓) = a→b↯ .elt f↓ (a↯ .elt a↓) + +------------------------------------------------------------------------ + +-- Extensionality for partial maps +part-ext : {A : Set ℓ} {x y : ↯ A ℓ'} + → (iso : x .Dom ↔ y .Dom) + → (∀ (xd : x .Dom) → x .elt xd ≡ y .elt (Inverse.to iso xd)) + → x ≡ y +part-ext = {! !} + + + From 8cdf3e106efb09b001d66d53b0cd06337da7004a Mon Sep 17 00:00:00 2001 From: e-mniang Date: Wed, 30 Jul 2025 15:32:35 -0400 Subject: [PATCH 02/16] modif path --- src/Effect/Monad/Partial.agda | 46 ++++++++++++++++++++++ src/partialMapClassifierDraft.agda | 63 ------------------------------ 2 files changed, 46 insertions(+), 63 deletions(-) create mode 100644 src/Effect/Monad/Partial.agda delete mode 100644 src/partialMapClassifierDraft.agda diff --git a/src/Effect/Monad/Partial.agda b/src/Effect/Monad/Partial.agda new file mode 100644 index 0000000000..0b7b3f7150 --- /dev/null +++ b/src/Effect/Monad/Partial.agda @@ -0,0 +1,46 @@ +module Partial where + +open import Level + +open import Data.Product +open import Data.Empty +open import Data.Unit + +-- The type of partial elements +record ↯ {ℓ} (A : Set ℓ) (ℓ' : Level) : Set (ℓ ⊔ suc ℓ') where + field + Dom : Set ℓ' + elt : Dom → A + +open ↯ + +private variable + ℓ ℓ' : Level + A B : Set ℓ + + +-- +never : ↯ A zero +never .Dom = ⊥ +never .elt = ⊥-elim + +always : A → ↯ A zero +always a .Dom = ⊤ +always a .elt _ = a + +----------------------- +↯-bind : ↯ A ℓ → (A → ↯ B ℓ') → ↯ B (ℓ ⊔ ℓ') +↯-bind a↯ f .Dom = Σ[ a↓ ∈ a↯ .Dom ] f (a↯ .elt a↓) .Dom +↯-bind a↯ f .elt (a↓ , fa↓) = f (a↯ .elt a↓) .elt fa↓ + +----------------------- +↯-map : (A → B) → ↯ A ℓ → ↯ B ℓ +↯-map f a↯ .Dom = a↯ .Dom +↯-map f a↯ .elt d = f (a↯ .elt d) + +----------------------- +↯-ap : ↯ (A → B) ℓ → ↯ A ℓ' → ↯ B (ℓ ⊔ ℓ') +↯-ap a→b↯ a↯ .Dom = a→b↯ .Dom × a↯ .Dom +↯-ap a→b↯ a↯ .elt (f↓ , a↓) = a→b↯ .elt f↓ (a↯ .elt a↓) + + diff --git a/src/partialMapClassifierDraft.agda b/src/partialMapClassifierDraft.agda deleted file mode 100644 index ef774fb7e4..0000000000 --- a/src/partialMapClassifierDraft.agda +++ /dev/null @@ -1,63 +0,0 @@ -module partialMapClassifierDraft where - -open import Level - -open import Data.Product -open import Data.Empty -open import Data.Unit -open import Relation.Binary.PropositionalEquality -open import Function.Bundles using (_↔_; Inverse) - --- The type of partial elements -record ↯ {ℓ} (A : Set ℓ) (ℓ' : Level) : Set (ℓ ⊔ suc ℓ') where - field - Dom : Set ℓ' - elt : Dom → A - -open ↯ - -private variable - ℓ ℓ' : Level - A B : Set ℓ - - --- Examples : -never : ↯ A zero -never .Dom = ⊥ -never .elt = ⊥-elim - -always : A → ↯ A zero -always a .Dom = ⊤ -always a .elt _ = a - --- The bind propertie -bind : ↯ A ℓ → (A → ↯ B ℓ') → ↯ B (ℓ ⊔ ℓ') -bind a↯ f .Dom = Σ[ a↓ ∈ a↯ .Dom ] f (a↯ .elt a↓) .Dom -bind a↯ f .elt (a↓ , fa↓) = f (a↯ .elt a↓) .elt fa↓ - --- -part-map : (A → B) → ↯ A ℓ → ↯ B ℓ -part-map f a↯ .Dom = a↯ .Dom -part-map f a↯ .elt d = f (a↯ .elt d) - --- -part-ap : ↯ (A → B) ℓ → ↯ A ℓ → ↯ B ℓ -part-ap a→b↯ a↯ .Dom = a→b↯ .Dom × a↯ .Dom -part-ap a→b↯ a↯ .elt (f↓ , a↓) = a→b↯ .elt f↓ (a↯ .elt a↓) - --- With different level : -part-ap-diff : ↯ (A → B) ℓ → ↯ A ℓ' → ↯ B (ℓ ⊔ ℓ') -part-ap-diff a→b↯ a↯ .Dom = a→b↯ .Dom × a↯ .Dom -part-ap-diff a→b↯ a↯ .elt (f↓ , a↓) = a→b↯ .elt f↓ (a↯ .elt a↓) - ------------------------------------------------------------------------- - --- Extensionality for partial maps -part-ext : {A : Set ℓ} {x y : ↯ A ℓ'} - → (iso : x .Dom ↔ y .Dom) - → (∀ (xd : x .Dom) → x .elt xd ≡ y .elt (Inverse.to iso xd)) - → x ≡ y -part-ext = {! !} - - - From 55a34ee34ff2e1ec9dca1740830605a3207f689f Mon Sep 17 00:00:00 2001 From: e-mniang Date: Wed, 30 Jul 2025 15:34:28 -0400 Subject: [PATCH 03/16] correction --- src/Effect/Monad/Partial.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Effect/Monad/Partial.agda b/src/Effect/Monad/Partial.agda index 0b7b3f7150..62a49d066e 100644 --- a/src/Effect/Monad/Partial.agda +++ b/src/Effect/Monad/Partial.agda @@ -1,4 +1,4 @@ -module Partial where +module Effect.Monad.Partial where open import Level From c9c4dbe8e8cbf588c3c3529baa9eb0c42cef3345 Mon Sep 17 00:00:00 2001 From: e-mniang Date: Wed, 30 Jul 2025 21:02:09 -0400 Subject: [PATCH 04/16] formating file --- src/Effect/Monad/Partial.agda | 33 +++++++++++++++++++-------------- 1 file changed, 19 insertions(+), 14 deletions(-) diff --git a/src/Effect/Monad/Partial.agda b/src/Effect/Monad/Partial.agda index 62a49d066e..3ea44fd7fa 100644 --- a/src/Effect/Monad/Partial.agda +++ b/src/Effect/Monad/Partial.agda @@ -1,12 +1,26 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The partial monad +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + module Effect.Monad.Partial where -open import Level +open import Level using (Level; suc; zero;_⊔_) +open import Data.Product using (_×_; Σ; Σ-syntax; _,_) +open import Data.Empty using (⊥-elim; ⊥) +open import Data.Unit using (⊤) + +private + variable + ℓ ℓ' : Level + A B : Set ℓ -open import Data.Product -open import Data.Empty -open import Data.Unit +------------------------------------------------------------------------ +-- The partial monad --- The type of partial elements record ↯ {ℓ} (A : Set ℓ) (ℓ' : Level) : Set (ℓ ⊔ suc ℓ') where field Dom : Set ℓ' @@ -14,12 +28,6 @@ record ↯ {ℓ} (A : Set ℓ) (ℓ' : Level) : Set (ℓ ⊔ suc ℓ') where open ↯ -private variable - ℓ ℓ' : Level - A B : Set ℓ - - --- never : ↯ A zero never .Dom = ⊥ never .elt = ⊥-elim @@ -28,17 +36,14 @@ always : A → ↯ A zero always a .Dom = ⊤ always a .elt _ = a ------------------------ ↯-bind : ↯ A ℓ → (A → ↯ B ℓ') → ↯ B (ℓ ⊔ ℓ') ↯-bind a↯ f .Dom = Σ[ a↓ ∈ a↯ .Dom ] f (a↯ .elt a↓) .Dom ↯-bind a↯ f .elt (a↓ , fa↓) = f (a↯ .elt a↓) .elt fa↓ ------------------------ ↯-map : (A → B) → ↯ A ℓ → ↯ B ℓ ↯-map f a↯ .Dom = a↯ .Dom ↯-map f a↯ .elt d = f (a↯ .elt d) ------------------------ ↯-ap : ↯ (A → B) ℓ → ↯ A ℓ' → ↯ B (ℓ ⊔ ℓ') ↯-ap a→b↯ a↯ .Dom = a→b↯ .Dom × a↯ .Dom ↯-ap a→b↯ a↯ .elt (f↓ , a↓) = a→b↯ .elt f↓ (a↯ .elt a↓) From ddbe9017033ef2d4f9716ff49a150ac43f07b3a4 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Wed, 27 Aug 2025 11:26:40 -0400 Subject: [PATCH 05/16] Update src/Effect/Monad/Partial.agda Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- src/Effect/Monad/Partial.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Effect/Monad/Partial.agda b/src/Effect/Monad/Partial.agda index 3ea44fd7fa..29f5108a27 100644 --- a/src/Effect/Monad/Partial.agda +++ b/src/Effect/Monad/Partial.agda @@ -15,8 +15,8 @@ open import Data.Unit using (⊤) private variable - ℓ ℓ' : Level - A B : Set ℓ + a ℓ ℓ' : Level + A B : Set a ------------------------------------------------------------------------ -- The partial monad From 52760d9f3ad8a63a36f947b09a5198b7766ec573 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Wed, 27 Aug 2025 11:26:58 -0400 Subject: [PATCH 06/16] Update src/Effect/Monad/Partial.agda Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- src/Effect/Monad/Partial.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Effect/Monad/Partial.agda b/src/Effect/Monad/Partial.agda index 29f5108a27..98a7afbaf2 100644 --- a/src/Effect/Monad/Partial.agda +++ b/src/Effect/Monad/Partial.agda @@ -21,7 +21,7 @@ private ------------------------------------------------------------------------ -- The partial monad -record ↯ {ℓ} (A : Set ℓ) (ℓ' : Level) : Set (ℓ ⊔ suc ℓ') where +record ↯ (A : Set a) (ℓ : Level) : Set (a ⊔ suc ℓ) where field Dom : Set ℓ' elt : Dom → A From 802df520775ccde3f43c02633616e4b2f06a4485 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Wed, 27 Aug 2025 11:27:08 -0400 Subject: [PATCH 07/16] Update src/Effect/Monad/Partial.agda Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- src/Effect/Monad/Partial.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Effect/Monad/Partial.agda b/src/Effect/Monad/Partial.agda index 98a7afbaf2..df29574b38 100644 --- a/src/Effect/Monad/Partial.agda +++ b/src/Effect/Monad/Partial.agda @@ -23,7 +23,7 @@ private record ↯ (A : Set a) (ℓ : Level) : Set (a ⊔ suc ℓ) where field - Dom : Set ℓ' + Dom : Set ℓ elt : Dom → A open ↯ From 8c13420e636d748e79bf505e61e0cf3bcd119425 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Tue, 7 Jul 2026 11:06:56 +0100 Subject: [PATCH 08/16] refactor: make `always` and `never` more `Level`-polymorphic --- src/Effect/Monad/Partial.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Effect/Monad/Partial.agda b/src/Effect/Monad/Partial.agda index df29574b38..df08a0cf45 100644 --- a/src/Effect/Monad/Partial.agda +++ b/src/Effect/Monad/Partial.agda @@ -10,8 +10,8 @@ module Effect.Monad.Partial where open import Level using (Level; suc; zero;_⊔_) open import Data.Product using (_×_; Σ; Σ-syntax; _,_) -open import Data.Empty using (⊥-elim; ⊥) -open import Data.Unit using (⊤) +open import Data.Empty.Polymorphic using (⊥-elim; ⊥) +open import Data.Unit.Polymorphic using (⊤) private variable From b56734c6a535a65c48e974553a6343d3aab6116d Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Tue, 7 Jul 2026 11:10:36 +0100 Subject: [PATCH 09/16] refactor: make `always` more `Level`-polymorphic --- src/Effect/Monad/Partial.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Effect/Monad/Partial.agda b/src/Effect/Monad/Partial.agda index df08a0cf45..31e2f09ec2 100644 --- a/src/Effect/Monad/Partial.agda +++ b/src/Effect/Monad/Partial.agda @@ -32,8 +32,8 @@ never : ↯ A zero never .Dom = ⊥ never .elt = ⊥-elim -always : A → ↯ A zero -always a .Dom = ⊤ +always : A → ↯ A ℓ +always {ℓ = ℓ} a .Dom = ⊤ {ℓ = ℓ} always a .elt _ = a ↯-bind : ↯ A ℓ → (A → ↯ B ℓ') → ↯ B (ℓ ⊔ ℓ') From 0be417fab63b42a7a009d528519d92a202d9df57 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Tue, 7 Jul 2026 11:11:17 +0100 Subject: [PATCH 10/16] refactor: make `never` more `Level`-polymorphic --- src/Effect/Monad/Partial.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Effect/Monad/Partial.agda b/src/Effect/Monad/Partial.agda index 31e2f09ec2..ff81342d15 100644 --- a/src/Effect/Monad/Partial.agda +++ b/src/Effect/Monad/Partial.agda @@ -28,8 +28,8 @@ record ↯ (A : Set a) (ℓ : Level) : Set (a ⊔ suc ℓ) where open ↯ -never : ↯ A zero -never .Dom = ⊥ +never : ↯ A ℓ +never {ℓ = ℓ} .Dom = ⊥ {ℓ = ℓ} never .elt = ⊥-elim always : A → ↯ A ℓ From cbd14d1c7c398c171c354085feaa089c89952afa Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 7 Jul 2026 11:17:42 +0100 Subject: [PATCH 11/16] fix: whitespace --- src/Effect/Monad/Partial.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Effect/Monad/Partial.agda b/src/Effect/Monad/Partial.agda index ff81342d15..0d925a8d8f 100644 --- a/src/Effect/Monad/Partial.agda +++ b/src/Effect/Monad/Partial.agda @@ -13,7 +13,7 @@ open import Data.Product using (_×_; Σ; Σ-syntax; _,_) open import Data.Empty.Polymorphic using (⊥-elim; ⊥) open import Data.Unit.Polymorphic using (⊤) -private +private variable a ℓ ℓ' : Level A B : Set a @@ -48,4 +48,3 @@ always a .elt _ = a ↯-ap a→b↯ a↯ .Dom = a→b↯ .Dom × a↯ .Dom ↯-ap a→b↯ a↯ .elt (f↓ , a↓) = a→b↯ .elt f↓ (a↯ .elt a↓) - From 2e36476f7f13b31a1c2aaeafcebc6be978b0caee Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 7 Jul 2026 11:26:28 +0100 Subject: [PATCH 12/16] refactor: code motion plus commentary --- src/Effect/Monad/Partial.agda | 30 ++++++++++++++++++------------ 1 file changed, 18 insertions(+), 12 deletions(-) diff --git a/src/Effect/Monad/Partial.agda b/src/Effect/Monad/Partial.agda index 0d925a8d8f..e7eb42b883 100644 --- a/src/Effect/Monad/Partial.agda +++ b/src/Effect/Monad/Partial.agda @@ -19,7 +19,7 @@ private A B : Set a ------------------------------------------------------------------------ --- The partial monad +-- Object part: type definition record ↯ (A : Set a) (ℓ : Level) : Set (a ⊔ suc ℓ) where field @@ -28,17 +28,8 @@ record ↯ (A : Set a) (ℓ : Level) : Set (a ⊔ suc ℓ) where open ↯ -never : ↯ A ℓ -never {ℓ = ℓ} .Dom = ⊥ {ℓ = ℓ} -never .elt = ⊥-elim - -always : A → ↯ A ℓ -always {ℓ = ℓ} a .Dom = ⊤ {ℓ = ℓ} -always a .elt _ = a - -↯-bind : ↯ A ℓ → (A → ↯ B ℓ') → ↯ B (ℓ ⊔ ℓ') -↯-bind a↯ f .Dom = Σ[ a↓ ∈ a↯ .Dom ] f (a↯ .elt a↓) .Dom -↯-bind a↯ f .elt (a↓ , fa↓) = f (a↯ .elt a↓) .elt fa↓ +------------------------------------------------------------------------ +-- Arrow part: Functor, Applicative, Monad component definition ↯-map : (A → B) → ↯ A ℓ → ↯ B ℓ ↯-map f a↯ .Dom = a↯ .Dom @@ -48,3 +39,18 @@ always a .elt _ = a ↯-ap a→b↯ a↯ .Dom = a→b↯ .Dom × a↯ .Dom ↯-ap a→b↯ a↯ .elt (f↓ , a↓) = a→b↯ .elt f↓ (a↯ .elt a↓) +↯-bind : ↯ A ℓ → (A → ↯ B ℓ') → ↯ B (ℓ ⊔ ℓ') +↯-bind a↯ f .Dom = Σ[ a↓ ∈ a↯ .Dom ] f (a↯ .elt a↓) .Dom +↯-bind a↯ f .elt (a↓ , fa↓) = f (a↯ .elt a↓) .elt fa↓ + +------------------------------------------------------------------------ +-- Specific constructions + +never : ↯ A ℓ +never {ℓ = ℓ} .Dom = ⊥ {ℓ = ℓ} +never .elt = ⊥-elim + +always : A → ↯ A ℓ +always {ℓ = ℓ} a .Dom = ⊤ {ℓ = ℓ} +always a .elt _ = a + From 055268f960ea09ff3e350dfbce45bc0f88c6427b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 7 Jul 2026 11:27:46 +0100 Subject: [PATCH 13/16] refactor: rename `elt` to `dom` --- src/Effect/Monad/Partial.agda | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/Effect/Monad/Partial.agda b/src/Effect/Monad/Partial.agda index e7eb42b883..adbd3cf60d 100644 --- a/src/Effect/Monad/Partial.agda +++ b/src/Effect/Monad/Partial.agda @@ -24,7 +24,7 @@ private record ↯ (A : Set a) (ℓ : Level) : Set (a ⊔ suc ℓ) where field Dom : Set ℓ - elt : Dom → A + dom : Dom → A open ↯ @@ -33,24 +33,24 @@ open ↯ ↯-map : (A → B) → ↯ A ℓ → ↯ B ℓ ↯-map f a↯ .Dom = a↯ .Dom -↯-map f a↯ .elt d = f (a↯ .elt d) +↯-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↯ .elt (f↓ , a↓) = a→b↯ .elt f↓ (a↯ .elt a↓) +↯-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↯ .elt a↓) .Dom -↯-bind a↯ f .elt (a↓ , fa↓) = f (a↯ .elt a↓) .elt fa↓ +↯-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 .elt = ⊥-elim +never .dom = ⊥-elim always : A → ↯ A ℓ always {ℓ = ℓ} a .Dom = ⊤ {ℓ = ℓ} -always a .elt _ = a +always a .dom _ = a From a01ecc7ad24c605d073b26e72aacde40dd782875 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 7 Jul 2026 11:31:50 +0100 Subject: [PATCH 14/16] fix: `without-K`! --- src/Effect/Monad/Partial.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Effect/Monad/Partial.agda b/src/Effect/Monad/Partial.agda index adbd3cf60d..1e86bf5595 100644 --- a/src/Effect/Monad/Partial.agda +++ b/src/Effect/Monad/Partial.agda @@ -4,7 +4,7 @@ -- The partial monad ------------------------------------------------------------------------ -{-# OPTIONS --cubical-compatible --safe #-} +{-# OPTIONS --without-K --safe #-} module Effect.Monad.Partial where From 890bc1461632e8616ffc4a32dd0a83cc28354ecd Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 7 Jul 2026 11:34:29 +0100 Subject: [PATCH 15/16] add: `CHANGELOG` entry --- CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2ebee679df..9564fa037c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -35,6 +35,8 @@ Deprecated names New modules ----------- +* `Effect.Monad.Partial` based on domain `Dom` and injection `dom`. + Additions to existing modules ----------------------------- From 972d26c409409a30cd68ff24255be881030076fd Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 7 Jul 2026 17:44:34 +0100 Subject: [PATCH 16/16] add: a version of Reed's commentary --- src/Effect/Monad/Partial.agda | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/Effect/Monad/Partial.agda b/src/Effect/Monad/Partial.agda index 1e86bf5595..2759c6272c 100644 --- a/src/Effect/Monad/Partial.agda +++ b/src/Effect/Monad/Partial.agda @@ -1,7 +1,13 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- The partial monad +-- 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 #-} @@ -18,6 +24,7 @@ private a ℓ ℓ' : Level A B : Set a + ------------------------------------------------------------------------ -- Object part: type definition