Error

Pair with experimental.desc-interp.trampoline.run:

let er = error.atType_strict H.string H.nat;
in run er.eff er.resp H.nat returnTy
     { handler = er.handler; dispatch = er.dispatch; }
     program initialState

Strategies differ in handler return shape and dispatch action:

strict : Σ State E → action="throw" collecting : Σ (List E) Unit → action="resume", response=tt result : Σ State (Sum E A_inner)→ action="abort"

EffError

EffError : Π(E:U₀). U₀ — kernel datatype with one constructor error(payload:E). Built via H.datatypeP; macro-derived .T, .D, .elim, and the error introducer.

EffErrorTy

Π-type of error's op-identity family: Π(E:U₀). U₀.

Resp_collecting

Collecting error response family; errors resume with Unit while accumulating payloads in state.

Resp_collectingTy

Π-type of collecting-error's response family: Π(E:U₀). Π(_op:EffError E). U₀. Body returns Unit — collecting always resumes with tt.

Resp_result

Result-channel error response family; errors abort into Sum E A_inner.

Resp_resultTy

Π-type of result-error's response family: Π(E:U₀). Π(_op:EffError E). U₀. Body returns Void — result never resumes (abort lives in the program's typed result channel).

Resp_strict

Strict error response family; every error op has Void response because strict errors never resume.

Resp_strictTy

Π-type of strict-error's response family: Π(E:U₀). Π(_op:EffError E). U₀. Body returns Void at every op — strict never resumes.

atType_collecting

atType_collecting E — per-E monomorphisation of handle_collecting (State specialised to List E). Exposes the State field as a convenience for callers needing H.nil E initial values.

atType_result

atType_result E State A_inner — per-(E, State, A_inner) monomorphisation of handle_result with the Sum E A_inner result channel pre-built.

atType_strict

atType_strict E State — per-(E, State) monomorphisation of handle_strict with a raise smart constructor and dispatch interpreter pre-built. Pass { handler; dispatch; } to the trampoline.

handle_collecting

Kernel collecting error handler; conses payloads into List E state and resumes with Unit.

handle_collectingTy

Π-type of the collecting error handler: Π(E:U₀). Π(op:EffError E). Π(_s:List E). Σ (List E) Unit. Always resumes — handler accumulates errors into List E state, signals resume via tt. Dispatch action = "resume".

handle_result

Kernel result error handler; aborts with Sum E A_inner while preserving state.

handle_resultTy

Π-type of the result error handler: Π(E State A_inner:U₀). Π(op:EffError E). Π(_s:State). Σ State (Sum E A_inner). Always aborts — handler returns inl payload in the Sum-typed result channel. Dispatch action = "abort".

handle_strict

Kernel strict error handler; maps raise to throw-shaped Σ State E.

handle_strictTy

Π-type of the strict error handler: Π(E State:U₀). Π(op:EffError E). Π(_s:State). Σ State E. Non-resumable — handler surrenders the error payload with the final state. Dispatch action = "throw".

uniformOf_collecting

uniformOf_collecting E A: UniRet-shaped adapter for handle_collecting. Dispatches via EffError.elim so the resume payload tt : Unit ≡ Resp_collecting E (error E payload) types in each branch.

uniformOf_collectingTy

Π-type of uniformOf_collecting: UniRet at S := List E, with A as a phantom parameter (collecting never aborts).

uniformOf_result

uniformOf_result E State A_inner: UniRet-shaped adapter for handle_result. Projects Σ State (Sum E A_inner) into mkAbort … sumPayload state.

uniformOf_resultTy

Π-type of uniformOf_result: UniRet at A := Sum E A_inner (handle_result's typed result channel becomes the abort value).

uniformOf_strict

uniformOf_strict E State: UniRet-shaped adapter for handle_strict. Projects Σ State E into mkAbort … e s; always inhabits the right summand.

uniformOf_strictTy

Π-type of uniformOf_strict: UniRet at A := E (the surrender value rides the abort channel).