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

module FailureAndNonDeterminism where

open import Algebra
import Algebra.FunctionProperties
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 ListMonoid {A : Set} = Monoid (List.monoid A)
open module FP {A : Set} = Algebra.FunctionProperties (_≡_ {A = A})

------------------------------------------------------------------------

infixr 5 _⊕_ _∣_

FND : Set → Set
FND = List ∘ Maybe

-- Basic functorial, applicative and monadic combinators.

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₂ _

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)  ∎
```