Weighted search is an essential component of many fundamental and useful
algorithms.
Despite this, it is relatively under explored as a computational effect,
receiving not nearly as much attention as either depth- or breadth-first
search.
This paper explores the algebraic underpinning of weighted search,
and demonstrates how to implement it as a monad transformer.

The development first explores breadth-first search, which can be expressed as
a polynomial over semirings. These polynomials are generalised to the free
semimodule monad to capture a wide range of applications, including
probability monads, polynomial
monads, and monads for weighted search.
Finally, a monad transformer based on the free semimodule monad is introduced.
Applying optimisations to this type yields an implementation of pairing
heaps, which is then used to implement Dijkstra's algorithm and efficient
probabilistic sampling.
The construction is formalised in Cubical Agda and implemented in Haskell.