On the Expressive Power of Hook-Indexed State: Comprehending State in the React UI Library (Extended Version)

1 Introduction

• React components use useState to retain internal state across rerenders, with the runtime supplying the latest value and rerendering affected components after updates.React is described as the most popular front-end web development library.Source: §1 · p. 1
• A type system with lightweight effect typing and pseudo-linearity of pointers captures state-related Rules of React that otherwise remain statically unenforceable.The motivating pitfalls include crashes from conditional hook calls and possible infinite rerendering after state updates during rendering.Source: §1 · pp. 1–2
• useState uses its argument to initialize state on the first render, then retrieves state from the heap on later renders.The paper models this context-dependent behavior in its hook calculus.Source: §1 · p. 2
• The paper proposes stateless, hook-state, and reference-state calculi, each with a sound type system and small-step operational semantics.The hook calculus includes a lightweight effect system and pseudo-linear pointer context.Source: §1 · p. 2
• A translation preserves typability and closely corresponds operationally, expressing hook-indexed state with ML-style references but duplicating code and breaking abstraction.The translation is local and compositional.Source: §1 · p. 2
• The paper sketches reconciliation, useEffect, and custom hooks as extensions to the hook calculus.These extensions are presented as evidence that the calculus offers a scalable foundation.Source: §1 · p. 2

2.1 Programming with React

• Local mutable variables reset on rerender, while a global counter shares state across instances; useState instead preserves separate state for each component instance.The setter triggers a rerender, and each useState call returns the most recent value for that instance.Source: §2.1 · p. 3

2.2 Local State, by Hook or by Crook

• Hook calls whose evaluation order changes can retrieve the wrong state, while an unconditional setter during rendering triggers endless rerenders.React identifies state by each hook’s evaluation order within a component instance; its top-level setter behavior retries rendering immediately.Source: §2.2 · pp. 3–4

2.3 A Core Calculus of Hook-Indexed State

• The core calculus models each component instance with a memory pointer and an Init or Succ phase, and its body syntax enforces top-level hook calls.Hooks are labeled in evaluation order: Init saves the initial value and setter, while Succ retrieves the latest value from the instance’s memory.Source: §2.3 · pp. 4–5

2.4 The Typing Rules of React

• The sound type system tracks state labels across bodies and instance memories, enforcing safe successor reads, one-time initialization, and setter-free component bodies.Initialization preserves the combined body-and-memory type as state cells are added; successor evaluation requires body labels to exist in memory, and phase contexts prevent reinitializing an instance.Source: §2.4 · pp. 5–6

2.5 Putting useState in Other Terms

• Translating useState is difficult because components interleave initialization with computation and have partially initialized state that is awkward to represent as one type-safe value.These features obstruct straightforward decomposition into state and pure update/render functions.Source: §2.5 · pp. 6–7
• The calculus translates hook-indexed state into first-class references while preserving types and operational semantics through a local translation that admits a compositional definition.The translation duplicates component bodies across initialization and successor phases; setters update references and flip a rerender flag, so the target code is cumbersome and exposes that flag.Source: §2.5 · p. 7

3.1 Syntax

• The calculus uses a fine-grain call-by-value syntax that separates values from computations and requires intermediate computations to be let-bound.The authors say this restriction simplifies the metatheory and that nested computations can be elaborated by inserting lets.Source: §3.1 · pp. 7–8
• The pure calculus defines standard value and computation forms plus element and runtime-instance types, including runtime constructs for initialization, clicks, and updates.Elements specify trees that the runtime realizes as distinguishable instances; the runtime constructs can be expressed using datatype folds and destructors.Source: §3.1 · p. 8

3.2 Type System

• The pure calculus uses mutually inductive typing judgments for values and computations, requires programs to have type Element, and assigns event handlers type 1 → 1.The initial configuration realizes a program into an ElemInst.Source: §3.2 · p. 9

3.3 Operational Semantics

