# Error


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

```nix
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)._