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})
infixr 5 _⊕_ _∣_
FND : Set → Set
FND = List ∘ Maybe
open RawMonad (Maybe.monadT (List.monad {ℓ = Level.zero})) public
using (return; _>>=_; _<$>_; _⊛_)
↯ : ∀ {A} → FND A
↯ = [ nothing ]
∅ : ∀ {A} → FND A
∅ = []
_⊕_ : ∀ {A} → FND A → FND A → FND A
x ⊕ y = LM._>>=_ x (maybe return y)
_∣_ : ∀ {A} → FND A → FND A → FND A
_∣_ = _++_
∅-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
∅-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)) ∎
↯-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₂ _
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) ∎