Theory errorLogMonad

Parents

(none)

bind : (α, ε) error # μ list -> (α -> (β, ε) error # μ list) -> (β, ε) error # μ list
choice : (α, δ) error # γ list -> (α, β) error # γ list -> (α, β) error # γ list
error : ε -> (α, ε) error # μ list
log : μ -> (unit, ε) error # μ list
return : α -> (α, ε) error # χ list
silently : α # γ -> α # β list

⊢ ∀M f.
    bind M f =
    case M of
      (emret u,ms1) => (I ## $++ ms1) (f u)
    | (error e,ms1) => (error e,ms1)

⊢ ∀M1 M2.
    choice M1 M2 =
    case M1 of
      (emret v,ms1) => (emret v,ms1)
    | (error e,ms1) => (I ## $++ ms1) M2

⊢ ∀e. error e = (error e,[])

⊢ ∀m. log m = (emret (),[m])

⊢ ∀v. return v = (emret v,[])

⊢ ∀M. silently M = (I ## K []) M

⊢ ∀M. (∃v ms. M = (emret v,ms)) ∨ ∃e ms. M = (error e,ms)

⊢ bind M f = (emret v,ms) ⇔
  ∃u ms0 ms1. M = (emret u,ms0) ∧ f u = (emret v,ms1) ∧ ms = ms0 ⧺ ms1

⊢ bind (return v) f = f v

⊢ bind M return = M

⊢ choice (return v) M = return v