on bf4e535 help sign in
Idris-dev/libs/effects/Effect/Exception.idr
30 lines 765 B history raw
1module Effect.Exception
3import Effects
4import System
5import Control.IOExcept
7data Exception : Type -> Effect where
8 Raise : a -> sig (Exception a) b
10instance Handler (Exception a) Maybe where
11 handle _ (Raise e) k = Nothing
13instance Handler (Exception a) List where
14 handle _ (Raise e) k = []
16instance Show a => Handler (Exception a) IO where
17 handle _ (Raise e) k = do print e
18 believe_me (exit 1)
20instance Handler (Exception a) (IOExcept a) where
21 handle _ (Raise e) k = ioM (return (Left e))
23instance Handler (Exception a) (Either a) where
24 handle _ (Raise e) k = Left e
26EXCEPTION : Type -> EFFECT
27EXCEPTION t = MkEff () (Exception t)
29raise : a -> Eff b [EXCEPTION a]
30raise err = call $ Raise err