Exception.idr

module Effect.Exception

import Effects
import System
import Control.IOExcept

data Exception : Type -> Effect where
     Raise : a -> sig (Exception a) b

implementation Handler (Exception a) Maybe where
     handle _ (Raise e) k = Nothing

implementation Handler (Exception a) List where
     handle _ (Raise e) k = []

implementation Show a => Handler (Exception a) IO where
     handle _ (Raise e) k = do printLn e
                               believe_me (exit 1)

implementation Handler (Exception a) (IOExcept a) where
     handle _ (Raise e) k = ioe_fail e

implementation Handler (Exception a) (Either a) where
     handle _ (Raise e) k = Left e

EXCEPTION : Type -> EFFECT
EXCEPTION t = MkEff () (Exception t)

raise : a -> Eff b [EXCEPTION a]
raise err = call $ Raise err