• The pure operational semantics realizes text and tags as runtime instances, assigns fresh identifiers to tags, and searches matching nodes to invoke click handlers.The top-level event step chooses a node identifier and performs the click handling and node updates.Source: §3.3 · p. 10

3.4 Metatheory

• The pure calculus satisfies preservation and progress for ordinary steps, while top-level configurations preserve ElemInst typing and can always take an event step.The top-level semantics never terminates because an event can always be received.Source: §3.4 · pp. 10–11

4.1 Syntax

• Hook state is identified by component-instance pointer and label: useState binds the current value and setter, while setters mutate a particular state cell.A component instance wraps its body and child element; runtime-generated pointers distinguish instances of the same component.Source: §4.1 · p. 11

4.2 Type System

• The hook type system tracks Pure versus Mut effects and component phases to restrict state mutation and distinguish one-time initialization from reruns.Phase contexts treat Init pointers linearly and allow Succ pointers to be reused; body-embedded computations must be Pure, preventing setters from being invoked there.Source: §4.1 · p. 12, §4.2 · pp. 12, 14

4.3 Operational Semantics

• During update, an instance whose rerender flag is true reevaluates its body; otherwise, it propagates the update trigger to its child.Applying a setter updates the heap, and component initialization allocates a fresh pointer and begins body evaluation.Source: §4.3 · p. 14
• In Init, useState stores the initial value; in Succ, it retrieves the stored value, and both phases bind a setter for the same hook location.Hook-body evaluation is parameterized by phase and component-instance pointer; evaluation of bodies and component instances is covered by separate rules.Source: §4.3 · p. 14

4.4 Metatheory

• The hook calculus has syntactic type soundness: well-typed configurations can take a top-level step, and preservation maintains typing as phase and heap contexts evolve.Progress during Succ-phase body evaluation requires all body labels to be in the instance memory, ensuring accessed heap values were initialized.Source: §4.4 · pp. 15–16

4.4.1 Consistency.

• Effect typing prevents setters from being called at component-body top level, while consistency ensures a well-typed component that evaluates to a value leaves the heap unchanged.This rules out the described infinite rerender cycle and ensures rendered state is not stale, so React’s retry behavior need not be modeled.Source: §4.4.1 · p. 16

5.1 Syntax and Typing Rules

• In the reference calculus, a component function returns a rendering function, a rerender flag, and an initial element; standard reference operations create, read, and update locations.Component instances carry the corresponding rendering function, flag, and realized element.Source: §5.1 · pp. 17–18

5.2 Operational Semantics

• Reference-calculus component updates rerender when the flag is true, otherwise propagate updates to the current element; clicks propagate through an instance to its child.Initialization evaluates the component function, instantiates its returned element, and creates a component instance.Source: §5.2 · p. 18

5.3 Metatheory

• The reference calculus has type soundness for its top-level judgment, with preservation maintaining typing and store typing and progress guaranteeing a next step.The store-typing judgment requires the store and its typing context to have matching locations, with each stored value matching its assigned type.Source: §5.3 · p. 18

6.2.1 Runtime Environment.

• The runtime environment relates dynamically generated identifiers, rerender flags, and state cells across the two languages.The translation is parameterized by this relation so fresh source and target constructs can be related.Source: §6.2.1 · p. 19

6.2.2 Location Variable Environment.

• The variable environment records previously bound location variables, allowing translation to handle intermediate evaluation stages as well as static bodies.When a label has no corresponding variable, the translation uses the runtime environment’s location instead.Source: §6.2.2 · pp. 19–20

6.3 Translation

• Initial- and successor-phase translations use references for state cells and setters that update state and mark the component for rerendering.Component bodies are translated in both phases, which accounts for the duplication discussed later.Source: §6.3 · pp. 20–21

6.4 Correctness

