Agda- A dependently typed functional programming language and proof assistant

Safe HaskellSafe-Inferred



class SemiRing a whereSource


oplus :: a -> a -> aSource

otimes :: a -> a -> aSource


SemiRing Distance 
SemiRing Weight 
SemiRing Occurrence

Occurrence is a complete lattice with least element Mixed and greatest element Unused.

It forms a commutative semiring where oplus is meet (glb) and otimes is composition. Both operations are idempotent.

For oplus, Unused is neutral (zero) and Mixed is dominant. For otimes, StrictPos is neutral (one) and Unused is dominant.

SemiRing Edge

These operations form a semiring if we quotient by the relation "the Occurrence components are equal".

SemiRing a => SemiRing (Maybe a)