add fancy error monad
This commit is contained in:
parent
4da8aa6031
commit
83ad802f6e
1 changed files with 335 additions and 0 deletions
335
src/Quox/Error.idr
Normal file
335
src/Quox/Error.idr
Normal file
|
|
@ -0,0 +1,335 @@
|
||||||
|
module Quox.Error
|
||||||
|
|
||||||
|
import Control.Monad.Identity
|
||||||
|
import Control.Monad.Trans
|
||||||
|
import Control.Monad.Reader
|
||||||
|
import Control.Monad.Writer
|
||||||
|
import Control.Monad.State
|
||||||
|
import Control.Monad.RWS
|
||||||
|
|
||||||
|
%default total
|
||||||
|
|
||||||
|
|
||||||
|
public export
|
||||||
|
data Elem : a -> List a -> Type where
|
||||||
|
Here : x `Elem` (x :: xs)
|
||||||
|
There : x `Elem` xs -> x `Elem` (y :: xs)
|
||||||
|
%builtin Natural Elem
|
||||||
|
|
||||||
|
export
|
||||||
|
Uninhabited (x `Elem` []) where
|
||||||
|
uninhabited Here impossible
|
||||||
|
uninhabited (There _) impossible
|
||||||
|
|
||||||
|
|
||||||
|
public export
|
||||||
|
data Spine : List a -> Type where
|
||||||
|
NIL : Spine []
|
||||||
|
CONS : Spine xs -> Spine (x :: xs)
|
||||||
|
%builtin Natural Spine
|
||||||
|
|
||||||
|
|
||||||
|
public export
|
||||||
|
record OneOf types where
|
||||||
|
constructor One
|
||||||
|
elem : type `Elem` types
|
||||||
|
1 value : type
|
||||||
|
|
||||||
|
export
|
||||||
|
Uninhabited (OneOf []) where uninhabited x = uninhabited x.elem
|
||||||
|
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
inj : ty `Elem` tys => ty -> OneOf tys
|
||||||
|
inj value = One %search value
|
||||||
|
|
||||||
|
public export
|
||||||
|
All : (Type -> Type) -> List Type -> Type
|
||||||
|
All p [] = ()
|
||||||
|
All p (x::xs) = (p x, All p xs)
|
||||||
|
|
||||||
|
|
||||||
|
private
|
||||||
|
eq : All Eq types => OneOf types -> OneOf types -> Bool
|
||||||
|
eq (One Here x) (One Here y) = x == y
|
||||||
|
eq (One (There p) x) (One (There q) y) = eq (One p x) (One q y)
|
||||||
|
eq (One Here _) (One (There _) _) = False
|
||||||
|
eq (One (There z) x) (One Here y) = False
|
||||||
|
|
||||||
|
export
|
||||||
|
All Eq types => Eq (OneOf types) where (==) = eq
|
||||||
|
|
||||||
|
|
||||||
|
private
|
||||||
|
ordsToEqs : Spine types => All Ord types => All Eq types
|
||||||
|
ordsToEqs @{NIL} = ()
|
||||||
|
ordsToEqs @{CONS tl} = (%search, ordsToEqs @{tl})
|
||||||
|
|
||||||
|
private
|
||||||
|
[eqOrds] (Spine types, All Ord types) => Eq (OneOf types) where
|
||||||
|
(==) = eq @{ordsToEqs}
|
||||||
|
|
||||||
|
|
||||||
|
private
|
||||||
|
cmp : All Ord types => OneOf types -> OneOf types -> Ordering
|
||||||
|
cmp (One Here x) (One Here y) = compare x y
|
||||||
|
cmp (One Here _) (One (There _) _) = LT
|
||||||
|
cmp (One (There _) _) (One Here _) = GT
|
||||||
|
cmp (One (There p) x) (One (There q) y) = cmp (One p x) (One q y)
|
||||||
|
|
||||||
|
export
|
||||||
|
(Spine types, All Ord types) => Ord (OneOf types) using eqOrds where
|
||||||
|
compare = cmp
|
||||||
|
|
||||||
|
|
||||||
|
export
|
||||||
|
All Show types => Show (OneOf types) where
|
||||||
|
showPrec d (One Here value) = showPrec d value
|
||||||
|
showPrec d (One (There p) value) = showPrec d $ One p value
|
||||||
|
|
||||||
|
|
||||||
|
public export
|
||||||
|
record ErrorT (errs : List Type) (m : Type -> Type) (res : Type) where
|
||||||
|
constructor MkErrorT
|
||||||
|
runErrorT : m (Either (OneOf errs) res)
|
||||||
|
|
||||||
|
public export
|
||||||
|
Error : List Type -> Type -> Type
|
||||||
|
Error errs = ErrorT errs Identity
|
||||||
|
|
||||||
|
export
|
||||||
|
runError : Error errs a -> Either (OneOf errs) a
|
||||||
|
runError = runIdentity . runErrorT
|
||||||
|
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
Functor m => Functor (ErrorT errs m) where
|
||||||
|
map f (MkErrorT act) = MkErrorT $ map (map f) act
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
Applicative m => Applicative (ErrorT errs m) where
|
||||||
|
pure = MkErrorT . pure . pure
|
||||||
|
MkErrorT mf <*> MkErrorT mx = MkErrorT [|mf <*> mx|]
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
Monad m => Monad (ErrorT errs m) where
|
||||||
|
MkErrorT act >>= k = MkErrorT $ act >>= either (pure . Left) (runErrorT . k)
|
||||||
|
|
||||||
|
|
||||||
|
private
|
||||||
|
without' : (xs : List a) -> x `Elem` xs -> List a
|
||||||
|
without' (_ :: xs) Here = xs
|
||||||
|
without' (y :: xs) (There p) = y :: without' xs p
|
||||||
|
|
||||||
|
infix 9 `without`
|
||||||
|
export %inline
|
||||||
|
without : (xs : List a) -> (x : a) -> x `Elem` xs => List a
|
||||||
|
xs `without` x = without' {x} xs %search
|
||||||
|
|
||||||
|
|
||||||
|
private
|
||||||
|
get' : err `Elem` errs -> OneOf errs -> Either err (OneOf (errs `without` err))
|
||||||
|
get' Here (One Here x) = Left x
|
||||||
|
get' Here (One (There p) x) = Right (One p x)
|
||||||
|
get' (There y) (One Here x) = Right (One Here x)
|
||||||
|
get' (There y) (One (There p) x) = mapSnd {elem $= There} $ get' y (One p x)
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
get : (0 err : Type) -> err `Elem` errs =>
|
||||||
|
OneOf errs -> Either err (OneOf (errs `without` err))
|
||||||
|
get _ = get' %search
|
||||||
|
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
noErrorsT : Monad m => ErrorT [] m a -> m a
|
||||||
|
noErrorsT (MkErrorT act) = act >>= either absurd pure
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
noErrors : Error [] a -> a
|
||||||
|
noErrors = runIdentity . noErrorsT
|
||||||
|
|
||||||
|
|
||||||
|
public export
|
||||||
|
data Embed : List a -> List a -> Type where
|
||||||
|
Nil : Embed [] ys
|
||||||
|
(::) : x `Elem` ys -> Embed xs ys -> Embed (x::xs) ys
|
||||||
|
|
||||||
|
|
||||||
|
private
|
||||||
|
embedElem' : Embed xs ys -> x `Elem` xs -> x `Elem` ys
|
||||||
|
embedElem' (e :: _) Here = e
|
||||||
|
embedElem' (_ :: es) (There p) = embedElem' es p
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
embedElem : Embed xs ys => x `Elem` xs -> x `Elem` ys
|
||||||
|
embedElem = embedElem' %search
|
||||||
|
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
(<|>) : Applicative m => ErrorT errs m a -> ErrorT errs m a -> ErrorT errs m a
|
||||||
|
MkErrorT act1 <|> MkErrorT act2 = MkErrorT [|act1 `or` act2|] where
|
||||||
|
or : Either l r -> Either l r -> Either l r
|
||||||
|
one `or` two = case one of Left err => two; Right x => pure x
|
||||||
|
|
||||||
|
|
||||||
|
public export
|
||||||
|
interface Monad m => MonadThrow errs m | m where
|
||||||
|
throw : err `Elem` errs => err -> m a
|
||||||
|
|
||||||
|
public export
|
||||||
|
interface
|
||||||
|
(MonadThrow errs1 m1,
|
||||||
|
MonadThrow errs2 m2,
|
||||||
|
err `Elem` errs1) =>
|
||||||
|
MonadCatch err errs1 errs2 m1 m2
|
||||||
|
| err, m1
|
||||||
|
where
|
||||||
|
catch : (act : m1 a) -> (catch : err -> m2 a) -> m2 a
|
||||||
|
|
||||||
|
public export
|
||||||
|
interface
|
||||||
|
(MonadThrow errs1 m1,
|
||||||
|
MonadThrow errs2 m2,
|
||||||
|
Embed errs1 errs2) =>
|
||||||
|
MonadEmbed errs1 errs2 m1 m2
|
||||||
|
| m1, m2
|
||||||
|
where
|
||||||
|
embed : m1 a -> m2 a
|
||||||
|
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
implementation
|
||||||
|
Monad m =>
|
||||||
|
MonadThrow errs (ErrorT errs m)
|
||||||
|
where
|
||||||
|
throw = MkErrorT . pure . Left . inj
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
implementation
|
||||||
|
(Monad m, err `Elem` errs) =>
|
||||||
|
MonadCatch err errs (errs `without` err)
|
||||||
|
(ErrorT errs m)
|
||||||
|
(ErrorT (errs `without` err) m)
|
||||||
|
where
|
||||||
|
catch (MkErrorT act) handler = MkErrorT $
|
||||||
|
act <&> mapFst (get err) >>= \case
|
||||||
|
Left (Left this) => runErrorT $ handler this
|
||||||
|
Left (Right other) => pure $ Left other
|
||||||
|
Right ok => pure $ Right ok
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
implementation
|
||||||
|
(Monad m, Embed errs1 errs2) =>
|
||||||
|
MonadEmbed errs1 errs2 (ErrorT errs1 m) (ErrorT errs2 m)
|
||||||
|
where
|
||||||
|
embed (MkErrorT act) = MkErrorT $ mapFst {elem $= embedElem} <$> act
|
||||||
|
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
MonadTrans (ErrorT errs) where lift = MkErrorT . map Right
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
MonadReader r m => MonadReader r (ErrorT errs m) where
|
||||||
|
local f (MkErrorT act) = MkErrorT $ local f act
|
||||||
|
ask = lift ask
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
MonadWriter w m => MonadWriter w (ErrorT errs m) where
|
||||||
|
tell = MkErrorT . map Right . tell
|
||||||
|
|
||||||
|
pass (MkErrorT act) = MkErrorT $ pass $ do
|
||||||
|
Right (res, f) <- act
|
||||||
|
| Left err => pure (Left err, id)
|
||||||
|
pure (Right res, f)
|
||||||
|
|
||||||
|
listen (MkErrorT act) = MkErrorT $ do
|
||||||
|
(res, x) <- listen act
|
||||||
|
pure $ mapSnd (,x) res
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
MonadState s m => MonadState s (ErrorT errs m) where
|
||||||
|
get = lift get
|
||||||
|
put = lift . put
|
||||||
|
state = lift . state
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
MonadRWS r w s m => MonadRWS r w s (ErrorT errs m) where
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
HasIO m => HasIO (ErrorT errs m) where
|
||||||
|
liftIO = MkErrorT . map Right . liftIO
|
||||||
|
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
MonadThrow errs m => MonadThrow errs (ReaderT r m) where throw = lift . throw
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
MonadThrow errs m => MonadThrow errs (WriterT w m) where throw = lift . throw
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
MonadThrow errs m => MonadThrow errs (StateT s m) where throw = lift . throw
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
MonadThrow errs m => MonadThrow errs (RWST r w s m) where throw = lift . throw
|
||||||
|
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
implementation
|
||||||
|
MonadCatch err errs1 errs2 m1 m2 =>
|
||||||
|
MonadCatch err errs1 errs2 (ReaderT r m1) (ReaderT r m2)
|
||||||
|
where
|
||||||
|
catch (MkReaderT act) handler = MkReaderT $ \r =>
|
||||||
|
act r `catch` runReaderT r . handler
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
implementation
|
||||||
|
MonadCatch err errs1 errs2 m1 m2 =>
|
||||||
|
MonadCatch err errs1 errs2 (WriterT w m1) (WriterT w m2)
|
||||||
|
where
|
||||||
|
catch (MkWriterT act) handler = MkWriterT $ \w =>
|
||||||
|
act w `catch` \e => unWriterT (handler e) w
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
implementation
|
||||||
|
MonadCatch err errs1 errs2 m1 m2 =>
|
||||||
|
MonadCatch err errs1 errs2 (StateT s m1) (StateT s m2)
|
||||||
|
where
|
||||||
|
catch (ST act) handler = ST $ \s =>
|
||||||
|
act s `catch` \e => runStateT' (handler e) s
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
implementation
|
||||||
|
MonadCatch err errs1 errs2 m1 m2 =>
|
||||||
|
MonadCatch err errs1 errs2 (RWST r w s m1) (RWST r w s m2)
|
||||||
|
where
|
||||||
|
catch (MkRWST act) handler = MkRWST $ \r, s, w =>
|
||||||
|
act r s w `catch` \e => unRWST (handler e) r s w
|
||||||
|
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
implementation
|
||||||
|
MonadEmbed errs1 errs2 m1 m2 =>
|
||||||
|
MonadEmbed errs1 errs2 (ReaderT r m1) (ReaderT r m2)
|
||||||
|
where
|
||||||
|
embed (MkReaderT act) = MkReaderT $ embed . act
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
implementation
|
||||||
|
MonadEmbed errs1 errs2 m1 m2 =>
|
||||||
|
MonadEmbed errs1 errs2 (WriterT w m1) (WriterT w m2)
|
||||||
|
where
|
||||||
|
embed (MkWriterT act) = MkWriterT $ embed . act
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
implementation
|
||||||
|
MonadEmbed errs1 errs2 m1 m2 =>
|
||||||
|
MonadEmbed errs1 errs2 (StateT s m1) (StateT s m2)
|
||||||
|
where
|
||||||
|
embed (ST act) = ST $ embed . act
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
implementation
|
||||||
|
MonadEmbed errs1 errs2 m1 m2 =>
|
||||||
|
MonadEmbed errs1 errs2 (RWST r w s m1) (RWST r w s m2)
|
||||||
|
where
|
||||||
|
embed (MkRWST act) = MkRWST $ \r, s, w => embed $ act r s w
|
||||||
Loading…
Reference in a new issue