• Type preservation and tight operational correspondence establish that the translation preserves typing and tracks source-language execution without administrative-redex complications.Target-language determinism also gives backward simulation, so translated terms do not go astray.Source: §6.4 · pp. 21–22, §6.4.2 · p. 23

6.5 Discussion

• The translation is feature-local but not macro-local: it leaves unrelated constructs unaffected while threading information between component phases.Its compositional definition has an exception: component translation passes the body twice, with the second copy translated in the successor phase.Source: §6.5 · p. 23
• Translating a component body for both phases duplicates code that programmers must repeat when reproducing source behavior in the target language.The authors note that phase-parameterized target components could remove duplication, but would make the translation more complex.Source: §6.5 · p. 23
• Direct access to the rerender flag in the reference language can let a handler suppress rerendering after state changes, unlike the hook language’s encapsulation.This difference means the translation does not preserve full abstraction: target contexts can distinguish translated terms.Source: §6.5 · p. 24

7.1 Reconciliation

• Without reconciliation, updating an outer component resets its nested counter; reconciliation preserves the inner counter’s state.The extension compares old and new rendered values, then either initializes new instances or preserves tag and component identity while recursing to children.Source: §7.1 · p. 24
• Reconciliation requires carrying prior element contents through rerendering so the semantics can decide whether to reinitialize or preserve instances.The target treats reconcile as a primitive that can be encoded using recursion and suitable destructors.Source: §7.1 · p. 24

7.2 The useEffect Hook

• Setters inside Effects must be permitted, but an unconditional setter can trigger an infinite rerender–Effect loop.The extension queues Effects and adds commit and check computations that flush queues and repeatedly rerender while flags are set.Source: §7.2 · p. 25
• Effects translate as thunks, while bodies pass a list of effects as state; useEffect enqueues an Effect for later execution.The final queue is saved in an extended component-instance constructor, and commit/check behave analogously in the target.Source: §7.2 · p. 25

7.3 Custom Hooks

• Custom hooks may call primitive or custom hooks in sequence, subject to the top-level restriction in their definitions.The extension replaces static state labels with a type-level list ordered by state initialization and dynamically allocated labels, so separate hook calls do not share state.Source: §7.3 · p. 25
• Custom hooks use Hook types graded by state-initialization order, and bind composes those grades across sequential hook calls.A hook returns its successor-phase interpretation alongside its value; nested custom hooks’ successor interpretations must be invoked in the enclosing hook’s successor phase.Source: §7.3 · p. 26

Earlier reactive systems

• Madsen et al. model class-based React lifecycles and reconciliation with SetState, while Flapjax uses signals and event streams in a more imperative style.Flapjax predates reconciliation-based approaches.Source: §8 · p. 26

React-tRace

• React-tRace aims to model React faithfully, whereas this work distills a well-behaved language for hook-indexed state and studies its expressiveness via translation.The type-and-effect system rules out programs React-tRace models, permitting substitution-based small-step semantics and omission of React’s retry behavior; reconciliation and useEffect receive less emphasis.Source: §8 · p. 26

Reactive views

• Chlipala and Fowler et al. model views of mutable data sources with monadic composition and dataflow updates, but provide no formal semantics.Their model differs from hook-indexed state.Source: §8 · p. 26

Model-View-Update

• Elm’s Model-View-Update architecture uses an event loop; it is simpler than React generally but can produce larger, more monolithic data models.Fowler formalizes MVU in λMVU and extends it with linear resources.Source: §8 · pp. 26–27

Document languages

• Crichton and Krishnamurthi formalize structured reactive documents, but their model updates state from a predefined event list rather than state hooks.Their article calculus represents hierarchically structured documents, including HTML.Source: §8 · p. 27

Translation methodology

• The paper gives its source and target languages separate semantics before proving the translation preserves types and behavior, following Pottier ’s methodology.O’Hearn and Reynolds instead give fragments semantics through translation.Source: §8 · p. 27

Conclusion

