Dynamic Effect Type Inference

[datvo06]

Aims to close #448 and #664.

As noted in some of our discussions, static effect typing is pretty impossible given how dynamic we are in selecting handlers and dispatching effects. So this PR adds a dynamic effect type inference. Even though it is dynamic, it should be able to do what we intended, specifically requiring or restricting side effects.

It does this by folding over apply: we install an interpretation of apply that records which ops fire, then evaluate the term under it to get the term's effect row: the set of operations it performs.
To help with this process, I created usesof (sibling of fvsof and typeof) which records the effect set.

Concretely the PR adds:

• usesof(term) (aliased effectsof): the effect row of a term.
• effect_type(term): the pair $\langle \tau, \epsilon \rangle$ of the result type from typeof and the effect row from usesof, folded over the same apply.
• Uses[...] on a return type, read by a new @final Operation.__uses_rule__ method, plus check_uses(op, body), which returns the effects body performs that the op's declared Uses[...] does not cover. This is the Support effect type annotations #448 checker: empty means the declaration holds, and it is transitively closed because usesof unions the whole term.
• Computation on a callback argument, so a higher-order op folds the effects hidden inside its callback instead of the checker hard-coding which ops are higher-order.
• Requires(...) on an argument plus check_requires(term) (this is from Supporting Refinement Type in conjunction with Effect type for stronger security emphasis #664 but I think this is quite small so I left it in): an argument satisfies Requires(X) iff X is in usesof(arg).
• toolsof / reachable_tools / check_tools in handlers/llm: the static tool graph an LLM template can reach, computed by reifying to a term and reading .tools, with no LLM call. check_tools(fn, *allowed) is the tool-graph analog of check_uses.

[datvo06]

A few honest caveats, since dynamic inference is not free:

• usesof is path insensitive over the reified term, so it is an over-approximation and it needs the term to be straight-line: native Python control flow gets resolved when the term is built, so a branchy function can under-approximate. The same precondition applies to reachable_tools.
• The Computation callback runs the callback on an opaque placeholder and raises an error (UnsoundCallbackFold) when the callback inspects that placeholder through the operator protocol (==, arithmetic, len, calling it, indexing). But object identity (is), type() and isinstance bypass the protocol and it cannot catch them, so a callback branching on those under-approximates silently. I've put these edge cases into the tests.

[datvo06]

I deferred the following LLM-specific features pending on #694 :

• The LLM tool restriction from #448 (only offering a template the tools it lists) belongs on the tool-assembl, not on Template.tools, so it lands separately once that seam is in place, I think after Add doctest validation stage to Callable decoding #694 landed, I can wire these in easily.
• Uses members that are Operation subclasses or string self-references, the build-time validation of annotations at op construction, and the usage multiset (usagesof) plus handler discharge.

[datvo06]

I checked most of the logics here, but I think I can review more until marking it ready for review.

[eb8680]

This looks interesting, but I think the specification of the intended behavior from #448 and #664 needs to be a lot clearer and a lot more grounded in relevant PL literature and the semantics of effectful before we can actually implement anything (or trust anything cooked up by Claude).

I also think there are many outstanding issues in effectful and downstream that are higher priority, especially given that lexical scoping already solves closely related problems (#590) and the large amount of work this will inevitably need before it's useable in practice.

[datvo06]

This looks interesting, but I think the specification of the intended behavior from #448 and #664 needs to be a lot clearer and a lot more grounded in relevant PL literature and the semantics of effectful before we can actually implement anything.

Got it. I ended up at this after failing to find a good relevant paper and then designing it based on stateless (we use apply instead of yield). But I will keep looking at PL literature to see if something relevant come up.

Will also work on #590!