{-# LANGUAGE RebindableSyntax #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | [Quantales](https://en.wikipedia.org/wiki/Quantale)
module NumHask.Algebra.Quantale
  ( Quantale,
    Residuated (..),
    StarAutonomous (..),
  )
where

import Data.Bool (Bool (..))
import Data.Set (Set)
import Data.Set qualified as Set
import NumHask.Algebra.Lattice (CompleteJoinSemiLattice (..))
import NumHask.Algebra.Multiplicative (Multiplicative (..))
import NumHask.Free.Carriers (MinPlus (..), Warshall (..))
import Prelude qualified as P

-- $setup
--
-- >>> :m -Prelude
-- >>> :set -XRebindableSyntax
-- >>> import NumHask.Prelude
-- >>> import NumHask.Free.Carriers

-- | A quantale is a monoid in complete join-semilattices: a complete
-- join-semilattice equipped with an associative multiplication ('*') and unit
-- ('one') that distributes over arbitrary joins.
--
-- > a * joins xs == joins (fmap (a *) xs)
-- > joins xs * a == joins (fmap (* a) xs)
-- > a * bottom == bottom
-- > bottom * a == bottom
class (CompleteJoinSemiLattice a, Multiplicative a) => Quantale a

-- | If a quantale is also a 'NumHask.Algebra.Ring.StarSemiring', then 'star'
-- is the least fixed point, equivalently the join of the geometric series:
--
-- > star a == joins (iterate (a *) one)
--
-- A 'NumHask.Algebra.Ring.KleeneAlgebra' is therefore the fragment of a
-- (commutative) quantale that only needs these iterative joins, while a
-- quantale admits arbitrary joins.

-- | A /residuated/ quantale: a quantale equipped with the left and right
-- residuals of multiplication.
--
-- In any quantale, multiplication by a fixed element preserves joins, so it
-- has both left and right adjoints. These adjoints are the residuals:
--
-- > a * lres a b <= b
-- > lres a b == joins [ x | a * x <= b ]
--
-- > rres a b * a <= b
-- > rres a b == joins [ x | x * a <= b ]
--
-- The order @<=@ is the one induced by the join-semilattice:
-- @x <= y@ iff @x \/ y == y@.
--
-- For commutative quantales the two residuals coincide: @lres = rres@.
class (Quantale a) => Residuated a where
  {-# MINIMAL lres, rres #-}

  -- | Left residual of multiplication: the greatest @x@ with @a * x <= b@.
  lres :: a -> a -> a

  -- | Right residual of multiplication: the greatest @x@ with @x * a <= b@.
  rres :: a -> a -> a

-- | A /star-autonomous/ quantale: a quantale with an involutive,
-- order-reversing linear negation.
--
-- The negation is an anti-automorphism of the underlying quantale:
--
-- > neg (neg a) == a
-- > joinLeq a b == joinLeq (neg b) (neg a)
-- > neg (a * b) == neg b * neg a
--
-- Multiplicative disjunction ('par') and its unit ('bot') are the duals of
-- '(*)' and 'one':
--
-- > par a b == neg (neg a * neg b)
-- > bot == neg one
--
-- This is the missing connective that turns a quantale into a model of
-- classical linear logic.
class (Quantale a) => StarAutonomous a where
  {-# MINIMAL neg #-}

  -- | Linear negation.
  neg :: a -> a

  -- | Multiplicative disjunction (par), dual to multiplication.
  par :: a -> a -> a
  par a
a a
b = a -> a
forall a. StarAutonomous a => a -> a
neg (a -> a
forall a. StarAutonomous a => a -> a
neg a
a a -> a -> a
forall a. Multiplicative a => a -> a -> a
* a -> a
forall a. StarAutonomous a => a -> a
neg a
b)

  -- | Unit of 'par', dual to 'one'.
  bot :: a
  bot = a -> a
forall a. StarAutonomous a => a -> a
neg a
forall a. Multiplicative a => a
one

-- | Boolean quantale: join is disjunction, multiplication is conjunction.
instance Quantale Bool

-- | Boolean implication as the residual of conjunction.
instance Residuated Bool where
  lres :: Bool -> Bool -> Bool
lres Bool
a Bool
b = Bool -> Bool
P.not Bool
a Bool -> Bool -> Bool
P.|| Bool
b
  rres :: Bool -> Bool -> Bool
rres = Bool -> Bool -> Bool
forall a. Residuated a => a -> a -> a
lres

-- | Boolean negation is complement; 'par' is disjunction and 'bot' is 'False'.
instance StarAutonomous Bool where
  neg :: Bool -> Bool
neg = Bool -> Bool
P.not
  par :: Bool -> Bool -> Bool
par = Bool -> Bool -> Bool
(P.||)
  bot :: Bool
bot = Bool
False

-- | Boolean quantale: join is disjunction, multiplication is conjunction.
instance Quantale Warshall

-- | Boolean implication as the residual of conjunction.
--
-- >>> lres (Warshall True) (Warshall False)
-- Warshall False
--
-- >>> lres (Warshall False) (Warshall True)
-- Warshall True
instance Residuated Warshall where
  lres :: Warshall -> Warshall -> Warshall
lres (Warshall Bool
a) (Warshall Bool
b) = Bool -> Warshall
Warshall (Bool -> Bool
P.not Bool
a Bool -> Bool -> Bool
P.|| Bool
b)
  rres :: Warshall -> Warshall -> Warshall
rres = Warshall -> Warshall -> Warshall
forall a. Residuated a => a -> a -> a
lres

-- | Boolean negation as complement; 'par' is disjunction and 'bot' is
-- 'Warshall False'.
instance StarAutonomous Warshall where
  neg :: Warshall -> Warshall
neg (Warshall Bool
a) = Bool -> Warshall
Warshall (Bool -> Bool
P.not Bool
a)
  par :: Warshall -> Warshall -> Warshall
par (Warshall Bool
a) (Warshall Bool
b) = Bool -> Warshall
Warshall (Bool
a Bool -> Bool -> Bool
P.|| Bool
b)
  bot :: Warshall
bot = Bool -> Warshall
Warshall Bool
P.False

-- | Tropical (min-plus) quantale: join is minimum, bottom is positive
-- infinity, multiplication is addition.
instance Quantale (MinPlus P.Double)

-- | Tropical residual is truncated subtraction.
--
-- >>> getMinPlus (lres (MinPlus 2) (MinPlus 5) :: MinPlus Double)
-- 3.0
--
-- >>> getMinPlus (lres (MinPlus 5) (MinPlus 2) :: MinPlus Double)
-- -3.0
instance Residuated (MinPlus P.Double) where
  lres :: MinPlus Double -> MinPlus Double -> MinPlus Double
lres (MinPlus Double
a) (MinPlus Double
b) = Double -> MinPlus Double
forall a. a -> MinPlus a
MinPlus (Double
b Double -> Double -> Double
forall a. Num a => a -> a -> a
P.- Double
a)
  rres :: MinPlus Double -> MinPlus Double -> MinPlus Double
rres = MinPlus Double -> MinPlus Double -> MinPlus Double
forall a. Residuated a => a -> a -> a
lres

-- | Tropical linear negation is additive inverse; 'par' is addition and
-- 'bot' is the multiplicative unit @0@.
instance StarAutonomous (MinPlus P.Double) where
  neg :: MinPlus Double -> MinPlus Double
neg (MinPlus Double
a) = Double -> MinPlus Double
forall a. a -> MinPlus a
MinPlus (Double -> Double
forall a. Num a => a -> a
P.negate Double
a)
  par :: MinPlus Double -> MinPlus Double -> MinPlus Double
par (MinPlus Double
a) (MinPlus Double
b) = Double -> MinPlus Double
forall a. a -> MinPlus a
MinPlus (Double
a Double -> Double -> Double
forall a. Num a => a -> a -> a
P.+ Double
b)
  bot :: MinPlus Double
bot = MinPlus Double -> MinPlus Double
forall a. StarAutonomous a => a -> a
neg MinPlus Double
forall a. Multiplicative a => a
one

-- | Power-set quantale of a monoid: join is union, bottom is the empty set,
-- multiplication is pointwise product of subsets, and the unit is the
-- singleton set containing 'one'.
--
-- This is the language quantale when the underlying monoid is the free monoid
-- over an alphabet.
instance (P.Ord a, Multiplicative a) => Multiplicative (Set a) where
  one :: Set a
one = a -> Set a
forall a. a -> Set a
Set.singleton a
forall a. Multiplicative a => a
one
  Set a
s * :: Set a -> Set a -> Set a
* Set a
t = [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList [a
x a -> a -> a
forall a. Multiplicative a => a -> a -> a
* a
y | a
x <- Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
s, a
y <- Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
t]

instance (P.Ord a, Multiplicative a) => Quantale (Set a)