• The soundly typed core calculus offers a blueprint for incorporating React-style hook-indexed state into languages.Its local translation to ML-style first-class references shows that hook-indexed state is expressible with references, but duplicates code and lowers abstraction.Source: §9 · p. 27
• Designers of languages with state scoped to re-instantiable blocks and observable changes have a principled basis for choosing among useState, ML-style references, and alternatives.The translation is local and compositional, but duplicates code and lowers abstraction.Source: §9 · p. 27

Disclosure of Use of AI in Research

• AI helped brainstorm names and tighten a couple of conclusion sentences, but was not used in the research itself.Source: Disclosure of Use of AI in Research · p. 27

• The work has no associated artifacts.Source: Data Availability Statement · p. 27

• Deductions used in a top-down derivation can be labeled separately from their use.Source: some judgment · p. 31
• Subconclusions can be labeled on the left to split up large derivations.Source: some judgment · p. 31
• A derived judgment can be used as a premise in a larger derivation.Source: some judgment · p. 31
• A subconclusion may use an unspecified or partially specified context that is specified when the subconclusion is invoked.Source: some judgment · p. 31

A.1 Derived Rules

• Derived rules cover list initialization, updating, iteration, click-search, mapping, and running clicks.The rules for initialization and updating use TC-Map; the map and click operations draw on fold or iter.Source: §A.1 · pp. 31–33
• Map is defined with fold to build a list by applying its function to each element.The accumulator starts as the empty list, and the derived rule is obtained using TC-Iter.Source: §A.1 · p. 31
• List initialization is defined as mapping init over a list, while list updating maps update over its elements.Source: §A.1 · p. 32
• Iteration is defined with fold, and its Mut-effect derivation can be obtained by invoking TC-Sub throughout.Source: §A.1 · p. 33
• List click-search is defined by iterating click over the list’s elements.Source: §A.1 · p. 33
• List click-run is defined by iterating runClick over the list, with its derived rule obtained using TC-Iter.Source: §A.1 · p. 33

A.2 Weakening

• Weakening Π arbitrarily is unsound because extending Π[p] can violate TC-EvalI’s requirement that Π[p] ∩ L = ∅.The permitted weakening is limited to initial-phase pointers unrelated to the term, as determined by Φ.Source: §A.2 · p. 34
• Weakening preserves value typing when Π is extended compatibly and Φ is sufficiently disjoint from the added context.Source: §A.2 · p. 34
• Values, declarations, and pure computations require Succ(Φ), a property established by the appendix’s lemmas.A Pure effect excludes TC-EvalI because that rule introduces an Init-phase pointer and a Mut effect.Source: §A.2 · p. 39
• With Succ(Φ′) and a defined phase combination, weakening can combine Φ with Φ′ while preserving value, computation, and declaration judgments.Source: §A.2 · pp. 39–40
• Related weakening results preserve computation and declaration typing under the stated context and phase conditions.Source: §A.2 · p. 40

A.3 Progress

• Canonical forms constrain typed values to the shapes required by their types, including the listed product, list, element, attribute, and element-instance forms.These forms support the case analysis used to show that well-typed terms can step.Source: §A.3 · p. 40
• A well-typed computation is either a value or can take a computation step.This is Theorem A.13’s progress result, proved by mutual induction over the computation typing judgment and related lemmas.Source: §A.3 · p. 40
• The progress proof covers component initialization and state operations by showing their well-typed cases can take steps.For useState, initialization writes the initial value into the component state; state access requires the relevant location to be defined.Source: §A.3 · p. 45
• Every well-typed top-level configuration can take a top-level step.The proof lifts computation progress to the top-level judgment, handling a value by an event step and a non-value by its computation step.Source: §A.3 · pp. 45–46

A.4 Preservation

