{-# LANGUAGE CPP #-} {-# 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 #if MIN_VERSION_base(4,7,0) import Data.Data (Data) #endif import Data.Semiring (Semiring(..)) import Data.Star (Star(..)) #if MIN_VERSION_base(4,7,0) import Data.Typeable (Typeable) #endif -- 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 /= :: 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 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 showList :: [Tropical e a] -> ShowS $cshowList :: forall (e :: Extrema) a. Show a => [Tropical e a] -> ShowS show :: Tropical e a -> String $cshow :: forall (e :: Extrema) a. Show a => Tropical e a -> String showsPrec :: Int -> Tropical e a -> ShowS $cshowsPrec :: forall (e :: Extrema) a. Show a => Int -> 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] readListPrec :: ReadPrec [Tropical e a] $creadListPrec :: forall (e :: Extrema) a. Read a => ReadPrec [Tropical e a] readPrec :: ReadPrec (Tropical e a) $creadPrec :: forall (e :: Extrema) a. Read a => ReadPrec (Tropical e a) readList :: ReadS [Tropical e a] $creadList :: forall (e :: Extrema) a. Read a => ReadS [Tropical e a] readsPrec :: Int -> ReadS (Tropical e a) $creadsPrec :: forall (e :: Extrema) a. Read a => Int -> ReadS (Tropical e a) Read #if MIN_VERSION_base(4,7,0) , Typeable , Typeable (Tropical e a) DataType Constr 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 -> DataType Tropical e a -> Constr (forall b. Data b => b -> b) -> Tropical e a -> Tropical e 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 b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (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 -> DataType forall (e :: Extrema) a. (Typeable e, Data a) => Tropical e a -> Constr 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)) $cTropical :: Constr $cInfinity :: Constr $tTropical :: DataType gmapMo :: (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) gmapMp :: (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) gmapM :: (forall d. Data d => d -> m d) -> Tropical e a -> m (Tropical e a) $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) gmapQi :: Int -> (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 gmapQ :: (forall d. Data d => d -> u) -> Tropical e a -> [u] $cgmapQ :: forall (e :: Extrema) a u. (Typeable e, Data a) => (forall d. Data d => d -> u) -> Tropical e a -> [u] gmapQr :: (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 gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Tropical e a -> r $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 gmapT :: (forall b. Data b => b -> b) -> Tropical e a -> Tropical e a $cgmapT :: forall (e :: Extrema) a. (Typeable e, Data a) => (forall b. Data b => b -> b) -> Tropical e a -> Tropical e a dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> 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)) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Tropical e a)) $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)) dataTypeOf :: Tropical e a -> DataType $cdataTypeOf :: forall (e :: Extrema) a. (Typeable e, Data a) => Tropical e a -> DataType toConstr :: Tropical e a -> Constr $ctoConstr :: forall (e :: Extrema) a. (Typeable e, Data a) => Tropical e a -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> 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) gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Tropical e a -> 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) $cp1Data :: forall (e :: Extrema) a. (Typeable e, Data a) => Typeable (Tropical e a) Data #endif ) 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