ListMonad.agda

open import Function.Base using (_∘_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)

----------
-- List の定義

infixr 50 _∷_

data List (A : Set) : Set where
  [] : List A
  _∷_ : A -> List A -> List A

sing : ∀{A} -> A -> List A
sing x = x ∷ []

map : ∀{A B} -> (A -> B) -> List A -> List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

infixr 50 _++_

_++_ : {A : Set} -> List A -> List A -> List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ xs ++ ys

concat : ∀{A} -> List (List A) -> List A
concat [] = []
concat (xs ∷ xss) = xs ++ concat xss

----------
-- List の補題

++-assoc : {A : Set} -> (xs ys zs : List A) -> (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc [] ys zs = refl
++-assoc (x ∷ xs) ys zs = cong (_∷_ x) (++-assoc xs ys zs)

concat-dist : ∀{A} -> (xss yss : List (List A)) -> concat (xss ++ yss) ≡ concat xss ++ concat yss
concat-dist [] yss = refl
concat-dist (xs ∷ xss) yss
  rewrite (++-assoc xs (concat xss) (concat yss)) =
  cong (_++_ xs) (concat-dist xss yss)

----------
-- Monad の定義

record Monad (M : Set -> Set) : Set1 where

  field
    fmap : ∀{A B} -> (A -> B) -> M A -> M B
    η : ∀{A} -> A -> M A
    μ : ∀{A} -> M (M A) -> M A
    Left-Id  : ∀{A} -> (xs : M A) -> (μ ∘ η) xs ≡ xs
    Right-Id : ∀{A} -> (xs : M A) -> (μ ∘ fmap η) xs ≡ xs
    Assoc : ∀{A : Set} -> (x : M (M (M A)))  -> (μ ∘ fmap μ) x ≡ (μ ∘ μ) x

----------
-- List の Monad インスタンス (List が Monad になっていることの証明)

list-Left-Id : ∀{A} -> (xs : List A) -> (concat ∘ sing) xs ≡ xs
list-Left-Id [] = refl
list-Left-Id (x ∷ xs) = cong (_∷_ x) (list-Left-Id xs)

list-Right-Id : ∀{A} -> (x : List A) -> (concat ∘ map sing) x ≡ x
list-Right-Id [] = refl
list-Right-Id (x ∷ xs) = cong (_∷_ x) (list-Right-Id xs)

list-Assoc : ∀{A : Set} -> (xs : List (List (List A)))  -> (concat ∘ map concat) xs ≡ (concat ∘ concat) xs
list-Assoc [] = refl
list-Assoc (xss ∷ xsss)
  rewrite (concat-dist xss (concat xsss)) =
  cong (_++_ (concat xss)) (list-Assoc xsss)

listMonad : Monad List
listMonad =
  record
  { fmap = map
  ; η = sing
  ; μ = concat
  ; Left-Id = list-Left-Id
  ; Right-Id = list-Right-Id
  ; Assoc = list-Assoc
  }

StateMonad.agda

open import Axiom.Extensionality.Propositional using (Extensionality)
open import Function.Base using (_∘_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)

data _×_ A B : Set where
  _,_ : A -> B -> A × B

State : Set -> Set -> Set
State S A = S -> S × A

state-fmap : ∀{S A B} -> (A -> B) -> State S A -> State S B
state-fmap f sa s with sa s
...                 | s1 , x = (s1 , f x)

state-η : ∀{S A} -> A -> State S A
state-η x s = (s , x)

state-μ : ∀{S A} -> State S (State S A) -> State S A
state-μ ssa s with ssa s
...               | s1 , sa = sa s1

postulate
  functional-EX : ∀{a b} -> Extensionality a b

state-Left-Id : ∀{S A} -> (sa : State S A) -> (state-μ ∘ state-η) sa ≡ sa
state-Left-Id sa = refl

state-Right-Id : ∀{S A} -> (sa : State S A) -> (state-μ ∘ state-fmap state-η) sa ≡ sa
state-Right-Id {S} sa = functional-EX right-id
  where
    right-id : (s : S) -> (state-μ ∘ state-fmap state-η) sa s ≡ sa s
    right-id s with sa s
    ...      | (s1 , x) = refl

state-Assoc : ∀{S A} -> (ssa : State S (State S (State S A))) -> (state-μ ∘ state-fmap state-μ) ssa ≡ (state-μ ∘ state-μ) ssa
state-Assoc {S} ssa = functional-EX assoc
  where
    assoc : (s : S) -> (state-μ ∘ state-fmap state-μ) ssa s ≡ (state-μ ∘ state-μ) ssa s
    assoc s with ssa s
    ...        | (s1 , sa) with sa s1
    ...                       | (s2 , x) = refl

----------
-- Monad の定義

record Monad (M : Set -> Set) : Set1 where

  field
    fmap : ∀{A B} -> (A -> B) -> M A -> M B
    η : ∀{A} -> A -> M A
    μ : ∀{A} -> M (M A) -> M A
    Left-Id  : ∀{A} -> (x : M A) -> (μ ∘ η) x ≡ x
    Right-Id : ∀{A} -> (x : M A) -> (μ ∘ fmap η) x ≡ x
    Assoc : ∀{A : Set} -> (x : M (M (M A)))  -> (μ ∘ fmap μ) x ≡ (μ ∘ μ) x

----------
-- State S の Monad インスタンス (State S が Monad になっていることの証明)

stateMonad : ∀{S} -> Monad (State S)
stateMonad =
  record
  { fmap = state-fmap
  ; η = state-η
  ; μ = state-μ
  ; Left-Id = state-Left-Id
  ; Right-Id = state-Right-Id
  ; Assoc = state-Assoc
  }