ch:coeffects: ch:coeffects

Problem and invariant. Compute flat implicit-name requirements and structural occurrence counts. Maintain that the flat list contains every implicit access exactly once and that each structural count equals the number of free occurrences of its name.

Representation. Use one expression tree and two result representations: a duplicate-free name list for flat requirements and an association list of natural counts for structural requirements. A single map from names to grades could represent both, but it would blur union’s idempotence and addition’s repeated-use behavior.

First complete version. Constants contribute neither requirement. An implicit access contributes a singleton flat list; an ordinary variable contributes count one. Addition recursively combines both children by union or count addition.

Remaining cases in metatheory order. Add duplicate elimination for implicit names, association-list lookup, count insertion, and count merging. Then check the scalar substitution calculation $2\times 2=4$, which corresponds to replacing a twice-used variable by a twice-demanding expression.

A failing version. Combine repeated counts by maximum instead of addition. The program still typechecks and audits cleanly, but $x$ receives count one rather than three in the named repeated-use term.

Acceptance test. Run the four Appendix E commands. Require the empty constant demand, the width singleton, the two-name union, counts $x=3,y=1$, the grade product four, the exact six-line transcript, and an empty audit. Restore and replay after mutation.

Mathematical boundary. The analyzer omits typing derivations, evaluation strategies, and context transformations. It illustrates the Set models and lemma 53.6; it proves no subject-reduction theorem.