• For computation and body substitution, typings under Φ1 and Φ2 yield typings under Φ = Φ1 Z Φ2; the passages also state context extension and order preservation results.Source: §A.4 · pp. 46–47
• A Pure computation step preserves its type and effect, and leaves the heap unchanged.The theorem applies to any heap H when a computation typed with effect Pure steps from H to H′.Source: §A.4 · p. 47
• During state initialization, preservation extends the hook’s store typing and heap consistently while substituting the initialized value and setter into the body.The proof chooses an extended store typing at the new hook location and extends the heap typing with the initialized state.Source: §A.4 · p. 51
• A subsequent state step preserves body typing using the existing hook value, with the heap unchanged.The state-step case requires the hook’s state type to be present in the typing context; initialization cannot occur in this case.Source: §A.4 · pp. 51–52
• Mutable computation steps preserve typing while allowing fresh extensions of state and heap contexts and preserving their ordering relation.The proof handles a let-step by extending the fresh context with the unchanged continuation context; other computation cases follow the pure-preservation argument, with subsumption having no effect on the derivation.Source: §A.4 · pp. 52–53
• Fresh component initialization adds an instance with empty state and rerender disabled, while the proof extends the typing context and derives the continuation’s typing.The new heap entry maps the fresh instance to st : ∅ and rerender : ff.Source: §A.4 · pp. 57–58
• A well-typed component instance taking a top-level step admits successor contexts related by fresh extension, as stated by preservation for ⇝⊤.The theorem quantifies over successor component and heap contexts and a successor permission context.Source: §A.4 · p. 60
• The preservation proof proceeds by small-step case analysis, including event dispatch and component-update cases.For the event case, the proof invokes preservation for ⇝; the component-update case retains the existing component and heap contexts.Source: §A.4 · pp. 59–60

A.5 Consistency

• Initialization can only extend the heap: existing state entries and rerender flags are preserved by the heap ordering.The ordering compares state maps by extension while requiring rerender flags to remain equal.Source: §A.5 · pp. 60–61
• Heap-preserving computation steps remain valid in a greater heap, provided the heaps are ordered as defined.The heap-lifting lemmas cover computations and component bodies, allowing the proof to carry successor-phase steps across initialization changes.Source: §A.5 · pp. 60, 62
• A component that satisfies the stated typing, separation, and freshness conditions remains consistent with its resulting value after evaluation.Theorem 4.9 establishes this for a sequence of steps in either the initialization or successor phase.Source: §A.5 · pp. 60, 64
• The consistency argument combines initialization monotonicity with heap lifting to preserve successor evaluation across heap growth.Single-step component consistency and preservation support the induction over the initialization sequence.Source: §A.5 · pp. 60, 65

B.1 Type Preservation

• Under a valid realization, delta lookups for flags and state labels are typed as references to Bool and the translated state type, respectively.Source: §B.1 · p. 65
• Typed source values translate to values of the corresponding translated type under the realized hook environment.The preservation condition requires the realization to cover the identifiers in the value.Source: §B.1 · p. 66
• Typed computations translate to computations of the corresponding translated type when the realization covers their identifiers.Source: §B.1 · p. 69
• Typed successor bodies translate to elements; for useState, the translation reads the state reference and its setter writes the new value and sets the flag.Source: §B.1 · pp. 73–74
• Typed initial bodies translate to the computation type when the initial label set extends the body’s labels and the delta typing covers the added labels.The theorem states the translated result has type Acomp.Source: §B.1 · p. 75

Heap/Store Preservation

• Appending two well-formed stores preserves well-formedness when their domains are disjoint.The resulting store and location typing are the unions of the respective inputs.Source: §B.1 · pp. 77–78
• Well-typed state stores translate to target stores with the translated location typing, provided their locations lie within the component’s allocated locations.The assumptions also require a valid renaming for the store’s identifiers.Source: §B.1 · p. 78
• Well-typed heaps translate to well-typed target heaps when the renaming is valid for the heap’s identifiers.The theorem follows from intermediate heap preservation with the source heap’s typing environment as the target environment.Source: §B.1 · pp. 78–79

