State

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

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.