git.iko.soy/Idris-dev
on 1b71663 help sign in
Idris-dev/libs/effects/Effect/Exception.idr
32 lines 796 B history raw
1module Effect.Exception
3import Effects
4import System
5import Control.IOExcept
7%access public export
9data Exception : Type -> Effect where
10 Raise : a -> sig (Exception a) b
12implementation Handler (Exception a) Maybe where
13 handle _ (Raise e) k = Nothing
15implementation Handler (Exception a) List where
16 handle _ (Raise e) k = []
18implementation Show a => Handler (Exception a) IO where
19 handle _ (Raise e) k = do printLn e
20 (exit 1)
22implementation Handler (Exception a) (IOExcept a) where
23 handle _ (Raise e) k = ioe_fail e
25implementation Handler (Exception a) (Either a) where
26 handle _ (Raise e) k = Left e
28EXCEPTION : Type -> EFFECT
29EXCEPTION t = MkEff () (Exception t)
31raise : a -> Eff b [EXCEPTION a]
32raise err = call $ Raise err