Option Monad Agda

Mon.agda

{-# OPTIONS --type-in-type #-}
-- ^^ ignoring sizing
module Mon where
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

REL : Set -> Set  -> Set 
REL A B = A -> B -> Set 

Rel :  Set -> Set 
Rel A  = REL A A 

-- Axiom
postulate
  extensionality : ∀ {A B : Set }{f g : A -> B}
    -> (∀ (x : A) -> f x ≡ g x)
    ---------------------------
    -> f ≡ g

data Option (A : Set) : Set where
    Some : A -> Option A
    None : Option A

fmap : { A B : Set} -> (A -> B) -> Option A -> Option B
fmap f None = None
fmap f (Some a) = Some (f a)


-- technically a PreCategory
-- https://ncatlab.org/homotopytypetheory/show/precategory
record Category : Set where
  field
    Ob : Set 
    _⇒_ : Rel Ob 
    _∘_  : ∀ {x y z : Ob} -> y ⇒ z -> x ⇒ y -> x ⇒ z
    id : ∀ {o : Ob} -> o ⇒ o
    idˡ : ∀ {x y : Ob} (f : x ⇒ y) -> f ∘ (id {x}) ≡ f
    idʳ : ∀ {x y : Ob} (f : x ⇒ y) -> (id {y}) ∘ f ≡ f
    ∘-assoc : ∀ {x y z w : Ob} (f : x ⇒ y) (g : y ⇒ z) (h : z ⇒ w) -> h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f


Agda : Category
Agda = record
    { Ob = Set
    ; _⇒_ = λ (A B : Set) -> (A -> B)
    ; _∘_ = λ f g x -> f(g x)
    ; id = λ x -> x
    ; idˡ = λ f -> refl
    ; idʳ = λ f -> refl
    ; ∘-assoc = λ f g h → refl
    }

record Functor (C : Category) (D : Category ) : Set where
  open module C = Category C renaming (_⇒_ to _⇒C_; _∘_ to _∘C_)
  open module D = Category D renaming (_⇒_ to _⇒D_; _∘_ to _∘D_)
  field
    F₀ : C.Ob -> D.Ob
    F₁ : ∀ {A B : C.Ob} (f : A ⇒C B ) -> (F₀ A) ⇒D (F₀ B)

    identity : ∀ {A} -> (F₁ (C.id {A})) ≡ D.id {(F₀ A)}
    homomorphism : ∀ {A B C} -> (f : A ⇒C B) -> (g : B ⇒C C) ->
      F₁ (g ∘C f) ≡ (F₁ g) ∘D (F₁ f)

Endofunctor : Set
Endofunctor = Functor Agda Agda

Option-Endofunctor : Endofunctor
Option-Endofunctor = record 
                        { F₀ = Option ; 
                          F₁ = fmap ;
                          identity = extensionality λ{ None -> refl 
                                                    ; (Some a) -> refl};
                          homomorphism = λ f g -> extensionality λ{ None -> refl 
                                                                ; (Some a) -> refl } 
                        }

record Monad (F : Endofunctor) : Set where
  open module F = Functor F using(F₀)
  field
    return : ∀ {A : Set} -> A -> F₀ A
    _>>=_  : ∀ {A B : Set} -> F₀ A -> (A -> F₀ B) -> F₀ B
    -- laws
    leftUnit : ∀ {A B : Set}
                 (a : A)
                 (f : A -> F₀ B)
                    -> (return a) >>= f ≡ f a
    rightUnit : ∀ {A : Set}
                  (m : F₀ A)
                    ->  m >>= return ≡ m
    associative : ∀ {A B C : Set}
                    (m : F₀ A)
                    (f : A -> F₀ B)
                    (g : B -> F₀ C)
                      -> (m >>= f) >>= g ≡ m >>= (λ x -> (f x >>= g))


bind : {A B : Set} -> Option A -> (A -> Option B) -> Option B
bind None f = None
bind (Some a) f = f a

Option-Monad : Monad Option-Endofunctor
Option-Monad = record {
      return = Some
    ; _>>=_ = bind
    ; leftUnit = λ a -> λ f -> refl
    ; rightUnit = λ { None  -> refl
                    ; (Some a) -> refl }
    ; associative = λ { None f g  -> refl
                      ; (Some a) f g -> refl }
  }