module Control.Catchable

import Control.IOExcept

class Catchable (m : Type -> Type) t where
    throw : t -> m a
    catch : m a -> (t -> m a) -> m a

instance Catchable Maybe () where
    catch Nothing  h = h ()
    catch (Just x) h = Just x

    throw () = Nothing

instance Catchable (Either a) a where
    catch (Left err) h = h err
    catch (Right x)  h = (Right x)

    throw x = Left x

instance Catchable (IOExcept err) err where
    catch (ioM prog) h = ioM (do p' <- prog
                                 case p' of
                                      Left e => let ioM he = h e in he
                                      Right val => return (Right val))
    throw x = ioM (return (Left x))

instance Catchable List () where
    catch [] h = h ()
    catch xs h = xs

    throw () = []