Monadic join (#2079)

Author: jamesmckinna

CHANGELOG.md

@@ -692,6 +692,9 @@ Non-backwards compatible changes
   This reorganisation means in particular that the functor/applicative of a monad
   are not computed using `_>>=_`. This may break proofs.
 
+* When `F : Set f → Set f` we moreover have a definable join/μ operator
+  `join : (M : RawMonad F) → F (F A) → F A`.
+
 * We now have `RawEmpty` and `RawChoice` respectively packing `empty : M A` and
   `(<|>) : M A → M A → M A`. `RawApplicativeZero`, `RawAlternative`, `RawMonadZero`,
   `RawMonadPlus` are all defined in terms of these.
@@ -2604,14 +2607,13 @@ Other minor changes
 
   diagonal           : Vec (Vec A n) n → Vec A n
   DiagonalBind._>>=_ : Vec A n → (A → Vec B n) → Vec B n
-  join               : Vec (Vec A n) n → Vec A n
 
   _ʳ++_              : Vec A m → Vec A n → Vec A (m + n)
 
   cast : .(eq : m ≡ n) → Vec A m → Vec A n
   ```
 
-* Added new instance in `Data.Vec.Categorical`:
+* Added new instance in `Data.Vec.Effectful`:
   ```agda
   monad : RawMonad (λ (A : Set a) → Vec A n)
   ```

src/Data/List/Effectful.agda

@@ -25,6 +25,7 @@ open P.≡-Reasoning
 private
   variable
     ℓ : Level
+    A : Set ℓ
 
 ------------------------------------------------------------------------
 -- List applicative functor
@@ -66,6 +67,9 @@ monad = record
   ; _>>=_  = flip concatMap
   }
 
+join : List (List A) → List A
+join = Join.join monad
+
 monadZero : ∀ {ℓ} → RawMonadZero {ℓ} List
 monadZero = record
   { rawMonad = monad

src/Data/Maybe/Effectful.agda

@@ -67,6 +67,9 @@ monad = record
   ; _>>=_ = _>>=_
   }
 
+join : Maybe (Maybe A) → Maybe A
+join = Join.join monad
+
 monadZero : RawMonadZero {f} Maybe
 monadZero = record
   { rawMonad = monad

src/Data/Sum/Effectful/Left.agda

@@ -62,6 +62,9 @@ monad = record
   ; _>>=_ = [ const ∘′ inj₁ , _|>′_ ]′
   }
 
+join : {B : Set (a ⊔ b)} → Sumₗ (Sumₗ B) → Sumₗ B
+join = Join.join monad
+
 ------------------------------------------------------------------------
 -- Get access to other monadic functions
 

src/Data/Sum/Effectful/Right.agda

@@ -56,6 +56,9 @@ monad = record
   ; _>>=_ = [ _|>′_ , const ∘′ inj₂ ]′
   }
 
+join : {A : Set (a ⊔ b)} → Sumᵣ (Sumᵣ A) → Sumᵣ A
+join = Join.join monad
+
 monadZero : B → RawMonadZero Sumᵣ
 monadZero b = record
   { rawMonad = monad

src/Data/Vec.agda

@@ -9,7 +9,7 @@
 
 -- See `Data.Vec.Functional` for an alternative implementation as
 -- functions from finite sets, which is more suitable for reasoning
--- about fixed sized vectors and for when ease of retrevial is
+-- about fixed sized vectors and for when ease of retrieval is
 -- important.
 
 {-# OPTIONS --cubical-compatible --safe #-}

src/Data/Vec/Base.agda

@@ -189,8 +189,6 @@ module DiagonalBind where
   _>>=_ : Vec A n → (A → Vec B n) → Vec B n
   xs >>= f = diagonal (map f xs)
 
-  join : Vec (Vec A n) n → Vec A n
-  join = _>>= id
 
 ------------------------------------------------------------------------
 -- Operations for reducing vectors
@@ -358,3 +356,4 @@ last {n = suc n} (_ ∷ xs) = last xs
 transpose : Vec (Vec A n) m → Vec (Vec A m) n
 transpose []         = replicate []
 transpose (as ∷ ass) = replicate _∷_ ⊛ as ⊛ transpose ass
+

src/Data/Vec/Effectful.agda

@@ -14,7 +14,7 @@ open import Data.Vec.Base as Vec hiding (_⊛_)
 open import Data.Vec.Properties
 open import Effect.Applicative as App using (RawApplicative)
 open import Effect.Functor as Fun using (RawFunctor)
-open import Effect.Monad using (RawMonad; RawMonadT; mkRawMonad)
+open import Effect.Monad using (RawMonad; module Join; RawMonadT; mkRawMonad)
 import Function.Identity.Effectful as Id
 open import Function.Base
 open import Level using (Level)
@@ -46,6 +46,9 @@ monad = record
   ; _>>=_ = DiagonalBind._>>=_
   }
 
+join : Vec (Vec A n) n → Vec A n
+join = Join.join monad
+
 ------------------------------------------------------------------------
 -- Get access to other monadic functions
 

src/Data/Vec/Effectful/Transformer.agda

@@ -50,7 +50,7 @@ monad {f} {g} M = record
   ; _>>=_ = λ ma k → mkVecT $ do
                       a ← runVecT ma
                       bs ← mapM {a = f} (runVecT ∘′ k) a
-                      pure (Vec.DiagonalBind.join bs)
+                      pure (Vec.diagonal bs)
   } where open RawMonad M; open Vec.TraversableM {m = f} {n = g} M
 
 monadT : RawMonadT {f} {g} (VecT n)

src/Effect/Monad.agda

@@ -16,7 +16,7 @@ open import Data.Unit.Polymorphic.Base using (⊤)
 open import Effect.Choice
 open import Effect.Empty
 open import Effect.Applicative
-open import Function.Base using (flip; _$′_; _∘′_)
+open import Function.Base using (id; flip; _$′_; _∘′_)
 open import Level using (Level; suc; _⊔_)
 
 private
@@ -58,7 +58,16 @@ record RawMonad (F : Set f → Set g) : Set (suc f ⊔ g) where
   unless : Bool → F ⊤ → F ⊤
   unless = when ∘′ not
 
+-- When level g=f, a join/μ operator is definable
+
+module Join {F : Set f → Set f} (M : RawMonad F) where
+  open RawMonad M
+
+  join : F (F A) → F A
+  join = _>>= id
+
 -- Smart constructor
+
 module _ where
 
   open RawMonad

src/Effect/Monad/Identity.agda

@@ -18,6 +18,7 @@ open import Level
 private
   variable
     a : Level
+    A : Set a
 
 record Identity (A : Set a) : Set a where
   constructor mkIdentity
@@ -47,3 +48,6 @@ comonad = record
   { extract = runIdentity
   ; extend  = λ f a → mkIdentity (f a)
   }
+
+join : Identity (Identity A) → Identity A
+join = Join.join monad

src/Effect/Monad/Partiality.agda

@@ -72,6 +72,9 @@ monad = record
   ; _>>=_  = bind
   }
 
+join : (A ⊥) ⊥ → A ⊥
+join = Join.join monad
+
 private module M {f} = RawMonad (monad {f})
 
 -- Non-termination.

src/Effect/Monad/Reader.agda

@@ -52,6 +52,9 @@ applicative = Trans.applicative Id.applicative
 monad : RawMonad (Reader R)
 monad = Trans.monad Id.monad
 
+join : Reader R (Reader R A) → Reader R A
+join = Join.join monad
+
 ------------------------------------------------------------------------
 -- Reader monad specifics
 

src/Effect/Monad/State.agda

@@ -59,6 +59,9 @@ applicative = Trans.applicative Id.monad
 monad : RawMonad (State S)
 monad = Trans.monad Id.monad
 
+join : State S (State S A) → State S A
+join = Join.join monad
+
 ------------------------------------------------------------------------
 -- State monad specifics
 

src/Effect/Monad/Writer.agda

@@ -55,6 +55,9 @@ module _ {𝕎 : RawMonoid w ℓ} where
   monad : RawMonad (Writer 𝕎)
   monad = Trans.monad Id.monad
 
+  join : Writer 𝕎 (Writer 𝕎 A) → Writer 𝕎 A
+  join = Join.join monad
+
   ----------------------------------------------------------------------
   -- Writer monad specifics