Theory "readerMonad"

Parents     indexedLists   patternMatches

Signature

Constant Type
BIND :(σ -> α) -> (α -> σ -> β) -> σ -> β
FMAP :(α -> β) -> (σ -> α) -> σ -> β
JOIN :(σ -> σ -> α) -> σ -> α
MCOMPOSE :(α -> σ -> β) -> (β -> σ -> γ) -> α -> σ -> γ
UNIT :α -> β -> α

Definitions

UNIT_def 
⊢ ∀x s. UNIT x s = x
MCOMPOSE_def 
⊢ ∀f1 f2 a. MCOMPOSE f1 f2 a = BIND (f1 a) f2
JOIN_def 
⊢ ∀MM s. JOIN MM s = MM s s
FMAP_def 
⊢ ∀f M1. FMAP f M1 = f ∘ M1
BIND_def 
⊢ ∀M f s. BIND M f s = f (M s) s

Theorems

MCOMPOSE_RIGHT_ID 
⊢ MCOMPOSE f UNIT = f
MCOMPOSE_LEFT_ID 
⊢ MCOMPOSE UNIT g = g
MCOMPOSE_ASSOC 
⊢ MCOMPOSE f (MCOMPOSE g h) = MCOMPOSE (MCOMPOSE f g) h
JOIN_BIND 
⊢ JOIN M = BIND M I
FMAP_o 
⊢ FMAP (f ∘ g) = FMAP f ∘ FMAP g
FMAP_ID 
⊢ (FMAP (λx. x) M = M) ∧ (FMAP I M = M)
FMAP_BIND 
⊢ FMAP f M = BIND M (UNIT ∘ f)
BIND_UNITR 
⊢ BIND m UNIT = m
BIND_UNITL 
⊢ BIND (UNIT x) f = f x
BIND_JOIN 
⊢ BIND M f = JOIN (FMAP f M)