Monad.agda

record Monad (F : Set₀ -> Set₀) : Set₁ where
  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))



data Maybe (A : Set) : Set where
  Nothing : Maybe A
  Just : A -> Maybe A



Maybe-Monad : Monad Maybe
Maybe-Monad = record {
      return = Just
    ; _>>=_ = λ { Nothing _  -> Nothing
                ; (Just a) f -> f a }
    ; leftUnit = λ a -> λ f -> refl
    ; rightUnit = λ { Nothing  -> refl
                    ; (Just a) -> refl }
    ; associative = λ { Nothing f g  -> refl
                      ; (Just a) f g -> refl }
  }