git.iko.soy/Idris-dev
on 76ec3fe help sign in
Idris-dev/libs/effects/Effect/Exception.idr
41 lines 984 B history raw
1module Effect.Exception
3import Effects
4import System
5import Control.IOExcept
7data Exception : Type -> Effect where
8 Raise : a -> { () } 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 printLn 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 -> { [EXCEPTION a ] } Eff b
30raise err = call $ Raise err
37-- TODO: Catching exceptions mid program?
38-- probably need to invoke a new interpreter
40-- possibly add a 'handle' to the Eff language so that an alternative
41-- handler can be introduced mid interpretation?