    module Agda.Utils.SemiRing where

    -- | Semirings (<https://en.wikipedia.org/wiki/Semiring>).

    class SemiRing a where
      ozero  :: a
      oone   :: a
      oplus  :: a -> a -> a
      otimes :: a -> a -> a

    instance SemiRing () where
      ozero :: ()
    ozero      = ()
      oone :: ()
    oone       = ()
      oplus :: () -> () -> ()
    oplus  ()
    _ ()
    _ = ()
      otimes :: () -> () -> ()
    otimes ()
    _ ()
    _ = ()

    instance SemiRing a => SemiRing (Maybe a) where
      ozero :: Maybe a
    ozero = Maybe a
    forall a. Maybe a
    Nothing
      oone :: Maybe a
    oone  = a -> Maybe a
    forall a. a -> Maybe a
    Just a
    forall a. SemiRing a => a
    oone

      oplus :: Maybe a -> Maybe a -> Maybe a
    oplus Maybe a
    Nothing Maybe a
    y = Maybe a
    y
      oplus Maybe a
    x Maybe a
    Nothing = Maybe a
    x
      oplus (Just a
    x) (Just a
    y) = a -> Maybe a
    forall a. a -> Maybe a
    Just (a -> a -> a
    forall a. SemiRing a => a -> a -> a
    oplus a
    x a
    y)

      otimes :: Maybe a -> Maybe a -> Maybe a
    otimes Maybe a
    Nothing Maybe a
    _ = Maybe a
    forall a. Maybe a
    Nothing
      otimes Maybe a
    _ Maybe a
    Nothing = Maybe a
    forall a. Maybe a
    Nothing
      otimes (Just a
    x) (Just a
    y) = a -> Maybe a
    forall a. a -> Maybe a
    Just (a -> a -> a
    forall a. SemiRing a => a -> a -> a
    otimes a
    x a
    y)

    -- | Star semirings
    -- (<https://en.wikipedia.org/wiki/Semiring#Star_semirings>).

    class SemiRing a => StarSemiRing a where
      ostar :: a -> a

    instance StarSemiRing () where
      ostar :: () -> ()
    ostar ()
    _ = ()

    instance StarSemiRing a => StarSemiRing (Maybe a) where
      ostar :: Maybe a -> Maybe a
    ostar Maybe a
    Nothing  = Maybe a
    forall a. SemiRing a => a
    oone
      ostar (Just a
    x) = a -> Maybe a
    forall a. a -> Maybe a
    Just (a -> a
    forall a. StarSemiRing a => a -> a
    ostar a
    x)