Valuation.hs

{-# OPTIONS_GHC -Wall -Werror #-}

-- |
-- A Haskell library providing reified algebraic structures for valuations,
-- based on the valuation algebra framework of Shenoy & Shafer (1990),
-- Kohlas (2003), and Abramsky & Carù (2019).
--
-- All core types are generalised over profunctors (@p@, @q@, @r@, @s@).
-- When these are @(->)@, each type specialises to an ordinary function;
-- primed type aliases (e.g. 'Semigroup'', 'PartialOrder'') provide
-- these specialisations.
--
-- == Type Hierarchy
--
-- === Data Types
--
-- @
-- 'Semigroup' p a                       -- p a (p a a)
-- 'Semigroup'' a                        -- a -> a -> a          (p ~ (->))
--
-- 'PartialOrder' p a                    -- p a (p a ('Maybe' 'Ordering'))
-- 'PartialOrder'' a                     -- a -> a -> 'Maybe' 'Ordering'   (p ~ (->))
--
-- 'Poset' p a                           -- p a (p a 'Bool')
-- 'Poset'' a                            -- a -> a -> 'Bool'              (p ~ (->))
--
-- 'ProjectValuation' p q v set var      -- p (set var) (q v v)
-- 'ProjectValuation'' v set var         -- set var -> v -> v    (p ~ (->), q ~ (->))
--
-- 'ValuationAlgebraOp' p set var v      -- p (set var) v
-- 'ValuationAlgebraOp'' set var v       -- set var -> v         (p ~ (->))
--
-- 'SemiValuationAlgebra' p q r v set var
--   = 'SemiValuationAlgebra'
--       ('Semigroup' p v)                       -- how to combine values
--       ('ProjectValuation' q r v set var)      -- how to project over a domain
--
-- 'ValuationAlgebra' p q r v set var
--   = 'ValuationAlgebra'
--       ('SemiValuationAlgebra' p q r v set var)
--       ('ValuationAlgebraOp' p set var v)      -- unit: identity value for a domain
--       ('ValuationAlgebraOp' p set var v)      -- zero: annihilating value for a domain
--
-- 'DomainLattice' p sg o
--   = 'DomainLattice'
--       ('Semigroup' p sg)                      -- join (∨ \/ supremum)
--       ('Semigroup' p sg)                      -- meet (∧ \/ infimum)
--       ('PartialOrder' p o)                    -- partial order
--
-- 'Valuation' set var a
--   = 'Valuation'
--       (set var)                               -- domain
--       a                                       -- information
--
-- 'Presheaf' cat cat' f                -- forall a b. cat a b -> cat' (f b) (f a)
-- 'Presheaf'' f                        -- forall a b. (a -> b) -> f b -> f a  (cat ~ (->), cat' ~ (->))
--
-- 'CovariantFunctor' cat cat' f        -- forall a b. cat a b -> cat' (f a) (f b)
-- 'CovariantFunctor'' f                -- forall a b. (a -> b) -> f a -> f b  (cat ~ (->), cat' ~ (->))
--
-- 'PresheafValuationAlgebra' p q r s v set var
--   = 'PresheafValuationAlgebra'
--       ('DomainLattice' p (set var) (set var)) -- lattice on domains
--       ('ValuationAlgebra' q r s v set var)    -- the valuation algebra
-- @
--
-- === Relationships
--
-- @
-- 'Semigroup' ──────────────────────────────────────────────────────┐
--                          'ProjectValuation' ────────────+──> 'SemiValuationAlgebra'
--                                                                       |
--                            'ValuationAlgebraOp' ──────────────────────+──> 'ValuationAlgebra'
--                                                                                    |
--         'PartialOrder' ──> 'DomainLattice' ────────────────────────────────────────+──> 'PresheafValuationAlgebra'
--
--         'Poset' ──────── (converts to\/from 'PartialOrder')
-- @
--
-- == Core Concepts
--
-- === Semigroup
--
-- A reified semigroup: 'Semigroup' @p a@ wraps @p a (p a a)@, representing an associative binary operation generalised over a profunctor @p@. When @p ~ (->)@, this specialises to 'Semigroup'' @a@ wrapping @a -> a -> a@. Unlike 'Prelude.Semigroup' which is a type class (one instance per type), this is a value — multiple semigroups can exist for the same type.
--
-- @
-- import qualified "Data.Valuation.Semigroup" as S
--
-- S.'Data.Valuation.Semigroup.sum'      :: 'Num' a => 'Semigroup' a       -- (+)
-- S.'Data.Valuation.Semigroup.product'  :: 'Num' a => 'Semigroup' a       -- (*)
-- S.'Data.Valuation.Semigroup.min'      :: 'Ord' a => 'Semigroup' a
-- S.'Data.Valuation.Semigroup.max'      :: 'Ord' a => 'Semigroup' a
-- S.'Data.Valuation.Semigroup.list'     :: 'Semigroup' [a]              -- (++)
-- S.'Data.Valuation.Semigroup.ordering' :: 'Semigroup' 'Ordering'         -- lexicographic
-- S.'Data.Valuation.Semigroup.first'    :: 'Semigroup' a                -- const
-- S.'Data.Valuation.Semigroup.second'   :: 'Semigroup' a                -- const id
-- @
--
-- Semigroups compose:
--
-- @
-- S.'Data.Valuation.Semigroup.pair'     :: 'Semigroup' a -> 'Semigroup' b -> 'Semigroup' (a, b)
-- S.'Data.Valuation.Semigroup.maybe'    :: 'Semigroup' a -> 'Semigroup' ('Maybe' a)
-- S.'Data.Valuation.Semigroup.function' :: 'Semigroup' b -> 'Semigroup' (a -> b)
-- S.'Data.Valuation.Semigroup.dual'     :: 'Semigroup' a -> 'Semigroup' a     -- flip
-- @
--
-- === PartialOrder
--
-- 'PartialOrder' @p a@ wraps @p a (p a ('Maybe' 'Ordering'))@ — a partial order comparison generalised over a 'Data.Profunctor.Profunctor' @p@. When @p ~ (->)@, this specialises to @a -> a -> 'Maybe' 'Ordering'@ (see 'PartialOrder''). Unlike 'Ord' which is total, this supports incomparable elements via 'Nothing'. It is 'Data.Functor.Contravariant.Contravariant', 'Data.Functor.Contravariant.Divisible.Divisible', 'Data.Functor.Contravariant.Divisible.Decidable', and has a lexicographic 'Semigroup'.
--
-- === Poset
--
-- 'Poset' @p a@ wraps @p a (p a 'Bool')@ — a simplified partial order that only captures the @<=@ relation as a 'Bool', generalised over a 'Data.Profunctor.Profunctor' @p@. When @p ~ (->)@, this specialises to @a -> a -> 'Bool'@ (see 'Poset''). Unlike 'PartialOrder' which distinguishes @LT@, @EQ@, @GT@, and incomparable, 'Poset' only records whether @a <= b@. It is 'Data.Functor.Contravariant.Contravariant', 'Data.Functor.Contravariant.Divisible.Divisible', 'Data.Functor.Contravariant.Divisible.Decidable', and has a conjunction 'Semigroup' (product order). Conversions 'fromPartialOrder' and 'toPartialOrder' bridge between 'Poset'' and 'PartialOrder''.
--
-- === Presheaf
--
-- A reified presheaf: 'Presheaf' @cat f cat'@ wraps @forall a b. cat a b -> cat' (f b) (f a)@, representing a contravariant mapping from a source category @cat@ to a target category @cat'@ acting on a type constructor @f@. When both categories are @(->)@, this specialises to 'Presheaf'' @f@ wrapping @forall a b. (a -> b) -> f b -> f a@, which is exactly 'Data.Functor.Contravariant.contramap'. Unlike 'Data.Functor.Contravariant.Contravariant' which is a type class (one instance per type), this is a value — and it is generalised over the source and target categories. Values are provided for standard types ('Data.Functor.Contravariant.Predicate', 'Data.Functor.Contravariant.Comparison', 'Data.Functor.Contravariant.Equivalence', 'Data.Proxy.Proxy', @'Data.Functor.Const.Const' r@). For a worked example of defining a 'Presheaf' over a finite category, see "Data.Valuation.PresheafExample".
--
-- === CovariantFunctor
--
-- A reified covariant functor: 'CovariantFunctor' @cat cat' f@ wraps @forall a b. cat a b -> cat' (f a) (f b)@, representing a covariant mapping from a source category @cat@ to a target category @cat'@ acting on a type constructor @f@. When both categories are @(->)@, this specialises to 'CovariantFunctor'' @f@ wrapping @forall a b. (a -> b) -> f a -> f b@, which is exactly 'fmap'. Unlike 'Functor' which is a type class (one instance per type), this is a value — and it is generalised over the source and target categories. Values are provided for standard types ('Data.Functor.Identity.Identity', 'Maybe', @[]@, 'Data.Proxy.Proxy', @'Data.Functor.Const.Const' r@).
--
-- === ProjectValuation
--
-- 'ProjectValuation' @p q v set var@ wraps @p (set var) (q v v)@, generalised over profunctors @p@ (outer) and @q@ (inner). When @p ~ (->)@ and @q ~ (->)@, this specialises to 'ProjectValuation'' @v set var@ wrapping @set var -> v -> v@. Given a domain of variables and a current value, it produces a new value. It is 'Data.Functor.Contravariant.Contravariant' in @var@, and has 'Data.Functor.Contravariant.Divisible.Divisible' and 'Data.Functor.Contravariant.Divisible.Decidable' instances for combining projections.
--
-- === Valuation
--
-- 'Valuation' @set var a@ pairs a domain @set var@ with information @a@. It is a 'Functor', 'Applicative', 'Monad', 'Control.Comonad.Comonad', 'Data.Bifunctor.Bifunctor', 'Control.Monad.Writer.Class.MonadWriter', and more in its type parameters.
--
-- === SemiValuationAlgebra
--
-- 'SemiValuationAlgebra' @p q r v set var@ bundles a 'Semigroup' @p v@ with a 'ProjectValuation' @q r v set var@. The three profunctor parameters allow the semigroup (@p@) and the projection (@q@, @r@) to use independent profunctors. This provides everything needed to combine valuations: a way to merge information and a way to project information over a domain.
--
-- === ValuationAlgebra
--
-- 'ValuationAlgebra' @p q r v set var@ extends 'SemiValuationAlgebra' with two additional 'ValuationAlgebraOp' functions:
--
-- * __unit__ ('ValuationAlgebraOp' @p set var v@): produces an identity value for a given domain
-- * __zero__ ('ValuationAlgebraOp' @p set var v@): produces an annihilating value for a given domain
--
-- === DomainLattice
--
-- 'DomainLattice' @p sg o@ packages a lattice structure on domains: join (∨) and meet (∧) as 'Semigroup' @p sg@ values, plus a 'PartialOrder' @p o@. The type aliases @'DomainLattice'' sg o = 'DomainLattice' (->) sg o@ and @'DomainLattice''' x = 'DomainLattice'' x x@ are provided for common cases.
--
-- The canonical instance is 'setDomainLattice' using 'Data.Set.union', 'Data.Set.intersection', and 'Data.Set.isSubsetOf'.
--
-- === PresheafValuationAlgebra
--
-- The presheaf formulation of a valuation algebra, following Shenoy & Shafer (1990), Kohlas (2003), and Abramsky & Carù (2019). 'PresheafValuationAlgebra' @p q r s v set var@ bundles a 'DomainLattice' @p@ with a 'ValuationAlgebra' @q r s@, providing the full structure needed for local computation on valuations. The four profunctor parameters allow the domain lattice (@p@) and the valuation algebra (@q@, @r@, @s@) to use different profunctors.
--
-- * 'marginalise' — the presheaf restriction map: project a valuation to a subdomain
-- * 'combine' — the combination operation: merge two valuations over the joined domain
-- * 'neutralValuation' — identity element for combination on a given domain
-- * 'nullValuation' — annihilating element for combination on a given domain
--
-- The module also provides law-checking functions for the valuation algebra axioms.
--
-- == Combining Valuations
--
-- The library provides three levels of combination, each using more algebraic structure:
--
-- @
-- -- Combine domains and information independently using two Semigroups
-- 'combineVar'
--   :: 'Semigroup'' (set var) -> 'Semigroup'' v
--   -> 'Valuation' set var v -> 'Valuation' set var v
--   -> 'Valuation' set var v
--
-- -- Combine using a 'SemiValuationAlgebra': merge domains, combine information,
-- -- then project through the merged domain
-- 'combineSemiValuation'
--   :: 'Semigroup'' (set var) -> 'SemiValuationAlgebra'' v set var
--   -> 'Valuation' set var v -> 'Valuation' set var v
--   -> 'Valuation' set var v
--
-- -- Combine using a 'ValuationAlgebra': like 'combineSemiValuation', but also
-- -- folds in the unit value for the merged domain
-- 'combineValuation'
--   :: 'Semigroup'' (set var) -> 'ValuationAlgebra'' v set var
--   -> 'Valuation' set var v -> 'Valuation' set var v
--   -> 'Valuation' set var v
-- @
--
-- At the highest level, 'PresheafValuationAlgebra' provides 'combine' which uses the bundled 'DomainLattice' to join domains automatically.
--
-- == Classy Optics
--
-- Every data type provides @Has*@ (classy lens) and @As*@ (classy prism) type classes, allowing generic programming over any type that contains or can be constructed from the given structure. For example, 'HasSemigroup' @c p a@ provides a lens to a 'Semigroup' @p a@ inside any @c@, and 'PresheafValuationAlgebra' has instances for 'HasDomainLattice', 'HasValuationAlgebra', 'HasSemiValuationAlgebra', 'HasSemigroup', and 'HasProjectValuation'.
--
-- == Modules
--
-- * "Data.Valuation" — Re-exports everything
-- * "Data.Valuation.DomainLattice" — Lattice structure on domains (join, meet, partial order)
-- * "Data.Valuation.PartialOrder" — Partial order comparison (@p a (p a ('Maybe' 'Ordering'))@)
-- * "Data.Valuation.Poset" — Simplified partial order (@p a (p a 'Bool')@)
-- * "Data.Valuation.CovariantFunctor" — Reified covariant functor (@forall a b. cat a b -> cat' (f a) (f b)@)
-- * "Data.Valuation.Presheaf" — Reified presheaf (@forall a b. cat a b -> cat' (f b) (f a)@)
-- * "Data.Valuation.PresheafValuationAlgebra" — Presheaf formulation: marginalise, combine, and axiom laws
-- * "Data.Valuation.ProjectValuation" — Domain projection
-- * "Data.Valuation.Semigroup" — Reified semigroups
-- * "Data.Valuation.SemiValuationAlgebra" — Semigroup + projection
-- * "Data.Valuation.Valuation" — Domain-information pairs
-- * "Data.Valuation.ValuationAlgebra" — Full algebra with unit and zero
-- * "Data.Valuation.ValuationAlgebraOp" — Operations on valuation algebras (@set var -> v@)
-- * "Data.Valuation.PresheafExample" — Worked example: a presheaf over a finite category
module Data.Valuation
  ( module V,
  )
where

import Data.Valuation.CovariantFunctor as V
import Data.Valuation.DomainLattice as V
import Data.Valuation.PartialOrder as V
import Data.Valuation.Poset as V
import Data.Valuation.Presheaf as V
import Data.Valuation.PresheafValuationAlgebra as V
import Data.Valuation.ProjectValuation as V
import Data.Valuation.SemiValuationAlgebra as V
import Data.Valuation.Semigroup as V
import Data.Valuation.Valuation as V
import Data.Valuation.ValuationAlgebra as V
import Data.Valuation.ValuationAlgebraOp as V