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