git.iko.soy/Idris-dev
on ff0fbfa help sign in
Idris-dev/lib/Control/Catchable.idr
35 lines 865 B history raw
1module Prelude.Catchable
3import Prelude.List
4import Prelude.Maybe
5import Prelude.Either
6import Control.IOExcept
8class Catchable (m : Type -> Type) t where
9 throw : t -> m a
10 catch : m a -> (t -> m a) -> m a
12instance Catchable Maybe () where
13 catch Nothing h = h ()
14 catch (Just x) h = Just x
16 throw () = Nothing
18instance Catchable (Either a) a where
19 catch (Left err) h = h err
20 catch (Right x) h = (Right x)
22 throw x = Left x
24instance Catchable (IOExcept err) err where
25 catch (ioM prog) h = ioM (do p' <- prog
26 case p' of
27 Left e => let ioM he = h e in he
28 Right val => return (Right val))
29 throw x = ioM (return (Left x))
31instance Catchable List () where
32 catch [] h = h ()
33 catch xs h = xs
35 throw () = []