B.2.1 Substitution

• The substitution proofs use mutual induction across values, computations, and bodies, with δ-elimination lemmas handling variables in the range of δ.For body substitution, the target variable must not be in img(δ); bound-variable and scope conventions are handled by α-conversion and freshness assumptions.Source: §B.2.1 · pp. 80, 84
• Substitution commutes with value and computation translations, and with successor- and initial-body translations when the substituted variable is outside img(δ).The body lemmas also require the relevant translations and substituted value to be well-defined.Source: §B.2.1 · pp. 80, 82, 84, 86

B.2.2 ϱ-Extension

• Extending ϱ leaves well-defined translations of values, computations, successor bodies, initial bodies, and handlers unchanged.The stated equalities apply when ϱ is a subset of the extended environment ϱ′.Source: §B.2.2 · pp. 87–88

B.2.3 Specialization

• A body translated with the nonexistent pointer ⊥ has the same translation as with any concrete pointer, for both successor and initial phases.The successor and initial specialization lemmas each require the translation at ⊥ to be well-defined.Source: §B.2.3 · pp. 88–89

B.2.4 δ-Elimination

• After substituting ϱ(p) for a flagged variable, the flag entry can be removed without changing successor- or initial-body translations.The corresponding label-elimination lemmas allow the same removal using ϱ(p, ℓ).Source: §B.2.4 · p. 89

B.2.5 Simulation.

• Target-language let-transitivity lifts a reduction of a let-bound computation to the enclosing let expression.The lemma is proved by lifting each intermediate reduction step through EC-Let.Source: §B.2.5 · p. 89
• Pure computation steps preserve typing and leave the heap unchanged while their translations take a corresponding reduction step.The theorem assumes a well-typed Pure computation, identifier compatibility, and a source step; it concludes that the target computation remains well typed and the heap is unchanged.Source: §B.2.5 · pp. 89–90
• Successor-body steps preserve body typing and identifier compatibility, and the translated successor bodies simulate the source step.The theorem applies when the body’s label set is included in the component’s state typings; its proof uses pure simulation for let steps.Source: §B.2.5 · pp. 94–95
• Initial-body steps preserve the component and initial-body typings under a permitted initialization extension, while the translated initial bodies simulate the source step.The result also preserves identifier compatibility between the transformed body, initial body, and resulting heap.Source: §B.2.5 · p. 97

Simulation

• The translated state setter writes the new value to a fresh reference and marks the component for rerendering.The construction is shown as a function that assigns the supplied value to the location and sets the component’s rerender flag to true.Source: §B.2.5 · pp. 100, 107
• For a well-typed source computation step with a related reference environment, Theorem 6.5 establishes updated contexts and an extended environment for the simulation.The proof proceeds by induction on the computation-step derivation.Source: §B.2.5 · p. 100
• The proof handles initialization and successor transitions using simulation results that provide updated contexts and reference environments.The initialization case invokes the initialization simulation theorem, while the successor case invokes the successor simulation theorem.Source: §B.2.5 · pp. 107–108

• Initialization cases derive typing for component initialization and translate it into target code that initializes the value before applying compInst.The text and tag initialization cases are also included in the case analysis.Source: §B.2.5 · pp. 111–112
• Clicking a true tag instance runs its handler and then its clicks, while clicking a false tag instance runs only its clicks.The proof derives the corresponding typing judgments for these click cases.Source: §B.2.5 · p. 114
• The remaining operational cases are handled by analogous arguments for text and tag updates, attribute runs, and click-handler runs.The proof states that text and tag updates are analogous to their initialization cases, and attribute runs are analogous to text clicks.Source: §B.2.5 · pp. 115–116
• Component updates preserve the typing derivation and simulate rerendering by clearing the flag, reinitializing the translated component, and applying compInst.The update case establishes that the rerender flag is true before the target reduction.Source: §B.2.5 · pp. 116–117