------------------------------------------------------------------------
-- A monad with non-determinism and failure
------------------------------------------------------------------------

module FailureAndNonDeterminism where

open import Algebra
import Algebra.FunctionProperties
open import Category.Monad
open import Data.List as List
import Data.List.Properties as ListProp
open import Data.Maybe as Maybe
open import Data.Product
open import Function
import Level
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open P.≡-Reasoning
private
  module LM = RawMonadPlus (List.monadPlus { = Level.zero})
  module ListMonoid {A : Set} = Monoid (List.monoid A)
  open module FP {A : Set} = Algebra.FunctionProperties (_≡_ {A = A})

------------------------------------------------------------------------
-- The monad

infixr 5 _⊕_ _∣_

-- The monad.

FND : Set  Set
FND = List  Maybe

-- Basic functorial, applicative and monadic combinators.

open RawMonad (Maybe.monadT (List.monad { = Level.zero})) public
  using (return; _>>=_; _<$>_; _⊛_)

-- Failure.

 :  {A}  FND A
 = [ nothing ]

-- No result.

 :  {A}  FND A
 = []

-- Catch.

_⊕_ :  {A}  FND A  FND A  FND A
x  y = LM._>>=_ x (maybe return y)

-- Non-determinism.

_∣_ :  {A}  FND A  FND A  FND A
_∣_ = _++_

----------------------------------------------------------------------
-- Laws

-- ∅ and _∣_ form a monoid.

∅-left-identity-∣ :  {A} (m : FND A)    m  m
∅-left-identity-∣ = proj₁ ListMonoid.identity

∅-right-identity-∣ :  {A} (m : FND A)  m    m
∅-right-identity-∣ = proj₂ ListMonoid.identity

∣-assoc :  {A}  Associative (_∣_ {A = A})
∣-assoc = ListMonoid.assoc

-- ↯ and _⊕_ form a monoid, with ∅ as a left zero, and _⊕_
-- distributing from the right over _∣_.

∅-left-zero-⊕ :  {A} (m : FND A)    m  
∅-left-zero-⊕ m = P.refl

∣-⊕-distrib :  {A} (m₁ m₂ m₃ : FND A) 
              (m₁  m₂)  m₃  (m₁  m₃)  (m₂  m₃)
∣-⊕-distrib m₁ m₂ m₃ = ListProp.Monad.right-distributive m₁ m₂ _

↯-left-identity-⊕ :  {A} (m : FND A)    m  m
↯-left-identity-⊕ m = proj₂ ListMonoid.identity m

↯-right-identity-⊕ :  {A} (m : FND A)  m    m
↯-right-identity-⊕ []            = P.refl
↯-right-identity-⊕ (just x   m) = P.cong (_∷_ (just x)) $ ↯-right-identity-⊕ m
↯-right-identity-⊕ (nothing  m) = P.cong (_∷_ nothing) $ ↯-right-identity-⊕ m

⊕-assoc :  {A}  Associative (_⊕_ {A = A})
⊕-assoc []            y z = P.refl
⊕-assoc (just u   x) y z = P.cong (_∷_ (just u)) $ ⊕-assoc x y z
⊕-assoc (nothing  x) y z = begin
  (y  (x  y))  z        ≡⟨ ∣-⊕-distrib y _ _ 
  (y  z)  ((x  y)  z)  ≡⟨ P.cong (_∣_ (y  z)) $ ⊕-assoc x y z 
  (y  z)  (x  (y  z))  

-- ↯ and ∅ are both left zeros of _>>=_, and _>>=_ distributes from
-- the right over _∣_.

↯-left-zero->>= :  {A B} (f : A  FND B)  ( >>= f)  
↯-left-zero->>= f = P.refl

∅-left-zero->>= :  {A B} (f : A  FND B)  ( >>= f)  
∅-left-zero->>= f = P.refl

∣->>=-distrib :  {A B} (m₁ m₂ : FND A) (f : A  FND B) 
                ((m₁  m₂) >>= f)  (m₁ >>= f)  (m₂ >>= f)
∣->>=-distrib m₁ m₂ f = ListProp.Monad.right-distributive m₁ m₂ _

-- Monad laws.

left-identity :  {A B} x (f : A  FND B)  (return x >>= f)  f x
left-identity x f = proj₂ ListMonoid.identity (f x)

right-identity :  {A} (m : FND A)  (m >>= return)  m
right-identity []            = P.refl
right-identity (just x   m) = P.cong (_∷_ (just x)) $ right-identity m
right-identity (nothing  m) = P.cong (_∷_ nothing)  $ right-identity m

>>=-assoc :  {A B C} (m : FND A) (f : A  FND B) (g : B  FND C) 
            (m >>= f >>= g)  (m >>= λ x  f x >>= g)
>>=-assoc []            f g = P.refl
>>=-assoc (nothing  m) f g = P.cong (_∷_ nothing) $ >>=-assoc m f g
>>=-assoc (just x   m) f g = begin
  ((f x  (m >>= f)) >>= g)              ≡⟨ ∣->>=-distrib (f x) _ _ 
  (f x >>= g)  (m >>= f >>= g)          ≡⟨ P.cong (_∣_ (f x >>= g)) $ >>=-assoc m f g 
  (f x >>= g)  (m >>= λ x  f x >>= g)