    {-# LANGUAGE DataKinds           #-}
    {-# LANGUAGE DeriveDataTypeable  #-}
    {-# LANGUAGE KindSignatures      #-}
    {-# LANGUAGE ScopedTypeVariables #-}

    -----------------------------------------------------------------------------
    -- |
    --   A tropical semiring is an extension of another totally ordered
    --   semiring with the operations of minimum or maximum as addition.
    --   The extended semiring is given positive or negative infinity as
    --   its 'zero' element, so that the following hold:
    --
    -- @
    --'plus' 'Infinity' y = y
    --'plus' x 'Infinity' = x@
    --
    --
    --   i.e., In the max-plus tropical semiring (where 'plus' is 'max'),
    --   'Infinity' unifies with the typical interpretation of negative infinity,
    --   and thus it is the identity for the maximum, and in the min-plus tropical
    --   semiring (where 'plus' is 'min'), 'Infinity' unifies with the typical
    --   interpretation of positive infinity, and thus it is the identity for the minimum.
    --
    -----------------------------------------------------------------------------

    module Data.Semiring.Tropical
      ( Tropical(Infinity,Tropical)
      , Extrema(Minima,Maxima)
      , Extremum(extremum)
      , EProxy(EProxy)
      ) where

    import Data.Data (Data)
    import Data.Semiring (Semiring(..))
    import Data.Star (Star(..))
    import Data.Typeable (Typeable)

    -- done for haddocks, to make sure -Wall works
    import qualified Data.Monoid as Monoid

    -- | On older GHCs, 'Data.Proxy.Proxy' is not polykinded, so we provide our own proxy type for 'Extrema'.
    --   This turns out not to be a problem, since 'Extremum' is a closed typeclass.
    data EProxy (e :: Extrema) = EProxy

    -- | A datatype to be used at the kind-level. Its only
    --   purpose is to decide the ordering for the tropical
    --   semiring in a type-safe way.
    data Extrema = Minima | Maxima

    -- | The 'Extremum' typeclass exists for us to match on
    --   the kind-level 'Extrema', so that we can recover
    --   which ordering to use in the `Semiring` instance
    --   for 'Tropical`.
    class Extremum (e :: Extrema) where
      -- unfortunately this has to take a `Proxy` because
      -- we don't have visual type applications before GHC 8.0
      extremum :: EProxy e -> Extrema

    instance Extremum 'Minima where
      extremum :: EProxy 'Minima -> Extrema
    extremum EProxy 'Minima
    _ = Extrema
    Minima
      {-# INLINE extremum #-} -- just to be safe

    instance Extremum 'Maxima where
      extremum :: EProxy 'Maxima -> Extrema
    extremum EProxy 'Maxima
    _ = Extrema
    Maxima
      {-# INLINE extremum #-} -- just to be safe

    -- | The tropical semiring.
    --
    --   @'Tropical' ''Minima' a@ is equivalent to the semiring
    --   \( (a \cup \{+\infty\}, \oplus, \otimes) \), where \( x \oplus y = min\{x,y\}\) and \(x \otimes y = x + y\).
    --
    --   @'Tropical' ''Maxima' a@ is equivalent to the semiring
    --   \( (a \cup \{-\infty\}, \oplus, \otimes) \), where \( x \oplus y = max\{x,y\}\) and \(x \otimes y = x + y\).
    --
    -- In literature, the 'Semiring' instance of the 'Tropical' semiring lifts
    -- the underlying semiring's additive structure. One might ask why this lifting doesn't
    -- instead witness a 'Monoid.Monoid', since we only lift 'zero' and 'plus' - the reason is
    -- that usually the additive structure of a semiring is monotonic, i.e.
    -- @a '+' ('min' b c) == 'min' (a '+' b) (a '+' c)@, but in general this is not true.
    -- For example, lifting 'Monoid.Product' 'Word' into 'Tropical' is lawful,
    -- but 'Monoid.Product' 'Int' is not, lacking distributivity: @(-1) '*' ('min' 0 1) '/=' 'min' ((-1) '*' 0) ((-1) '*' 1)@.
    -- So, we deviate from literature and instead
    -- witness the lifting of a 'Monoid.Monoid', so the user must take care to ensure
    -- that their implementation of 'mappend' is monotonic.
    data Tropical (e :: Extrema) a
      = Infinity
      | Tropical a
      deriving
        ( Tropical e a -> Tropical e a -> Bool
    (Tropical e a -> Tropical e a -> Bool)
    -> (Tropical e a -> Tropical e a -> Bool) -> Eq (Tropical e a)
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    forall (e :: Extrema) a.
    Eq a =>
    Tropical e a -> Tropical e a -> Bool
    $c== :: forall (e :: Extrema) a.
    Eq a =>
    Tropical e a -> Tropical e a -> Bool
    == :: Tropical e a -> Tropical e a -> Bool
    $c/= :: forall (e :: Extrema) a.
    Eq a =>
    Tropical e a -> Tropical e a -> Bool
    /= :: Tropical e a -> Tropical e a -> Bool
    Eq
        , Int -> Tropical e a -> ShowS
    [Tropical e a] -> ShowS
    Tropical e a -> String
    (Int -> Tropical e a -> ShowS)
    -> (Tropical e a -> String)
    -> ([Tropical e a] -> ShowS)
    -> Show (Tropical e a)
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    forall (e :: Extrema) a. Show a => Int -> Tropical e a -> ShowS
    forall (e :: Extrema) a. Show a => [Tropical e a] -> ShowS
    forall (e :: Extrema) a. Show a => Tropical e a -> String
    $cshowsPrec :: forall (e :: Extrema) a. Show a => Int -> Tropical e a -> ShowS
    showsPrec :: Int -> Tropical e a -> ShowS
    $cshow :: forall (e :: Extrema) a. Show a => Tropical e a -> String
    show :: Tropical e a -> String
    $cshowList :: forall (e :: Extrema) a. Show a => [Tropical e a] -> ShowS
    showList :: [Tropical e a] -> ShowS
    Show
        , ReadPrec [Tropical e a]
    ReadPrec (Tropical e a)
    Int -> ReadS (Tropical e a)
    ReadS [Tropical e a]
    (Int -> ReadS (Tropical e a))
    -> ReadS [Tropical e a]
    -> ReadPrec (Tropical e a)
    -> ReadPrec [Tropical e a]
    -> Read (Tropical e a)
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    forall (e :: Extrema) a. Read a => ReadPrec [Tropical e a]
    forall (e :: Extrema) a. Read a => ReadPrec (Tropical e a)
    forall (e :: Extrema) a. Read a => Int -> ReadS (Tropical e a)
    forall (e :: Extrema) a. Read a => ReadS [Tropical e a]
    $creadsPrec :: forall (e :: Extrema) a. Read a => Int -> ReadS (Tropical e a)
    readsPrec :: Int -> ReadS (Tropical e a)
    $creadList :: forall (e :: Extrema) a. Read a => ReadS [Tropical e a]
    readList :: ReadS [Tropical e a]
    $creadPrec :: forall (e :: Extrema) a. Read a => ReadPrec (Tropical e a)
    readPrec :: ReadPrec (Tropical e a)
    $creadListPrec :: forall (e :: Extrema) a. Read a => ReadPrec [Tropical e a]
    readListPrec :: ReadPrec [Tropical e a]
    Read
        , Typeable
        , Typeable (Tropical e a)
    Typeable (Tropical e a) =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> Tropical e a -> c (Tropical e a))
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c (Tropical e a))
    -> (Tropical e a -> Constr)
    -> (Tropical e a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c (Tropical e a)))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c (Tropical e a)))
    -> ((forall b. Data b => b -> b) -> Tropical e a -> Tropical e a)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> Tropical e a -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> Tropical e a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Tropical e a -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> Tropical e a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Tropical e a -> m (Tropical e a))
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Tropical e a -> m (Tropical e a))
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Tropical e a -> m (Tropical e a))
    -> Data (Tropical e a)
    Tropical e a -> Constr
    Tropical e a -> DataType
    (forall b. Data b => b -> b) -> Tropical e a -> Tropical e a
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Tropical e a -> u
    forall u. (forall d. Data d => d -> u) -> Tropical e a -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Tropical e a -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Tropical e a -> r
    forall (e :: Extrema) a.
    (Typeable e, Data a) =>
    Typeable (Tropical e a)
    forall (e :: Extrema) a.
    (Typeable e, Data a) =>
    Tropical e a -> Constr
    forall (e :: Extrema) a.
    (Typeable e, Data a) =>
    Tropical e a -> DataType
    forall (e :: Extrema) a.
    (Typeable e, Data a) =>
    (forall b. Data b => b -> b) -> Tropical e a -> Tropical e a
    forall (e :: Extrema) a u.
    (Typeable e, Data a) =>
    Int -> (forall d. Data d => d -> u) -> Tropical e a -> u
    forall (e :: Extrema) a u.
    (Typeable e, Data a) =>
    (forall d. Data d => d -> u) -> Tropical e a -> [u]
    forall (e :: Extrema) a r r'.
    (Typeable e, Data a) =>
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Tropical e a -> r
    forall (e :: Extrema) a r r'.
    (Typeable e, Data a) =>
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Tropical e a -> r
    forall (e :: Extrema) a (m :: * -> *).
    (Typeable e, Data a, Monad m) =>
    (forall d. Data d => d -> m d) -> Tropical e a -> m (Tropical e a)
    forall (e :: Extrema) a (m :: * -> *).
    (Typeable e, Data a, MonadPlus m) =>
    (forall d. Data d => d -> m d) -> Tropical e a -> m (Tropical e a)
    forall (e :: Extrema) a (c :: * -> *).
    (Typeable e, Data a) =>
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Tropical e a)
    forall (e :: Extrema) a (c :: * -> *).
    (Typeable e, Data a) =>
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Tropical e a -> c (Tropical e a)
    forall (e :: Extrema) a (t :: * -> *) (c :: * -> *).
    (Typeable e, Data a, Typeable t) =>
    (forall d. Data d => c (t d)) -> Maybe (c (Tropical e a))
    forall (e :: Extrema) a (t :: * -> * -> *) (c :: * -> *).
    (Typeable e, Data a, Typeable t) =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Tropical e a))
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Tropical e a -> m (Tropical e a)
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Tropical e a -> m (Tropical e a)
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Tropical e a)
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Tropical e a -> c (Tropical e a)
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Tropical e a))
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Tropical e a))
    $cgfoldl :: forall (e :: Extrema) a (c :: * -> *).
    (Typeable e, Data a) =>
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Tropical e a -> c (Tropical e a)
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Tropical e a -> c (Tropical e a)
    $cgunfold :: forall (e :: Extrema) a (c :: * -> *).
    (Typeable e, Data a) =>
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Tropical e a)
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Tropical e a)
    $ctoConstr :: forall (e :: Extrema) a.
    (Typeable e, Data a) =>
    Tropical e a -> Constr
    toConstr :: Tropical e a -> Constr
    $cdataTypeOf :: forall (e :: Extrema) a.
    (Typeable e, Data a) =>
    Tropical e a -> DataType
    dataTypeOf :: Tropical e a -> DataType
    $cdataCast1 :: forall (e :: Extrema) a (t :: * -> *) (c :: * -> *).
    (Typeable e, Data a, Typeable t) =>
    (forall d. Data d => c (t d)) -> Maybe (c (Tropical e a))
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Tropical e a))
    $cdataCast2 :: forall (e :: Extrema) a (t :: * -> * -> *) (c :: * -> *).
    (Typeable e, Data a, Typeable t) =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Tropical e a))
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Tropical e a))
    $cgmapT :: forall (e :: Extrema) a.
    (Typeable e, Data a) =>
    (forall b. Data b => b -> b) -> Tropical e a -> Tropical e a
    gmapT :: (forall b. Data b => b -> b) -> Tropical e a -> Tropical e a
    $cgmapQl :: forall (e :: Extrema) a r r'.
    (Typeable e, Data a) =>
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Tropical e a -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Tropical e a -> r
    $cgmapQr :: forall (e :: Extrema) a r r'.
    (Typeable e, Data a) =>
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Tropical e a -> r
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Tropical e a -> r
    $cgmapQ :: forall (e :: Extrema) a u.
    (Typeable e, Data a) =>
    (forall d. Data d => d -> u) -> Tropical e a -> [u]
    gmapQ :: forall u. (forall d. Data d => d -> u) -> Tropical e a -> [u]
    $cgmapQi :: forall (e :: Extrema) a u.
    (Typeable e, Data a) =>
    Int -> (forall d. Data d => d -> u) -> Tropical e a -> u
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Tropical e a -> u
    $cgmapM :: forall (e :: Extrema) a (m :: * -> *).
    (Typeable e, Data a, Monad m) =>
    (forall d. Data d => d -> m d) -> Tropical e a -> m (Tropical e a)
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Tropical e a -> m (Tropical e a)
    $cgmapMp :: forall (e :: Extrema) a (m :: * -> *).
    (Typeable e, Data a, MonadPlus m) =>
    (forall d. Data d => d -> m d) -> Tropical e a -> m (Tropical e a)
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Tropical e a -> m (Tropical e a)
    $cgmapMo :: forall (e :: Extrema) a (m :: * -> *).
    (Typeable e, Data a, MonadPlus m) =>
    (forall d. Data d => d -> m d) -> Tropical e a -> m (Tropical e a)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Tropical e a -> m (Tropical e a)
    Data
        )

    instance forall e a. (Ord a, Extremum e) => Ord (Tropical e a) where
      compare :: Tropical e a -> Tropical e a -> Ordering
    compare Tropical e a
    Infinity Tropical e a
    Infinity         = Ordering
    EQ
      compare Tropical e a
    Infinity Tropical e a
    _                = case EProxy e -> Extrema
    forall (e :: Extrema). Extremum e => EProxy e -> Extrema
    extremum (EProxy e
    forall (e :: Extrema). EProxy e
    EProxy :: EProxy e) of
        Extrema
    Minima -> Ordering
    GT
        Extrema
    Maxima -> Ordering
    LT
      compare Tropical e a
    _ Tropical e a
    Infinity                = case EProxy e -> Extrema
    forall (e :: Extrema). Extremum e => EProxy e -> Extrema
    extremum (EProxy e
    forall (e :: Extrema). EProxy e
    EProxy :: EProxy e) of
        Extrema
    Minima -> Ordering
    LT
        Extrema
    Maxima -> Ordering
    GT
      compare (Tropical a
    x) (Tropical a
    y) = a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare a
    x a
    y

    instance forall e a. (Ord a, Monoid.Monoid a, Extremum e) => Semiring (Tropical e a) where
      zero :: Tropical e a
    zero = Tropical e a
    forall (e :: Extrema) a. Tropical e a
    Infinity
      one :: Tropical e a
    one  = a -> Tropical e a
    forall (e :: Extrema) a. a -> Tropical e a
    Tropical a
    forall a. Monoid a => a
    Monoid.mempty
      plus :: Tropical e a -> Tropical e a -> Tropical e a
    plus Tropical e a
    Infinity Tropical e a
    y = Tropical e a
    y
      plus Tropical e a
    x Tropical e a
    Infinity = Tropical e a
    x
      plus (Tropical a
    x) (Tropical a
    y) = a -> Tropical e a
    forall (e :: Extrema) a. a -> Tropical e a
    Tropical
        ( case EProxy e -> Extrema
    forall (e :: Extrema). Extremum e => EProxy e -> Extrema
    extremum (EProxy e
    forall (e :: Extrema). EProxy e
    EProxy :: EProxy e) of
            Extrema
    Minima -> a -> a -> a
    forall a. Ord a => a -> a -> a
    min a
    x a
    y
            Extrema
    Maxima -> a -> a -> a
    forall a. Ord a => a -> a -> a
    max a
    x a
    y
        )
      times :: Tropical e a -> Tropical e a -> Tropical e a
    times Tropical e a
    Infinity Tropical e a
    _ = Tropical e a
    forall (e :: Extrema) a. Tropical e a
    Infinity
      times Tropical e a
    _ Tropical e a
    Infinity = Tropical e a
    forall (e :: Extrema) a. Tropical e a
    Infinity
      times (Tropical a
    x) (Tropical a
    y) = a -> Tropical e a
    forall (e :: Extrema) a. a -> Tropical e a
    Tropical (a -> a -> a
    forall a. Monoid a => a -> a -> a
    Monoid.mappend a
    x a
    y)
      fromNatural :: Natural -> Tropical e a
    fromNatural Natural
    0 = Tropical e a
    forall a. Semiring a => a
    zero
      fromNatural Natural
    _ = Tropical e a
    forall a. Semiring a => a
    one

    instance forall e a. (Ord a, Monoid.Monoid a, Extremum e) => Star (Tropical e a) where
      star :: Tropical e a -> Tropical e a
    star Tropical e a
    _ = Tropical e a
    forall a. Semiring a => a
    one