# State


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

```nix
let st = state.atType H.nat H.nat;
in run st.eff st.resp H.nat
     { inherit (st) handler dispatch; }
     program initialState
```

## `EffState`

_EffState : Π(S:U₀). U₀ — kernel datatype with three constructors (`get`, `put(param:S)`, `modify(fn:S→S)`). Built via `H.datatypeP`; macro-derived `.T`, `.D`, `.elim`, and per-constructor introducers._

## `EffStateTy`

_Π-type of state's op-identity family: `Π(S:U₀). U₀`._

## `Resp_State`

_Resp_State S op: response type family for state operations; get returns S, put/modify return Unit._

## `Resp_StateTy`

_Π-type of state's per-op response family: `Π(S:U₀). Π(_op:EffState S). U₀`._

## `atType`

_`atType S A` — per-`(S, A)` monomorphisation of `(EffState, Resp_State)` shipping `send`-wrapped smart constructors `get`/`put`/`modify`, the kernel-resident `handler` (= `handle_State` applied to `S` and `A`), and the Nix-side `dispatch` interpreter that reads the kernel-eval'd Sum return value into a `{ action; newState; response?; value?; }` step decision for the trampoline._

## `elimAt`

_elimAt k S — EffState.elim k with hidden state type supplied._

## `getAt`

_getAt S — EffState.get with hidden state type supplied._

## `handle_State`

_handle_State S A op s: kernel-resident state handler returning UniRet left/resume results for get, put, and modify._

## `handle_StateTy`

_Π-type of the state handler: `Π(S A:U₀). Π(op:EffState S). Π(_s:S). Sum (Σ _r:Resp_State[S,op], S) (Σ _a:A, S)`. Always returns the left (resume) summand — state effects never abort._

## `modifyAt`

_modifyAt S fn — EffState.modify with hidden state type and explicit function parameter supplied._

## `modifyPrefixAt`

_modifyPrefixAt S — EffState.modify with hidden state type supplied, leaving the explicit function parameter._

## `putAt`

_putAt S param — EffState.put with hidden state type and explicit state parameter supplied._

## `putPrefixAt`

_putPrefixAt S — EffState.put with hidden state type supplied, leaving the explicit state parameter._