Agda.Utils.SemiRing

Documentation

class SemiRing a where

Methods

oplus :: a -> a -> a

otimes :: a -> a -> a

Instances

SemiRing PartialOrdering

Partial ordering forms a semiring under supremum (disjunction) and composition (transitivity, sequencing)

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)