The Agda Typeclassopedia: Monad

Monad.agda

{-# OPTIONS --without-K --safe #-}

module Monad where

-- [0] https://wiki.haskell.org/Typeclassopedia#Monad

open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import Function using (_∘_)

record Monad (m : Set → Set) : Set₁ where
    infixl 5 _>>=_ _>>_

    field
        return : ∀ {a : Set} → a → m a
        _>>=_  : ∀ {a b : Set} → m a → (a → m b) → m b

        left-identity : ∀ {a b : Set} (g : a → m b) (x : a)
            → return x >>= g ≡ g x
        right-identity : ∀ {a : Set} (x : m a)
            → x >>= return ≡ x
        associativity : ∀ {a b c : Set} (g : a → m b) (h : b → m c) (x : m a)
            → (x >>= g) >>= h ≡ x >>= λ { x → g x >>= h }

    -- Equivalent to `Applicative._⊛>_`.
    _>>_ : ∀ {a b : Set} → m a → m b → m b
    x >> y = x >>= λ { x → y }

    liftM : ∀ {a b : Set} → (a → b) → m a → m b
    liftM g x = x >>= (return ∘ g)

    -- Equivalent to `Applicative._⊛_`.
    ap : ∀ {a b : Set} → m (a → b) → m a → m b
    ap g x = g >>= λ { g → x >>= λ { x → return (g x) } }

module Example where
    data Maybe (a : Set) : Set where
        Just    : a → Maybe a
        Nothing : Maybe a

    _>>=_ : ∀ {a b : Set} → Maybe a → (a → Maybe b) → Maybe b
    Just x  >>= g = g x
    Nothing >>= g = Nothing

    monad : Monad Maybe
    monad = record
        { return = Just
        ; _>>=_  = _>>=_
        ; left-identity  = λ { g x → refl }
        ; right-identity = λ { (Just x) → refl ; Nothing → refl }
        ; associativity  = λ { g h (Just x) → refl ; g h Nothing → refl }
        }