List is a monad.

ListMonad.agda

open import Data.List 
open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Algebra
module LM {a}{A : Set a} = Monoid (monoid A)

infixr 5 _>>=_
_>>=_ : ∀ {a b}{A : Set a}{B : Set b} → List A → (A → List B) → List B
_>>=_ [] f = []
_>>=_ (x ∷ xs) f = f x ++ (xs >>= f)

return : ∀ {a}{A : Set a} → A → List A
return x = x ∷ []

left-ret : ∀ {a b}{A : Set a}{B : Set b}(f : A → List B)(x : A) → return x >>= f ≡ f x
left-ret f x = proj₂ LM.identity (f x)

right-ret : ∀ {a}{A : Set a}(xs : List A) → xs ≡ xs >>= return 
right-ret [] = refl
right-ret (x ∷ xs) = cong (_∷_ x) (right-ret xs)

>>=-rdist : 
  ∀ {a b}{A : Set a}{B : Set b}
    xs ys (f : A → List B) 
    → ((xs ++ ys) >>= f) ≡ (xs >>= f) ++ (ys >>= f)
>>=-rdist [] ys f = refl
>>=-rdist (x ∷ xs) ys f rewrite
    LM.assoc (f x) (xs >>= f) (ys >>= f)
  | >>=-rdist xs ys f 
  = refl

assoc : 
  ∀ {a b c}{A : Set a}{B : Set b}{C : Set c}
    (xs : List A)
    (f : A → List B) 
    (g : B → List C) → 
    ((xs >>= f) >>= g) ≡ (xs >>= λ x → f x >>= g)
assoc [] f g = refl
assoc (x ∷ xs) f g rewrite 
    sym $ assoc xs f g 
  | sym $ >>=-rdist (f x) (xs >>= f) g 
  = refl