Skip to content

Instantly share code, notes, and snippets.

@bond15
Last active March 6, 2021 19:44
Show Gist options
  • Save bond15/9add24ac77594373c286849fa7cfe79f to your computer and use it in GitHub Desktop.
Save bond15/9add24ac77594373c286849fa7cfe79f to your computer and use it in GitHub Desktop.
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 }
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment