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).
--
-- == Type Hierarchy
--
-- === Data Types
--
-- @
-- 'BinaryFunctionT' f a b        -- a -> a -> f b
--   |
--   +-- 'BinaryFunction' a b     -- a -> a -> b          (f ~ 'Data.Functor.Identity.Identity')
--   |     |
--   |     +-- 'Magma' a          -- a -> a -> a          (a ~ b)
--   |
--   +-- 'MagmaT' f a             -- a -> a -> f a        (a ~ b)
--
-- 'Semigroup' a                   -- a -> a -> a
--
-- 'PartialOrder' a                -- a -> a -> 'Maybe' 'Ordering'
--
-- 'ProjectValuation' v set var    -- set var -> v -> v
--
-- 'SemiValuationAlgebra' v set var
--   = 'SemiValuationAlgebra'
--       ('Semigroup' v)                   -- how to combine values
--       ('ProjectValuation' v set var)    -- how to project over a domain
--
-- 'ValuationAlgebraOp' set var v      -- set var -> v
--
-- 'ValuationAlgebra' v set var
--   = 'ValuationAlgebra'
--       ('SemiValuationAlgebra' v set var)
--       ('ValuationAlgebraOp' set var v)  -- unit: identity value for a domain
--       ('ValuationAlgebraOp' set var v)  -- zero: annihilating value for a domain
--
-- 'DomainLattice' sg p
--   = 'DomainLattice'
--       ('Semigroup' sg)                  -- join (∨ \/ supremum)
--       ('Semigroup' sg)                  -- meet (∧ \/ infimum)
--       ('PartialOrder' p)               -- partial order
--
-- 'Valuation' set var a
--   = 'Valuation'
--       (set var)                       -- domain
--       a                               -- information
--
-- 'PresheafValuationAlgebra' v set var
--   = 'PresheafValuationAlgebra'
--       ('DomainLattice' (set var) (set var))   -- lattice on domains
--       ('ValuationAlgebra' v set var)          -- the valuation algebra
-- @
--
-- === Relationships
--
-- @
-- 'BinaryFunctionT' ──specialises──> 'Magma' ──iso──> 'Semigroup'
--                                                         |
--                          'ProjectValuation' ────────────+──> 'SemiValuationAlgebra'
--                                                                       |
--                            'ValuationAlgebraOp' ──────────────────────+──> 'ValuationAlgebra'
--                                                                                    |
--         'PartialOrder' ──> 'DomainLattice' ────────────────────────────────────────+──> 'PresheafValuationAlgebra'
-- @
--
-- == Core Concepts
--
-- === BinaryFunctionT
--
-- 'BinaryFunctionT' @f a b@ wraps @a -> a -> f b@ — a binary function from two @a@ values to an effectful @b@. It has instances for 'Data.Profunctor.Profunctor', 'Data.Profunctor.Strong', 'Data.Profunctor.Choice', 'Functor', 'Applicative', 'Monad', and more.
--
-- When @f ~ 'Data.Functor.Identity.Identity'@ and @a ~ b@, this specialises to 'Magma' @a@ — a binary operation on @a@.
--
-- === Semigroup
--
-- A reified semigroup: a @newtype@ over @a -> a -> a@ representing an associative binary operation. Unlike 'Prelude.Semigroup' which is a type class (one instance per type), this is a value — multiple semigroups can exist for the same type.
--
-- 'Semigroup' is isomorphic to 'Magma' (and hence @'BinaryFunctionT' 'Data.Functor.Identity.Identity' a a@) via 'HasBinaryFunctionT' \/ 'AsBinaryFunctionT'.
--
-- @
-- 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' @a@ wraps @a -> a -> 'Maybe' 'Ordering'@ — a partial order comparison. 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'.
--
-- 'PartialOrder' is isomorphic to @'BinaryFunctionT' 'Maybe' a 'Ordering'@ via 'HasBinaryFunctionT' \/ 'AsBinaryFunctionT'.
--
-- === ProjectValuation
--
-- 'ProjectValuation' @v set var@ wraps @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
--
-- Bundles a 'Semigroup' @v@ with a 'ProjectValuation' @v set var@. This provides everything needed to combine valuations: a way to merge information and a way to project information over a domain.
--
-- === ValuationAlgebra
--
-- Extends 'SemiValuationAlgebra' with two additional 'ValuationAlgebraOp' functions:
--
-- * __unit__ (@set var -> v@): produces an identity value for a given domain
-- * __zero__ (@set var -> v@): produces an annihilating value for a given domain
--
-- === DomainLattice
--
-- 'DomainLattice' @sg p@ packages a lattice structure on domains: join (∨) and meet (∧) as 'Semigroup' values, plus a 'PartialOrder'. The type alias @'DomainLattice'' x = 'DomainLattice' x x@ is provided for the common case where the semigroup and partial order operate on the same type.
--
-- 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). A 'PresheafValuationAlgebra' bundles a 'DomainLattice' with a 'ValuationAlgebra', providing the full structure needed for local computation on valuations:
--
-- * '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 a@ provides a lens to a 'Semigroup' @a@ inside any @c@, and 'PresheafValuationAlgebra' has instances for 'HasDomainLattice', 'HasValuationAlgebra', 'HasSemiValuationAlgebra', 'HasSemigroup', and 'HasProjectValuation'.
--
-- == Modules
--
-- * "Data.Valuation" — Re-exports everything
-- * "Data.Valuation.BinaryFunction" — 'BinaryFunctionT' and type aliases
-- * "Data.Valuation.DomainLattice" — Lattice structure on domains (join, meet, partial order)
-- * "Data.Valuation.PartialOrder" — Partial order comparison (@a -> a -> 'Maybe' 'Ordering'@)
-- * "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@)
module Data.Valuation
  ( module V,
  )
where

import Data.Valuation.BinaryFunction as V
import Data.Valuation.DomainLattice as V
import Data.Valuation.PartialOrder 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