Error monad in CPS style

Error.idr

module Error

export
data Error : (err, a : Type) -> Type where
  MkError : (forall r. (err -> r) -> (a -> r) -> r) -> Error err a

export %inline
runError : Error err a -> (err -> r) -> (a -> r) -> r
runError (MkError hdl) kE kV = hdl kE kV

export %inline
handle : Error err a -> (err -> a) -> a
handle ma kE = runError ma kE id

export
Functor (Error err) where
  map f (MkError hdl) = MkError (\ kE, kV => hdl kE (kV . f))

bind : Error err a -> (a -> Error err b) -> Error err b
bind (MkError hdl) f = MkError (\ kE, kV => hdl kE (\ a => runError (f a) kE kV))

export
raise : err -> Error err a
raise err = MkError $ \ kE, kV => kE err

export
Applicative (Error err) where
  pure v = MkError $ \ kE, kV => kV v
  mf <*> mx = bind mf $ \ f => map f mx

export
Monad (Error err) where
  (>>=) = bind

export
catch : Error err a -> (err -> Error err2 a) -> Error err2 a
catch ma kE = runError ma kE pure