{-# 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