open import Library.Monad

open import Level

module Library.Error where

open import Data.Sum.Base using (_⊎_; inj₁; inj₂)

module ErrorMonad {e} {E : Set e} where

  Error : ∀{a} (A : Set a)  Set (e  a)
  Error A = E  A

  pattern fail err = inj₁ err
  pattern ok   val = inj₂ val

  instance
    functorError :  {a}  Functor (Error {a})
    fmap {{functorError}} f (fail err) = fail err
    fmap {{functorError}} f (ok   a  ) = ok (f a)

    applicativeError :  {a}  Applicative (Error {a})
    pure  {{applicativeError}}              = ok
    _<*>_ {{applicativeError}} (fail err) x = fail err
    _<*>_ {{applicativeError}} (ok   f  ) x = f <$> x

    monadError :  {a}  Monad (Error {a})
    _>>=_ {{monadError}} (fail err) k = fail err
    _>>=_ {{monadError}} (ok   a  ) k = k a

  liftM2 :  {} {A B C : Set } (f : A  B  C)  Error A  Error B  Error C
  liftM2 f m n = f <$> m <*> n

  throwError : ∀{a} {A : Set a}  E  Error A
  throwError = fail

  catchError : ∀{a} {A : Set a}  Error A  (E  Error A)  Error A
  catchError (fail e) h = h e
  catchError (ok a)   h = ok a