How a composite p :.: q of thin profunctors decides its arrows. In general HasArrow (p :.: q) a c is an existential over the objects b of the middle category (the join ⋁_b p(a,b) ∧ q(b,c) in the enriching Bool), which a Constraint cannot express. But when the left leg is corepresented (f a ≤ b, a companion) or the right leg represented (b ≤ g c, a conjoint) the middle object is determined and the existential collapses to a substitution: q (f a) c, respectively p a (g c). The strategy is chosen by the closed family ThinCompStrategy from the shape of the legs, so that the one ThinProfunctor instance for :.: never overlaps with anything; a composite of two non-representable legs falls back to BySearch, which enumerates the middle category and decides both legs at each object (Search). (Star and Costar have the same two shapes, but functors between thin kinds are written as FunctorForReps here, so Rep/Corep cover them.)

The join ⋁_b p(a,b) ⊗ w_b of an edge out of a with whatever the vector holds for where that edge lands: one row of the matrix of p against a vector, over the given middle objects. The objects and the vector are walked in step, so ws is always the vector cut down to bs.

This is the module's one join. Composing two profunctors multiplies by a column read off the right-hand one (MatMul); the closure multiplies by the previous iterate (Walks), which is what lets that iterate be computed once instead of once per pair.

One column of the matrix of an enriched profunctor: its hom-objects into c, over the given objects.

Matrix multiplication over a list of middle objects, ⋁_b p(a,b) ⊗ q(b,c): the hom-object of the composite of two enriched profunctors when the middle category is enumerable. The type-level twin of Proarrow.Category.Instance.FinRel.

The arrows of a composite by search: is there an object b among bs with both p a b and q b c? Over the full object list this is the join ⋁_b p(a,b) ∧ q(b,c), which is MatMul in the enriching BOOL.

Walk the object list deciding both legs at each object; a hit is the composite, and a miss reduces the search to the tail of the list.

An actual composite proves the search succeeds: locate its middle object in the list, then at that position both legs hold and the disjunction is TRU whatever the rest of the list says.

Whether a composite decides its arrows, by the same strategy as ComposeThin: a representable leg is substituted away and the other leg decided, a search is decided by running it. This is what makes composites decidable in turn, so that searches can nest.

A walk of at most n steps along p, finished by an arrow of the base category. Its hom-object in any enriching category is Walks: at BOOL the truth of the walk, decided with the path as witness; at COST the shortest distance.

The hom-object of a walk of at most n steps, in any enriching category v: an arrow of the base, or an edge followed by one entry of the previous iterate (WalkRow). Naming the whole iterate rather than a shorter walk per pair is what keeps this affordable. At BOOL it is the truth of Walk, at COST the shortest distance, computed by GHC at the type level and by row at the value level.

The n-th iterate of the fixed point for a fixed target b: the hom-object of the walks of at most n steps into b, one entry per object, in the order of Objects. It starts as the column of the base hom-objects, there being no step to take yet, and grows by NextRow.

Each iterate is written in terms of the whole previous one, so it is computed once and read by every object. That sharing is what makes the fixed point affordable: the work is the number of steps times the square of the number of objects, where a recursion per pair of objects would instead cost the number of objects to the power of the number of steps.

One more step, taken for every object at once: an arrow of the base, or an edge into the previous iterate (MatVec).

The Kleene closure of p: walks of at most as many steps as there are objects, which is all of them, since a shortest walk never revisits an object. It is the free category on the graph p in whatever p is enriched in: at BOOL the reflexive-transitive closure of a relation, with the path as witness (decide); at COST the free Lawvere metric space, with the shortest distances (withProObj) and the shortest paths (shortest).

What the closure needs of its ingredients: a quantale to compute in, an enriched graph over an enumerable enriched base, and a known number of steps.

A walk graded by its cost: each piece comes with a budget, an arrow of v into the piece's hom-object, and the grade of the walk is the tensor of the budgets. A walk at grade d is a generalised element of the closure, d ~> Walks v n p a b (underlyingAt), and shortest produces one at grade exactly the hom-object.

The n-th iterate reflected to the value level: every object paired with its own entry, which is exactly the hom-object of the walks from it. row builds one and everything that needs a shorter walk reads it, so the value level shares its work the same way the type level does.

The n-th iterate: the base hom-objects, then one more step for every object at a time.

Object evidence for the hom-object of a walk: read the object's own entry out of an iterate.

The same, for a caller that is not already holding the iterate.

Object evidence for one summand of MatVec: an edge and its tensor with the entry after it.

Object evidence for the join over the given middle objects.

A graded walk is a generalised element of the closure: inject it into the join at its middle object.

An edge with a budget, followed by a generalised element of the shorter walks.

The injection of one summand into the join over the middle objects.

A walk of pieces at the unit, as a generalised element at the unit.

The best walk between two points, graded by exactly their hom-object: a shortest path at COST, a path or the absence of one at BOOL. At every join it keeps the summand the join is (minIs); a pair no walk connects gets the empty walk at InitialObject.

The best walk through one of the given middle objects.

A graded walk together with a unit into its grade is a walk of pieces at the unit: the budget splits over the pieces (splitUnit) and each piece is read off with enriched.

The action of the base on a closure: the triangle inequality. It holds for the best walks but is not derived structurally, so it is a checkedArrow.