R7: Retained behaviour: a resolved code entry is typed at its reference's typereq:R7

Open, waits on a ruling (decisions row 82: typed behaviour values): resolve_typed: a resolved code entry is typed at its reference's type, with capture layout fixed at resolution and identity by allocation or structure (decisions row 82, open)
Open, waits on a ruling (decisions row 82: typed behaviour values): code-valued services with a capture law, R5's through R7 (decisions row 82)
Open, not triaged: the reserved contract of a retained behaviour: its entry, captures, invocation context and lifetime, designed now for the planned Cache, Pool and callback modules; the value form and its evaluator wait for the first of them (decisions row 234)
Open, worded as a proposed claim: posted-body-entry-typed (proposed claim; residual-program-typing): a checked Eff body supplied at a posting site, with its resolved entry, typed lexical environment and selected service policy, stays typed under world extension (decisions rows 82, 225)

Requirement R7: Retained behaviourabout:req:R7

This page explains requirement R7 in Effect4. It covers what the requirement asks for stored code entries, why typed code resolution matters, and how the property is checked.

What the requirement asksabout:req:R7:what-it-asks

Requirement R7 demands that stored code behaviors resolve into typed entries with fixed capture layouts (docs/core/system-map.md §8, docs/core/machine-state.md §5):

Typed resolution: a resolved code entry is typed at its reference type through resolve_typed.
Fixed capture layout: captured services and environment variables fix their layout at resolution.
Stable identity: code entry identity is established by allocation or structural equality.
Owner resolution: stored behavior references resolve into the canonical Eff program owner rather than storing host closures.

Captured control state and reusable behavior content must remain distinct syntactic sorts.

Why it mattersabout:req:R7:why-it-matters

Advanced Effect modules like PubSub, Mailbox, and actor pools store and dispatch deferred execution tasks.

If stored behaviors captured arbitrary host closures, internal execution state would leak into value sorts and defeat reification.

Typed first-order resolution lets a stored routine be serialized, replayed and checked across runs.

How it is checkedabout:req:R7:how-it-is-checked

The requirement is checked by formalizing code resolution and capture typing contracts:

Code entry typing is governed by the resolve_typed specification connecting code references to target typing signatures.
Posted body entry typing asks that a queued task run under a fitting environment (decisions rows 82 and 225).
Reserved contracts for retained behavior prevent execution details from freezing into data values (decisions row 234).

The plan on this page gives each theorem's status and the goals it rests on.