[Defined a specialised variant of _⇨_.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101119194543
 Ignore-this: 3010746d7162d03e8b041a301746bed0
] hunk ./ReverseComposition.agda 405
+------------------------------------------------------------------------
+-- A special case
+
+-- _⇨_ where the target type is Maybe something.
+
+infixl 5 _⇨M_
+
+_⇨M_ : ∀ {ℓ} → List (Set ℓ) → Set ℓ → Set (suc ℓ)
+As ⇨M B = As ⇨ Maybe B
+
+-- Variants of the monadic combinators.
+
+returnM : ∀ {ℓ} {B : Set ℓ} → B → [] ⇨M B
+returnM = return ∘′ just
+
+_then_else_ : ∀ {ℓ As Bs} {B C : Set ℓ} →
+              As ⇨M B → (B → Bs ⇨M C) → Bs ⇨M C → As ++ Bs ⇨M C
+g then s else f = g >>= maybe s f
+
+-- Failure and left-biased choice.
+
+zeroM : ∀ {ℓ As} {B : Set ℓ} → As ⇨M B
+zeroM = return∥ nothing
+
+_⊕_ : ∀ {ℓ As} {B : Set ℓ} → As ⇨M B → As ⇨M B → As ⇨M B
+_⊕_ = zipWith∥ (RawMonadPlus._∣_ Maybe.monadPlus)
+
+-- Various laws.
+
+module MLaws {ℓ} where
+
+  open ≈-Reasoning
+
+  >>=M-cong : ∀ {As₁ Bs₁ As₂ Bs₂} {B C₁ C₂ : Set ℓ}
+                {f₁ : As₁ ⇨M B} {g₁ : Maybe B → Bs₁ ⇨M C₁}
+                {f₂ : As₂ ⇨M B} {g₂ : Maybe B → Bs₂ ⇨M C₂} →
+              f₁ ≈ f₂ →
+              (∀ x → g₁ (just x) ≈ g₂ (just x)) →
+              g₁ nothing ≈ g₂ nothing →
+              f₁ >>= g₁ ≈ f₂ >>= g₂
+  >>=M-cong {g₁ = g₁} {g₂ = g₂} f₁≈f₂ g₁j≈g₂j g₁n≈g₂n =
+    f₁≈f₂ >>=-cong′ lemma
+    where
+    open MonadLaws
+
+    lemma : ∀ x → g₁ x ≈ g₂ x
+    lemma (just x) = g₁j≈g₂j x
+    lemma nothing  = g₁n≈g₂n
+
+  left-zero : ∀ As {Bs} {B C : Set ℓ}
+              (s : B → Bs ⇨M C) (f : Bs ⇨M C) →
+              zeroM {As = As} then s else f ≈ const⋆ As f
+  left-zero As s f = MoreLaws∥.return∥->>= As nothing (maybe s f)
+
+  right-zeros : ∀ {As Bs} {B C : Set ℓ} (g : As ⇨M B) →
+                g then const zeroM else zeroM {As = Bs} {B = C} ≈
+                zeroM {As = As ++ Bs} {B = C}
+  right-zeros {B = B} g =
+    g >>= maybe (const zeroM) zeroM  ≈⟨ >>=M-cong (refl g) (λ _ → refl zeroM) (refl zeroM) ⟩
+    g >>= const zeroM                ≈⟨ MoreLaws∥.>>=-return∥ g nothing ⟩
+    zeroM                            ∎
+
+  right-identities : ∀ {As} {B : Set ℓ} (g : As ⇨M B) →
+                     g then returnM else zeroM ≈ g
+  right-identities {B = B} g =
+    g >>= maybe returnM zeroM  ≈⟨ >>=M-cong (refl g) (refl ∘ returnM) (refl zeroM) ⟩
+    g >>= return               ≈⟨ MonadLaws.right-identity g ⟩
+    g                          ∎
+
+  distrib : ∀ {As Bs Cs} {B C D : Set ℓ}
+            (g : As ⇨M B) (s : B → Bs ⇨M C) (f : Bs ⇨M C)
+            (s′ : C → Cs ⇨M D) (f′ : Cs ⇨M D) →
+            (g then s else f) then s′ else f′ ≈
+            g then (λ x → s x then s′ else f′)
+              else (f then s′ else f′)
+  distrib g s f s′ f′ =
+    (g >>= maybe s f) >>= c′                   ≈⟨ MonadLaws.assoc g (maybe s f) c′ ⟩
+    g >>= (λ x → maybe s f x >>= c′)           ≈⟨ >>=M-cong (refl g) (λ x → refl (s x >>= c′)) (refl (f >>= c′)) ⟩
+    g >>= maybe (λ x → s x >>= c′) (f >>= c′)  ∎
+    where c′ = maybe s′ f′
+
+  private
+    _∣_ : {A : Set ℓ} → Maybe A → Maybe A → Maybe A
+    _∣_ = RawMonadPlus._∣_ Maybe.monadPlus
+
+  left-identity : ∀ {As} {B : Set ℓ} (f : As ⇨M B) → zeroM ⊕ f ≈ f
+  left-identity f =
+    zeroM ⊕ f            ≈⟨ MoreLaws∥.left-identity _ _ f ⟩
+    map (_∣_ nothing) f  ≈⟨ MoreLaws∥.map-id _ ⟩
+    f                    ∎
+
+  right-identity : ∀ {As} {B : Set ℓ} (f : As ⇨M B) → f ⊕ zeroM ≈ f
+  right-identity f =
+    f ⊕ zeroM                  ≈⟨ MoreLaws∥.right-identity _ f _ ⟩
+    map (λ x → x ∣ nothing) f  ≈⟨ refl f >>=∥-cong′ lemma ⟩
+    map id                  f  ≈⟨ MoreLaws∥.map-id _ ⟩
+    f                          ∎
+    where
+    open MonadLaws∥
+
+    lemma : ∀ x → return∥ (x ∣ nothing) ≈ return∥ x
+    lemma (just x) = refl (return∥ (just x))
+    lemma nothing  = refl zeroM
+
+  assoc : ∀ {As} {B : Set ℓ} (f g h : As ⇨M B) →
+          f ⊕ (g ⊕ h) ≈ (f ⊕ g) ⊕ h
+  assoc f g h = sym $ MoreLaws∥.assoc f g h lemma
+    where
+    lemma : ∀ x y z → (x ∣ y) ∣ z ≡ x ∣ (y ∣ z)
+    lemma nothing  y z = P.refl
+    lemma (just x) y z = P.refl
+