{-# LANGUAGE Safe #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
module Data.Semigroup.Quantale (
type UnitalQuantale
, Quantale(..)
, (<==), (==>)
) where
import safe Control.Applicative
import safe Data.Connection.Conn
import safe Data.Functor.Contravariant
import safe Data.Monoid
import safe Data.Order
import safe Data.Int
import safe Data.Word
import safe Data.Semigroup
import safe Data.Semigroup.Join
import safe Data.Universe.Class (Finite(..))
import safe Prelude hiding (Eq(..), Ord(..), floor, ceiling, until)
import safe qualified Data.Order.Float as F32
import safe qualified Data.Order.Double as F64
import safe qualified Data.Map as Map
import safe qualified Data.Map.Merge.Lazy as Map
import safe qualified Data.Set as Set
import safe qualified Prelude as P
type UnitalQuantale a = (Monoid a, Quantale a)
class Semigroup a => Quantale a where
residL :: a -> ConnL a a
residL x = ConnL (<>x) (//x)
residR :: a -> ConnR a a
residR x = ConnR (x<>) (x\\)
infixl 5 //
(//) :: a -> a -> a
x // y = lowerL (residL x) y
infixr 5 \\
(\\) :: a -> a -> a
x \\ y = upperR (residR x) y
infixr 1 ==>
(==>) :: (Meet-Quantale) a => a -> a -> a
(==>) x y = getMeet $ Meet x \\ Meet y
infixl 1 <==
(<==) :: (Meet-Quantale) a => a -> a -> a
(<==) x y = getMeet $ Meet x // Meet y
instance (Applicative f, Quantale a) => Quantale (F1 f a) where
F1 x // F1 y = F1 $ (//) <$> x <*> y
(\\) = flip (//)
instance (Applicative f, Applicative g, Quantale a) => Quantale (F2 f g a) where
(//) = liftA2 (//)
(\\) = flip (//)
instance Quantale All where
All x \\ All y = All $ x <= y
(//) = flip (\\)
instance Quantale a => Quantale (r -> a) where
(\\) = flip (//)
(//) = liftA2 (//)
instance (TotalOrder a, Bounded a) => Quantale (Min a) where
x \\ y = if x P.> y then y else mempty
(//) = flip (\\)
deriving via (F1 Meet (Min ())) instance Quantale (Meet ())
deriving via (F1 Meet (Min Word8)) instance Quantale (Meet Word8)
deriving via (F1 Meet (Min Word16)) instance Quantale (Meet Word16)
deriving via (F1 Meet (Min Word32)) instance Quantale (Meet Word32)
deriving via (F1 Meet (Min Word64)) instance Quantale (Meet Word64)
deriving via (F1 Meet (Min Word)) instance Quantale (Meet Word)
deriving via (F1 Meet (Min Int8)) instance Quantale (Meet Int8)
deriving via (F1 Meet (Min Int16)) instance Quantale (Meet Int16)
deriving via (F1 Meet (Min Int32)) instance Quantale (Meet Int32)
deriving via (F1 Meet (Min Int64)) instance Quantale (Meet Int64)
deriving via (F1 Meet (Min Int)) instance Quantale (Meet Int)
deriving via (F2 Meet Down (Join a)) instance Quantale (Join a) => Quantale (Meet (Down a))
deriving via (F2 Join Down (Meet a)) instance Quantale (Meet a) => Quantale (Join (Down a))
deriving via (F1 Meet (r -> Meet a)) instance Quantale (Meet a) => Quantale (Meet (r -> a))
instance Quantale (Meet Bool) where
(\\) = liftA2 (<=)
(//) = flip (\\)
instance Quantale (Meet Ordering) where
(//) = flip (\\)
(\\) = liftA2 impliesOrdering
where
impliesOrdering LT _ = GT
impliesOrdering EQ LT = LT
impliesOrdering EQ _ = GT
impliesOrdering GT x = x
instance UnitalQuantale (Meet a) => Quantale (Meet (Maybe a)) where
(//) = flip (\\)
(\\) = liftA2 impliesMaybe
where
impliesMaybe (Just a) (Just b) = Just (a ==> b)
impliesMaybe Nothing _ = Just top
impliesMaybe _ Nothing = Nothing
instance (Preorder a, UnitalQuantale (Meet a)) => Quantale (Meet (Either a a)) where
(//) = flip (\\)
(\\) = liftA2 impliesEither
where
impliesEither (Left _) (Right _) = Right top
impliesEither (Right _) l@Left{} = l
impliesEither (Right u) (Right u') = Right $ u ==> u'
impliesEither (Left l) (Left l') = case l ==> l' of
ll' | ll' ~~ top -> Right top
| otherwise -> Left ll'
instance Quantale (Meet (Predicate a)) where
(\\) = liftA2 $ \(Predicate f) (Predicate g) -> Predicate $ \a -> f a <= g a
(//) = flip (\\)
instance TotalOrder a => Quantale (Meet (Set.Set a)) where
(\\) = liftA2 (Set.\\)
(//) = flip (\\)
instance (TotalOrder k, Finite k, UnitalQuantale (Meet a)) => Quantale (Meet (Map.Map k a)) where
(\\) = liftA2 impliesMap
where
impliesMap a b = Map.union x y where
x = Map.merge
Map.dropMissing
(Map.mapMissing (\_ _ -> top))
(Map.zipWithMatched (\_ -> (==>)))
a b
y = Map.fromList [(k, top) | k <- universeF, not (Map.member k a), not (Map.member k b) ]