exception

For failing and recovering: throw abandons the rest of the computation with a word of why (an err: a message, a diagnostic), and recover hears it. Catch holds computations, so it is made where it is, not lifted (parallel.hf says the same): both operations take the evidence exception err <: e. What happens to the world a throw abandons — kept, or rolled back — is nowhere in here: it is each handler’s to say.

ExceptionF

data ExceptionF err (m : Type -> Type) x = Throw err | Catch (m x) (err -> m x)

exception

exception : (err : Type) -> HFunctor

For failing with why, an err (a message, a diagnostic), and recovering from it.

throw

throw : {err : Type}
      -> {e : HFunctor}
      -> {a : Type}
      -> {{ev : exception err <: e}}
      -> err
      -> Co e a

Abandon the rest, with a word of why.

recover

recover : {err : Type}
        -> {e : HFunctor}
        -> {a : Type}
        -> {{ev : exception err <: e}}
        -> Co e a
        -> (err -> Co e a)
        -> Co e a

recover c h is c; if c throws, it is h of what was thrown (a do block’s try ... catch is this). (Which err that is is found from h’s type: a handler that does not look at it says it, (h : String -> Co e a), there being no search for evidence.)

DivByZero

data DivByZero = MkDivByZero

What divOrThrow and modOrThrow throw: the divisor was zero.

divOrThrow

divOrThrow : {a : Type}
           -> {e : HFunctor}
           -> {{div : Division a}}
           -> {{z : IsZero a}}
           -> {{ev : exception DivByZero <: e}}
           -> a
           -> a
           -> Co e a

x / y, but by zero a throw, not 0 (the prelude’s division is total): for a caller that would hear of it. Whether the divisor is zero is the type’s to say (IsZero).

modOrThrow

modOrThrow : {a : Type}
           -> {e : HFunctor}
           -> {{mod : Remainder a}}
           -> {{z : IsZero a}}
           -> {{ev : exception DivByZero <: e}}
           -> a
           -> a
           -> Co e a

x % y, but by zero a throw, not x.

triedFunctor

triedFunctor : (err : Type) -> (e : HFunctor) -> RawFunctor

attempted

attempted : (err : Type) -> (e : HFunctor) -> Handler (exception err <+> e)

A handler of exception err into the rest of the world, e: a throw no recover hears ends the computation, Left what was thrown. An operation of e’s is done as it is; one that holds a computation of its own, run apart (browser.dom’s on, an event’s), has none of its throws heard here — one no recover of its own hears abandons that run.

attempt

attempt : (err : Type)
        -> {e : HFunctor}
        -> {a : Type}
        -> Co (exception err <+> e) a
        -> Co e (Either err a)

c, its throws heard: Right what it comes to, or Left what was thrown and heard by no recover (remote’s calls that came to no answer, for one).