[ refactor ] Make Data.Irrelevant.Irrelevant a proper Monad

CHANGELOG.md

@@ -24,6 +24,12 @@ Non-backwards compatible changes
 Minor improvements
 ------------------
 
+* The function `Data.Irrelevant._>>=_` now has the correct type for a 'bind'
+  operation of a `Monad`, by moving the property `irrelevant-recompute`
+  from `Relation.Nullary.Recomputable` to `Data.Irrelevant` as `recompute`,
+  and re-exporting it from the former module with the old name. This should
+  be backwards compatible.
+
 * The function `Data.Nat.LCG.step` is now a manifest field of the record type
   `Generator`, as per the discussion on #2936 and upstream issues/PRs. This is
   consistent with a minimal API for such LCGs, and should be backwards compatible.
@@ -94,6 +100,13 @@ Deprecated names
   ¬∀⟶∃¬-          ↦   ¬∀⇒∃¬
   ```
 
+* In `Data.Irrelevant`:
+  ```agda
+  _$∙⁺_     : (.A → B) → Irrelevant A → B
+  _$∙⁻_     : (Irrelevant A → B) → .A → B
+  recompute : Recomputable (Irrelevant A)
+  ```
+
 * In `Data.List.Fresh.Membership.Setoid.Properties`:
   ```agda
   ≈-subst-∈   ↦   ∈-resp-≈

src/Data/Irrelevant.agda

@@ -14,6 +14,7 @@
 module Data.Irrelevant where
 
 open import Level using (Level)
+open import Relation.Nullary.Recomputable.Core using (Recomputable)
 
 private
   variable
@@ -31,7 +32,25 @@ record Irrelevant (A : Set a) : Set a where
 open Irrelevant public
 
 ------------------------------------------------------------------------
--- Algebraic structure: Functor, Appplicative and Monad-like
+-- Relationship with the . modality: wrapped/unwrapped application
+
+infixr -1 _$∙⁺_ _$∙⁻_
+
+_$∙⁺_ : (.A → B) → Irrelevant A → B
+f $∙⁺ [ a ] = f a
+{-# INLINE _$∙⁺_ #-}
+
+_$∙⁻_ : (Irrelevant A → B) → .A → B
+f $∙⁻ a = f [ a ]
+{-# INLINE _$∙⁻_ #-}
+
+-- Irrelevant types are Recomputable
+
+recompute : Recomputable (Irrelevant A)
+irrelevant (recompute [ a ]) = a
+
+------------------------------------------------------------------------
+-- Algebraic structure: Functor, Appplicative and Monad
 
 map : (A → B) → Irrelevant A → Irrelevant B
 map f [ a ] = [ f a ]
@@ -44,8 +63,8 @@ _<*>_ : Irrelevant (A → B) → Irrelevant A → Irrelevant B
 [ f ] <*> [ a ] = [ f a ]
 
 infixl 1 _>>=_
-_>>=_ : Irrelevant A → (.A → Irrelevant B) → Irrelevant B
-[ a ] >>= f = f a
+_>>=_ : Irrelevant A → (A → Irrelevant B) → Irrelevant B
+[ a ] >>= f = recompute (f a)
 
 ------------------------------------------------------------------------
 -- Other functions

src/Relation/Nullary/Recomputable.agda

@@ -9,7 +9,6 @@
 module Relation.Nullary.Recomputable where
 
 open import Data.Empty using (⊥)
-open import Data.Irrelevant using (Irrelevant; irrelevant; [_])
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Level using (Level)
 open import Relation.Nullary.Negation.Core using (¬_)
@@ -21,20 +20,17 @@ private
     B : Set b
 
 ------------------------------------------------------------------------
--- Re-export
+-- Re-export core definitions
 
 open import Relation.Nullary.Recomputable.Core public
 
-
-------------------------------------------------------------------------
--- Constructions
-
 -- Irrelevant types are Recomputable
 
-irrelevant-recompute : Recomputable (Irrelevant A)
-irrelevant (irrelevant-recompute [ a ]) = a
+open import Data.Irrelevant public
+  using () renaming (recompute to irrelevant-recompute)
 
--- Corollary: so too is ⊥
+------------------------------------------------------------------------
+-- Constructions
 
 ⊥-recompute : Recomputable ⊥
 ⊥-recompute = irrelevant-recompute