Python Effects as Sheaf Sections

JuGeo models Python's five effect families — exceptions, state, async, generators, and context managers — as sheaf-theoretic structures on the semantic site, enabling compositional effect reasoning and precise compatibility checking at component boundaries.

🕑 18 min read Core Concept

📋

On this page: Sheaf model of effects · 5 effect families · Comparison with F* Dijkstra monads · Annotations · Python examples

The Sheaf Model of Effects

An effect is any observable computational behaviour other than the direct mapping of input values to output values. Effects — raising exceptions, reading or writing mutable state, performing I/O, suspending execution — are exactly the phenomena that make compositional verification hard. They create implicit dependencies between components that are not visible in type signatures alone.

JuGeo treats each Python function as an object in the semantic site \((\mathcal{C}, J)\) and models its effects as sections of an effect sheaf \(\mathcal{E}\). Formally, an effect section \(e \in \mathcal{E}(U)\) over a coordinate \(U\) is a predicate set describing the observable behaviours of \(U\) on any input. The restriction map \(\rho_{V \hookrightarrow U}\) propagates effect obligations along call edges: if \(U\) calls \(V\), then \(U\)'s effects include the restriction of \(V\)'s effects to \(U\)'s context.

Effect Sheaf Condition

\[ \mathcal{E}(U) \;\cong\; \varprojlim\Bigl(\prod_i \mathcal{E}(U_i) \;\rightrightarrows\; \prod_{i,j} \mathcal{E}(U_i \times_U U_j)\Bigr) \]

This condition states that the total effect of a module \(U\) is exactly determined by the effects of its components \(\{U_i\}\), provided they are compatible on shared boundaries. Incompatibilities are Čech H¹ obstructions in the effect sheaf — precisely the “effect leaks” that cause unexpected exceptions or state corruption under composition.

Five Effect Families

EXCEPTIONS

Coordinate Forks

Exceptions split the execution path into a normal return and one or more exceptional branches. JuGeo models this as a coordinate fork: the function's coordinate splits into a success fiber and a failure fiber, each carrying its own judgment and trust level.

STATE

Scope Sections

Mutable state (globals, instance variables, closures) is modelled as a scope section: a local section of the state sheaf over the coordinate's lexical scope. Writes are extension maps; reads are restriction maps on scope sections.

ASYNC

Suspended Morphisms

Coroutines and async def functions are modelled as suspended morphisms: arrows in the site that carry a suspension point, splitting execution across event loop ticks. Each await-point becomes a restriction map to a temporal subsection.

GENERATORS

Fiber Restrictions

Generators yield a sequence of sections — one per yield — modelled as a fiber restriction sequence over an index coordinate. Generator state between yields is the transition data between consecutive fibers in the sequence.

CONTEXT MANAGERS

Covering Families

Context managers (with blocks) provide resources for a bounded scope. JuGeo models them as covering families: the __enter__/__exit__ pair defines a cover of the enclosing coordinate, with the managed resource as the gluing data on the intersection.

💡

Effect lattice. The five families form a lattice under the “subsumes” relation. A function that raises exceptions is strictly less pure than one that does not; one that mutates state is less pure than a read-only function. JuGeo uses this lattice to compute the meet of effect levels in composed trust judgments, so the composed trust can never exceed the least pure component.

Comparison with F* Dijkstra Monads

F*'s Dijkstra monad framework assigns a predicate transformer to each effectful computation. JuGeo's effect sheaf approach is structurally related but differs in representation and target language. The table below highlights the key correspondences and differences.

Concept	F* / Dijkstra Monads	JuGeo
Effect specification	Predicate transformer \(\mathrm{wp}: (a \to \mathrm{Type}) \to \mathrm{Type}\)	Sheaf section \(e \in \mathcal{E}(U)\) with restriction maps
Exceptions	`ExnST` monad; exception wp	Coordinate fork; H⁰ obstruction on the failure fiber
Mutable state	`ST` monad; heap predicate transformer	Scope section; alias analysis via `heap_aliasing` encoding
Async / concurrency	Not built-in; requires external libraries	Suspended morphisms; modeled through the public geometry and descent layers
Effect composition	Monad transformers	Sheaf product; compatible restrictions auto-composed via descent
Verification target	F* programs (ML-like syntax)	Existing Python codebases; no rewriting required
Proof obligation	Discharged by F*'s SMT backend (Z3)	Discharged by Z3/CVC5 via JuGeo encodings layer
Partial verification	Requires full type annotations	Supports partial annotation; unannotated portions carry NONE trust

The key practical advantage of JuGeo's sheaf approach is applicability to existing Python code without syntactic transformations. The developer need not rewrite functions in a monadic style. JuGeo infers effect sections from the code's structure and from optional annotations, then verifies compatibility.

Effect Annotations

JuGeo's stable public API for effect reasoning is currently geometry-first rather than decorator-first. In practice you inspect coordinates, runtime effect summaries, and descent compatibility, then use the CLI to prove, repair, or align the code that those summaries refer to.

python

from jugeo.geometry.site import Coordinate, CoordinateKind

coord = Coordinate(("mymod", "payments", "process_payment"), kind=CoordinateKind.FUNCTION)
report = coord.runtime_effects()

print(report["coordinate"])
print(report["effects"])

Python Examples

Querying effect sections across a module:

python

from jugeo.geometry.site import Coordinate, CoordinateKind

coord = Coordinate(("mymod", "payments", "process_payment"), kind=CoordinateKind.FUNCTION)

print(coord.program_loader())
print(coord.runtime_effects())

Checking effect compatibility at a call boundary:

python

from jugeo.geometry.site import Coordinate, CoordinateKind

caller = Coordinate(("mymod", "api", "handle_request"), kind=CoordinateKind.FUNCTION)
callee = Coordinate(("mymod", "db", "query"), kind=CoordinateKind.FUNCTION)

print(caller.runtime_effects())
print(callee.runtime_effects())

Generator fiber analysis:

python

from jugeo.geometry.site import Coordinate, CoordinateKind

coord = Coordinate(("mymod", "pipeline", "batch_records"), kind=CoordinateKind.FUNCTION)
print(coord.runtime_effects())
print(coord.callable_surface())