Syntactic polynomial objects, promoted to a kind.

Values of a polynomial functor p evaluated at x.

The constructors mirror the polynomial grammar. EP and ES wrap the standard product and coproduct of Haskell ((,) and Either); they are not reimplemented, only tagged so that the polynomial shape remains inspectable.

ET is the Dirichlet tensor: a pair of positions with one function out of the product of direction sets. This cannot be built from a pair of ordinary Eval values, which is why Pos and Dir are needed.

EC is the composition product: a p-position with a q-component hung on each p-pin, and a path (dp, dq) into x.

Position set of a polynomial.

For a value of p(x), 'Pos p' is the index type of positions.

Direction set of a polynomial.

For a value of p(x) at a given position, 'Dir p' is the domain of the function into x.

Sum gets a flat direction space Either (Dir p) (Dir q). This is an over-approximation: only the branch selected by the position is in-fibre. It is nonetheless the right shape for dynamics, where the input direction is supplied after the position is observed: a wrong-branch direction is simply off-fibre. The netlist view (Netlist) remains position-dependent and still does not admit a Sum instance.

For Comp, Dir ('Comp p q) = ('Dir p, 'Dir q) is the same flat approximation: the q-position (hence its honest pin set) depends on which p-direction was taken. Exact for Sum-free factors with uniform directions — the monomial fragment.

Reassemble a value after taking it apart. This is the executable form of the round-trip law fromNet (toNet v) ≡ v.

Left unitor for the Dirichlet tensor: Y ⊗ p ≅ p.

The Y factor is degenerate; collapse via fromNet on the other factor.

Inverse left unitor: p -> Y ⊗ p.

Right unitor for the Dirichlet tensor: p ⊗ Y ≅ p.

Inverse right unitor: p -> p ⊗ Y.

Read the bundle map off a Morphism at a chosen position.

Instantiating the output as Dir p turns an opaque morphism into a forward position plus a backward direction map — the crux that makes parT a few lines.

Functorial action of the Dirichlet tensor on Netlist factors.

Map each tensor factor through its morphism independently; backward directions thread through both pullback maps.

Composition-product view of a nested evaluation Eval p (Eval q x).

Correctness iso (right): Eval (Comp p q) x ≅ Eval p (Eval q x).

Nested evaluation from a composition-product value.

Correctness iso (left): inverse of nestedToComp.

Left unitor for the composition product: Y ◁ p -> p.

Inverse left unitor for the composition product: p -> Y ◁ p.

Right unitor for the composition product: p ◁ Y -> p.

Inverse right unitor for the composition product: p -> p ◁ Y.

Left associator for the composition product: ((p ◁ q) ◁ r) -> (p ◁ (q ◁ r)).

Right associator for the composition product.

Pair two polynomial values into a Dirichlet tensor (p ⊗ q).

Each factor contributes its position and pin assignment; the result is one joint assignment over the product of direction sets.

A morphism p -> q in Poly, encoded as a natural transformation between the evaluated functors.

By the Yoneda / sigma universal property, this is equivalent to a bundle map: a function on positions together with a contravariant family of functions on directions.

Konst and Depend extend the original Poly sketch so that backward maps can depend on the current position, giving point-dependent lenses.

Interpret a Morphism as a natural transformation.

The monomial interface: i directions (input), o positions (output).

The general point-dependent lens.

Forward pass get :: a -> b; backward pass put :: a -> db -> da depends on the current position.

>>> let l = lens show (\n d -> n + d) :: Morphism (Mono Int Int) (Mono Int String)
>>> let (v, put) = applyLens l 40 in (v, put 2)
("40",42)

The position-independent dagger case.

Expressible without Konst or Depend.

>>> let d = dagger (+1) (subtract 1) :: Morphism (Mono Int Int) (Mono Int Int)
>>> let (v, put) = applyLens d 5 in (v, put 6)
(6,5)

Apply a monomial morphism as a lens: (get, put).

Prism: match on a sum-like source, build from the focused branch.

>>> let p = prism (\case Left n -> Left n; Right s -> Right (Right s)) Left :: Morphism (Mono (Either Int String) (Either Int String)) ('Sum (Mono Int Int) (Mono (Either Int String) (Either Int String)))
>>> case runMorphism p (EP (EK (Left 7), EE id)) of ES (Left (EP (EK n, EE k))) -> (n, k 1)
(7,Left 1)

Extract the forward match of a prism.