Skip to content

Instantly share code, notes, and snippets.

@gallais
Created Feb 24, 2022
Embed
What would you like to do?
Error monad in CPS style
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment