diff --git a/changelog.md b/changelog.md --- a/changelog.md +++ b/changelog.md @@ -1,3 +1,16 @@ +0.0.4 + +* Generalise data types over the Profunctor and not (->) +* Add `CovariantFunctor` module — reified covariant functor, dual of `Presheaf` +* Add composition functions for `Presheaf` and `CovariantFunctor`: + - `composePresheafFunctor` (contravariant ∘ covariant = contravariant) + - `composeFunctorPresheaf` (covariant ∘ contravariant = contravariant) + - `composePresheaf` (contravariant ∘ contravariant = covariant) + - `composeFunctor` (covariant ∘ covariant = covariant) +* Add law-checking functions for `Presheaf` (identity, composition) +* Add law-checking functions for `CovariantFunctor` (identity, composition) +* Update documentation and doctests + 0.0.3 * Generalise data types over the Profunctor and not (->) diff --git a/src/Data/Valuation.hs b/src/Data/Valuation.hs --- a/src/Data/Valuation.hs +++ b/src/Data/Valuation.hs @@ -5,80 +5,83 @@ -- 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 -- -- @ --- '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' p a -- p a (p a a) +-- 'Semigroup'' a -- a -> a -> a (p ~ (->)) -- --- 'Semigroup' a -- a -> a -> a +-- 'PartialOrder' p a -- p a (p a ('Maybe' 'Ordering')) +-- 'PartialOrder'' a -- a -> a -> 'Maybe' 'Ordering' (p ~ (->)) -- --- 'PartialOrder' a -- a -> a -> 'Maybe' 'Ordering' +-- 'Poset' p a -- p a (p a 'Bool') +-- 'Poset'' a -- a -> a -> 'Bool' (p ~ (->)) -- --- 'ProjectValuation' v set var -- set var -> v -> v +-- 'ProjectValuation' p q v set var -- p (set var) (q v v) +-- 'ProjectValuation'' v set var -- set var -> v -> v (p ~ (->), q ~ (->)) -- --- 'SemiValuationAlgebra' v set var --- = 'SemiValuationAlgebra' --- ('Semigroup' v) -- how to combine values --- ('ProjectValuation' v set var) -- how to project over a domain +-- 'ValuationAlgebraOp' p set var v -- p (set var) v +-- 'ValuationAlgebraOp'' set var v -- set var -> v (p ~ (->)) -- --- 'ValuationAlgebraOp' set var v -- set var -> v +-- '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' v set var +-- 'ValuationAlgebra' p q r 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 +-- ('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' sg p +-- 'DomainLattice' p sg o -- = 'DomainLattice' --- ('Semigroup' sg) -- join (∨ \/ supremum) --- ('Semigroup' sg) -- meet (∧ \/ infimum) --- ('PartialOrder' p) -- partial order +-- ('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 +-- (set var) -- domain +-- a -- information -- --- 'PresheafValuationAlgebra' v set var +-- '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' (set var) (set var)) -- lattice on domains --- ('ValuationAlgebra' v set var) -- the valuation algebra +-- ('DomainLattice' p (set var) (set var)) -- lattice on domains +-- ('ValuationAlgebra' q r s v set var) -- the valuation algebra -- @ -- -- === Relationships -- -- @ --- 'BinaryFunctionT' ──specialises──> 'Magma' ──iso──> 'Semigroup' --- | +-- 'Semigroup' ──────────────────────────────────────────────────────┐ -- 'ProjectValuation' ────────────+──> 'SemiValuationAlgebra' -- | -- 'ValuationAlgebraOp' ──────────────────────+──> 'ValuationAlgebra' -- | -- 'PartialOrder' ──> 'DomainLattice' ────────────────────────────────────────+──> 'PresheafValuationAlgebra' +-- +-- 'Poset' ──────── (converts to\/from 'PartialOrder') -- @ -- -- == 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'. +-- 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 @@ -104,13 +107,23 @@ -- -- === 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' @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'. -- --- 'PartialOrder' is isomorphic to @'BinaryFunctionT' 'Maybe' a 'Ordering'@ via 'HasBinaryFunctionT' \/ 'AsBinaryFunctionT'. +-- === 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@). +-- +-- === 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' @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. +-- '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 -- @@ -118,24 +131,24 @@ -- -- === 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. +-- '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 -- --- Extends 'SemiValuationAlgebra' with two additional 'ValuationAlgebraOp' functions: +-- 'ValuationAlgebra' @p q r v set var@ 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 +-- * __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' @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. +-- '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). A 'PresheafValuationAlgebra' bundles a 'DomainLattice' with a 'ValuationAlgebra', providing the full structure needed for local computation on valuations: +-- 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 @@ -151,21 +164,21 @@ -- @ -- -- Combine domains and information independently using two Semigroups -- 'combineVar' --- :: 'Semigroup' (set var) -> 'Semigroup' v +-- :: '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 +-- :: '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 +-- :: 'Semigroup'' (set var) -> 'ValuationAlgebra'' v set var -- -> 'Valuation' set var v -> 'Valuation' set var v -- -> 'Valuation' set var v -- @ @@ -174,14 +187,16 @@ -- -- == 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'. +-- 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.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.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 @@ -194,9 +209,11 @@ ) where -import Data.Valuation.BinaryFunction as V +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 diff --git a/src/Data/Valuation/BinaryFunction.hs b/src/Data/Valuation/BinaryFunction.hs deleted file mode 100644 --- a/src/Data/Valuation/BinaryFunction.hs +++ /dev/null @@ -1,335 +0,0 @@ -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE FunctionalDependencies #-} -{-# LANGUAGE TupleSections #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -{-# OPTIONS_GHC -Wall -Werror #-} - --- | Binary functions over a functor, generalising magmas and semigroups. -module Data.Valuation.BinaryFunction - ( BinaryFunctionT (..), - BinaryFunction, - MagmaT, - Magma, - - -- * optics - HasBinaryFunctionT (..), - AsBinaryFunctionT (..), - - -- * combinators - binaryFunction, - semigroupBinaryFunctionT, - ) -where - -import Control.Applicative (Alternative (..)) -import Control.Lens - ( Iso, - Lens', - Prism', - Rewrapped, - Wrapped (..), - from, - iso, - over, - review, - view, - _Wrapped, - ) -import Control.Monad.Fix (MonadFix (..)) -import Control.Monad.IO.Class (MonadIO (..)) -import Control.Monad.Zip (MonadZip (..)) -import Control.Selective (Selective (..), selectM) -import Data.Distributive (Distributive (..)) -import Data.Functor.Alt (Alt (..)) -import Data.Functor.Apply (Apply (..)) -import Data.Functor.Bind (Bind (..)) -import Data.Functor.Identity (Identity (..)) -import Data.Functor.Plus (Plus (..)) -import Data.Profunctor (Choice (..), Profunctor (..), Strong (..)) -import Data.Profunctor.Closed (Closed (..)) -import Data.Valuation.Semigroup - ( Semigroup', - applySemigroup, - runSemigroup, - ) -import Prelude hiding (Semigroup) -import qualified Prelude - --- $setup --- >>> :set -Wno-name-shadowing -Wno-type-defaults - --- | --- >>> let BinaryFunctionT f = BinaryFunctionT (\x y -> [x + y]) :: BinaryFunctionT [] Int Int --- >>> f 3 5 --- [8] --- --- >>> let BinaryFunctionT f = BinaryFunctionT (\x y -> Just (x ++ y)) :: BinaryFunctionT Maybe String String --- >>> f "hello" " world" --- Just "hello world" -newtype BinaryFunctionT f a b - = BinaryFunctionT (a -> a -> f b) - -instance - (BinaryFunctionT f a b ~ t) => - Rewrapped (BinaryFunctionT f' a' b') t - -instance Wrapped (BinaryFunctionT f a b) where - type Unwrapped (BinaryFunctionT f a b) = a -> a -> f b - _Wrapped' = - iso (\(BinaryFunctionT x) -> x) BinaryFunctionT - --- | A 'BinaryFunctionT' specialised to 'Identity'. -type BinaryFunction a b = - BinaryFunctionT Identity a b - --- | A 'BinaryFunctionT' where the input and output types coincide. -type MagmaT f x = - BinaryFunctionT f x x - --- | A 'BinaryFunction' where the input and output types coincide. -type Magma x = - BinaryFunction x x - --- | Classy lens for types that contain a 'BinaryFunctionT'. -class HasBinaryFunctionT c f a b | c -> f a b where - binaryFunctionT :: - Lens' c (BinaryFunctionT f a b) - -instance HasBinaryFunctionT (BinaryFunctionT f a b) f a b where - binaryFunctionT = id - --- | Classy prism for types that can be constructed from a 'BinaryFunctionT'. -class AsBinaryFunctionT c f a b | c -> f a b where - _BinaryFunctionT :: - Prism' c (BinaryFunctionT f a b) - -instance AsBinaryFunctionT (BinaryFunctionT f a b) f a b where - _BinaryFunctionT = id - -instance HasBinaryFunctionT (Semigroup' a) Identity a a where - binaryFunctionT = applySemigroup . from binaryFunction - -instance AsBinaryFunctionT (Semigroup' a) Identity a a where - _BinaryFunctionT = applySemigroup . from binaryFunction - --- | Iso between a 'BinaryFunction' and its underlying binary function. -binaryFunction :: Iso (BinaryFunction a b) (BinaryFunction a' b') (a -> a -> b) (a' -> a' -> b') -binaryFunction = _Wrapped . iso (\k a1 a2 -> runIdentity (k a1 a2)) (\k a1 a2 -> Identity (k a1 a2)) - --- | --- >>> let BinaryFunctionT f = fmap (*2) (BinaryFunctionT (\x y -> [x + y]) :: BinaryFunctionT [] Int Int) --- >>> f 3 5 --- [16] --- --- >>> let BinaryFunctionT f = fmap show (BinaryFunctionT (\x y -> Just (x + y)) :: BinaryFunctionT Maybe Int Int) --- >>> f 3 5 --- Just "8" -instance (Functor f) => Functor (BinaryFunctionT f a) where - fmap g = over _Wrapped (\h a1 a2 -> fmap g (h a1 a2)) - --- | --- >>> import Data.Functor.Apply ((<.>)) --- >>> let BinaryFunctionT f = (BinaryFunctionT (\x y -> [(*x), (*y)]) :: BinaryFunctionT [] Int (Int -> Int)) <.> BinaryFunctionT (\x y -> [x + y, x * y]) --- >>> f 3 5 --- [24,45,40,75] -apBFT :: (f (b -> c) -> f b -> f c) -> BinaryFunctionT f a (b -> c) -> BinaryFunctionT f a b -> BinaryFunctionT f a c -apBFT ap' (BinaryFunctionT hf) (BinaryFunctionT ha) = BinaryFunctionT (\a1 a2 -> ap' (hf a1 a2) (ha a1 a2)) - -instance (Apply f) => Apply (BinaryFunctionT f a) where - (<.>) = apBFT (<.>) - --- | --- >>> let BinaryFunctionT f = pure 42 :: BinaryFunctionT [] Int Int --- >>> f 1 2 --- [42] --- --- >>> let BinaryFunctionT f = (BinaryFunctionT (\x y -> [(*x), (*y)]) :: BinaryFunctionT [] Int (Int -> Int)) <*> BinaryFunctionT (\x y -> [x + y, x * y]) --- >>> f 3 5 --- [24,45,40,75] -instance (Applicative f) => Applicative (BinaryFunctionT f a) where - pure b = BinaryFunctionT (\_ _ -> pure b) - (<*>) = apBFT (<*>) - --- | --- >>> import Data.Functor.Bind ((>>-)) --- >>> let BinaryFunctionT f = BinaryFunctionT (\x y -> [x + y, x * y]) >>- (\b -> BinaryFunctionT (\x y -> [b + x, b + y])) :: BinaryFunctionT [] Int Int --- >>> f 3 5 --- [11,13,18,20] -bindBFT :: (f b -> (b -> f c) -> f c) -> BinaryFunctionT f a b -> (b -> BinaryFunctionT f a c) -> BinaryFunctionT f a c -bindBFT bnd (BinaryFunctionT h) k = BinaryFunctionT (\a1 a2 -> bnd (h a1 a2) (\b -> view _Wrapped (k b) a1 a2)) - -instance (Bind f) => Bind (BinaryFunctionT f a) where - (>>-) = bindBFT (>>-) - --- | --- >>> let BinaryFunctionT f = BinaryFunctionT (\x y -> [x + y, x * y]) >>= (\b -> BinaryFunctionT (\x y -> [b + x, b + y])) :: BinaryFunctionT [] Int Int --- >>> f 3 5 --- [11,13,18,20] --- --- >>> let BinaryFunctionT f = return 42 :: BinaryFunctionT [] Int Int --- >>> f 1 2 --- [42] -instance (Monad f) => Monad (BinaryFunctionT f a) where - (>>=) = bindBFT (>>=) - --- | --- >>> import Data.Profunctor (dimap, lmap, rmap) --- >>> let BinaryFunctionT f = dimap (+1) (*2) (BinaryFunctionT (\x y -> [x + y]) :: BinaryFunctionT [] Int Int) --- >>> f 3 5 --- [20] --- --- >>> import Data.Profunctor (lmap) --- >>> let BinaryFunctionT f = lmap (*10) (BinaryFunctionT (\x y -> [x, y]) :: BinaryFunctionT [] Int Int) --- >>> f 3 5 --- [30,50] --- --- >>> import Data.Profunctor (rmap) --- >>> let BinaryFunctionT f = rmap show (BinaryFunctionT (\x y -> [x + y]) :: BinaryFunctionT [] Int Int) --- >>> f 3 5 --- ["8"] -instance (Functor f) => Profunctor (BinaryFunctionT f) where - dimap f g = over _Wrapped (\h a1 a2 -> fmap g (h (f a1) (f a2))) - lmap f = over _Wrapped (\h a1 a2 -> h (f a1) (f a2)) - rmap g = over _Wrapped (\h a1 a2 -> fmap g (h a1 a2)) - --- | --- >>> import Data.Profunctor (Strong(..)) --- >>> let BinaryFunctionT f = first' (BinaryFunctionT (\x y -> [x + y]) :: BinaryFunctionT [] Int Int) --- >>> f (1, "hello") (2, "world") --- [(3,"hello")] --- --- >>> import Data.Profunctor (Strong(..)) --- >>> let BinaryFunctionT f = second' (BinaryFunctionT (\x y -> [x + y]) :: BinaryFunctionT [] Int Int) --- >>> f ("hello", 1) ("world", 2) --- [("hello",3)] -instance (Functor f) => Strong (BinaryFunctionT f) where - first' = over _Wrapped (\h (a1, c) (a2, _) -> fmap (,c) (h a1 a2)) - second' = over _Wrapped (\h (c, a1) (_, a2) -> fmap (c,) (h a1 a2)) - --- | --- >>> import Data.Profunctor (Choice(..)) --- >>> let BinaryFunctionT f = left' (BinaryFunctionT (\x y -> [x + y]) :: BinaryFunctionT [] Int Int) --- >>> f (Left 1) (Left 2) --- [Left 3] --- >>> f (Left 1) (Right "hi") --- [Right "hi"] --- >>> f (Right "hi") (Left 2) --- [Right "hi"] --- >>> f (Right "a") (Right "b") --- [Right "a"] --- --- >>> import Data.Profunctor (Choice(..)) --- >>> let BinaryFunctionT f = right' (BinaryFunctionT (\x y -> [x + y]) :: BinaryFunctionT [] Int Int) --- >>> f (Right 1) (Right 2) --- [Right 3] --- >>> f (Left "hi") (Right 2) --- [Left "hi"] -instance (Applicative f) => Choice (BinaryFunctionT f) where - left' = over _Wrapped $ \h ea1 ea2 -> case (ea1, ea2) of - (Left a1, Left a2) -> fmap Left (h a1 a2) - (Right c, _) -> pure (Right c) - (_, Right c) -> pure (Right c) - right' = over _Wrapped $ \h ea1 ea2 -> case (ea1, ea2) of - (Right a1, Right a2) -> fmap Right (h a1 a2) - (Left c, _) -> pure (Left c) - (_, Left c) -> pure (Left c) - --- | --- >>> import Control.Monad.Fix (mfix) --- >>> let BinaryFunctionT f = mfix (\x -> BinaryFunctionT (\a _ -> [const 42 x + a])) :: BinaryFunctionT [] Int Int --- >>> f 1 2 --- [43] -instance (MonadFix f) => MonadFix (BinaryFunctionT f a) where - mfix g = BinaryFunctionT (\a1 a2 -> mfix (\b -> view _Wrapped (g b) a1 a2)) - --- | --- >>> import Control.Selective (select) --- >>> let BinaryFunctionT f = select (BinaryFunctionT (\_ _ -> [Left 1, Right 2]) :: BinaryFunctionT [] Int (Either Int Int)) (BinaryFunctionT (\_ _ -> [(+10)])) --- >>> f 0 0 --- [11,2] -instance (Monad f) => Selective (BinaryFunctionT f a) where - select = selectM - --- | --- >>> import Control.Monad.Zip (mzip) --- >>> let BinaryFunctionT f = mzip (BinaryFunctionT (\x y -> [x + y, x * y]) :: BinaryFunctionT [] Int Int) (BinaryFunctionT (\x y -> [x - y])) --- >>> f 5 3 --- [(8,2)] -instance (MonadZip f) => MonadZip (BinaryFunctionT f a) where - mzipWith g (BinaryFunctionT h1) (BinaryFunctionT h2) = BinaryFunctionT (\a1 a2 -> mzipWith g (h1 a1 a2) (h2 a1 a2)) - --- | --- >>> let BinaryFunctionT f = liftIO (putStrLn "hello") :: BinaryFunctionT IO Int () --- >>> f 1 2 --- hello -instance (MonadIO f) => MonadIO (BinaryFunctionT f a) where - liftIO io = BinaryFunctionT (\_ _ -> liftIO io) - --- | --- >>> import Data.Functor.Alt (()) --- >>> let BinaryFunctionT f = (BinaryFunctionT (\_ _ -> Nothing) :: BinaryFunctionT Maybe Int Int) BinaryFunctionT (\x y -> Just (x + y)) --- >>> f 3 5 --- Just 8 -instance (Alt f) => Alt (BinaryFunctionT f a) where - BinaryFunctionT h1 BinaryFunctionT h2 = BinaryFunctionT (\a1 a2 -> h1 a1 a2 h2 a1 a2) - --- | --- >>> import Data.Functor.Plus (zero) --- >>> let BinaryFunctionT f = zero :: BinaryFunctionT [] Int Int --- >>> f 1 2 --- [] -instance (Plus f) => Plus (BinaryFunctionT f a) where - zero = BinaryFunctionT (\_ _ -> zero) - --- | --- >>> import Control.Applicative (empty, (<|>)) --- >>> let BinaryFunctionT f = (BinaryFunctionT (\_ _ -> Nothing) :: BinaryFunctionT Maybe Int Int) <|> BinaryFunctionT (\x y -> Just (x + y)) --- >>> f 3 5 --- Just 8 --- --- >>> import Control.Applicative (empty) --- >>> let BinaryFunctionT f = empty :: BinaryFunctionT [] Int Int --- >>> f 1 2 --- [] -instance (Alternative f) => Alternative (BinaryFunctionT f a) where - empty = BinaryFunctionT (\_ _ -> empty) - BinaryFunctionT h1 <|> BinaryFunctionT h2 = BinaryFunctionT (\a1 a2 -> h1 a1 a2 <|> h2 a1 a2) - --- | --- >>> let BinaryFunctionT f = runSemigroup semigroupBinaryFunctionT (BinaryFunctionT (\_ _ -> [1, 2]) :: BinaryFunctionT [] Int Int) (BinaryFunctionT (\_ _ -> [10, 20])) in f 0 0 --- [1,2,10,20] -semigroupBinaryFunctionT :: (Prelude.Semigroup (f b)) => Semigroup' (BinaryFunctionT f a b) -semigroupBinaryFunctionT = review applySemigroup (\(BinaryFunctionT h1) (BinaryFunctionT h2) -> BinaryFunctionT (\a1 a2 -> h1 a1 a2 <> h2 a1 a2)) - --- | --- >>> let BinaryFunctionT f = BinaryFunctionT (\_ _ -> [1, 2]) <> (BinaryFunctionT (\_ _ -> [3, 4]) :: BinaryFunctionT [] Int Int) --- >>> f 0 0 --- [1,2,3,4] -instance (Prelude.Semigroup (f b)) => Prelude.Semigroup (BinaryFunctionT f a b) where - (<>) = runSemigroup semigroupBinaryFunctionT - --- | --- >>> let BinaryFunctionT f = mempty :: BinaryFunctionT [] Int Int --- >>> f 1 2 --- [] -instance (Prelude.Monoid (f b)) => Prelude.Monoid (BinaryFunctionT f a b) where - mempty = BinaryFunctionT (\_ _ -> mempty) - --- | --- >>> import Data.Distributive (distribute) --- >>> import Data.Functor.Identity (Identity(..)) --- >>> let BinaryFunctionT f = distribute [BinaryFunctionT (\x y -> Identity (x + y)), BinaryFunctionT (\x y -> Identity (x * y))] :: BinaryFunctionT Identity Int [Int] --- >>> f 3 5 --- Identity [8,15] -instance (Distributive f) => Distributive (BinaryFunctionT f a) where - distribute gs = BinaryFunctionT (\a1 a2 -> distribute (fmap (\(BinaryFunctionT h) -> h a1 a2) gs)) - --- | --- >>> import Data.Profunctor.Closed (Closed(..)) --- >>> import Data.Functor.Identity (Identity(..)) --- >>> let BinaryFunctionT f = closed (BinaryFunctionT (\x y -> Identity (x + y)) :: BinaryFunctionT Identity Int Int) --- >>> runIdentity (f (*2) (*3)) 10 --- 50 -instance (Distributive f) => Closed (BinaryFunctionT f) where - closed (BinaryFunctionT h) = BinaryFunctionT (\xa1 xa2 -> distribute (\x -> h (xa1 x) (xa2 x))) diff --git a/src/Data/Valuation/CovariantFunctor.hs b/src/Data/Valuation/CovariantFunctor.hs new file mode 100644 --- /dev/null +++ b/src/Data/Valuation/CovariantFunctor.hs @@ -0,0 +1,212 @@ +{-# LANGUAGE RankNTypes #-} +{-# OPTIONS_GHC -Wall -Werror #-} + +-- | A reified covariant functor: a covariant mapping from one category to another, +-- wrapping @forall a b. cat a b -> cat' (f a) (f b)@. +-- +-- 'CovariantFunctor' @cat cat' f@ reifies the action of a covariant functor on +-- a type constructor @f@, generalised over a source category @cat@ and a +-- target category @cat'@. When both 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. +-- +-- @ +-- newtype 'CovariantFunctor' cat cat' f = 'CovariantFunctor' (forall a b. cat a b -> cat' (f a) (f b)) +-- type 'CovariantFunctor'' f = 'CovariantFunctor' (->) (->) f +-- @ +module Data.Valuation.CovariantFunctor + ( CovariantFunctor (..), + CovariantFunctor', + + -- * combinators + runCovariantFunctor, + composeFunctor, + fmapCovariantFunctor, + + -- * covariant functor values + identityCovariantFunctor, + maybeCovariantFunctor, + listCovariantFunctor, + proxyCovariantFunctor, + constCovariantFunctor, + + -- * laws + lawCovariantFunctorIdentity, + lawCovariantFunctorComposition, + ) +where + +import Data.Functor.Compose (Compose (..)) +import Data.Functor.Const (Const (..)) +import Data.Functor.Identity (Identity (..)) +import Data.Profunctor (Profunctor (dimap)) +import Data.Proxy (Proxy) + +-- $setup +-- >>> :set -Wno-name-shadowing -Wno-type-defaults +-- >>> import Data.Functor.Const (Const(..)) +-- >>> import Data.Functor.Identity (Identity(..)) +-- >>> import Data.Proxy (Proxy(..)) + +-- | +-- >>> runCovariantFunctor listCovariantFunctor (+1) [1,2,3] +-- [2,3,4] +-- +-- >>> runCovariantFunctor maybeCovariantFunctor (*2) (Just 5) +-- Just 10 +newtype CovariantFunctor cat cat' f = CovariantFunctor (forall a b. cat a b -> cat' (f a) (f b)) + +-- | A 'CovariantFunctor' specialised to @(->)@ for both categories. +-- Wraps @forall a b. (a -> b) -> f a -> f b@, equivalent to 'fmap'. +type CovariantFunctor' f = CovariantFunctor (->) (->) f + +-- | Unwrap a 'CovariantFunctor' to its underlying natural transformation. +-- +-- >>> runCovariantFunctor identityCovariantFunctor (+1) (Identity 3) +-- Identity 4 +-- +-- >>> runCovariantFunctor maybeCovariantFunctor show (Just 42) +-- Just "42" +-- >>> runCovariantFunctor maybeCovariantFunctor show Nothing +-- Nothing +-- +-- >>> runCovariantFunctor listCovariantFunctor (*2) [1,2,3] +-- [2,4,6] +-- >>> runCovariantFunctor listCovariantFunctor (*2) [] +-- [] +runCovariantFunctor :: CovariantFunctor cat cat' f -> cat a b -> cat' (f a) (f b) +runCovariantFunctor (CovariantFunctor f) = f + +-- | Compose two covariant functors. +-- The result is covariant (covariant ∘ covariant = covariant). +-- +-- Given @f@ covariant from @cat@ to @cat'@ and @g@ covariant from @cat'@ to @cat''@, +-- @g ∘ f@ is covariant from @cat@ to @cat''@ acting on @'Compose' g f@. +-- +-- >>> import Data.Functor.Compose (Compose(..)) +-- >>> let p = composeFunctor maybeCovariantFunctor listCovariantFunctor +-- >>> runCovariantFunctor p (+1) (Compose [Just 1, Nothing, Just 3]) +-- Compose [Just 2,Nothing,Just 4] +-- +-- >>> import Data.Functor.Compose (Compose(..)) +-- >>> let p = composeFunctor listCovariantFunctor maybeCovariantFunctor +-- >>> runCovariantFunctor p (+1) (Compose (Just [1,2,3])) +-- Compose (Just [2,3,4]) +-- >>> runCovariantFunctor p (+1) (Compose Nothing :: Compose Maybe [] Int) +-- Compose Nothing +composeFunctor :: + (Profunctor cat'') => + CovariantFunctor cat cat' f -> + CovariantFunctor cat' cat'' g -> + CovariantFunctor cat cat'' (Compose g f) +composeFunctor (CovariantFunctor f) (CovariantFunctor g) = + CovariantFunctor (dimap getCompose Compose . g . f) + +-- | The canonical 'CovariantFunctor'' for any 'Functor', +-- using 'fmap'. +-- +-- >>> runCovariantFunctor fmapCovariantFunctor (+1) [1,2,3] +-- [2,3,4] +-- >>> runCovariantFunctor fmapCovariantFunctor not (Just True) +-- Just False +fmapCovariantFunctor :: (Functor f) => CovariantFunctor' f +fmapCovariantFunctor = CovariantFunctor fmap + +-- | 'CovariantFunctor'' on 'Identity': maps the wrapped value. +-- +-- >>> runCovariantFunctor identityCovariantFunctor (+1) (Identity 3) +-- Identity 4 +-- >>> runCovariantFunctor identityCovariantFunctor show (Identity 42) +-- Identity "42" +identityCovariantFunctor :: CovariantFunctor' Identity +identityCovariantFunctor = CovariantFunctor fmap + +-- | 'CovariantFunctor'' on 'Maybe': maps over the contained value if present. +-- +-- >>> runCovariantFunctor maybeCovariantFunctor (+1) (Just 3) +-- Just 4 +-- >>> runCovariantFunctor maybeCovariantFunctor (+1) Nothing +-- Nothing +-- +-- >>> runCovariantFunctor maybeCovariantFunctor show (Just 42) +-- Just "42" +maybeCovariantFunctor :: CovariantFunctor' Maybe +maybeCovariantFunctor = CovariantFunctor fmap + +-- | 'CovariantFunctor'' on @[]@: maps over each element. +-- +-- >>> runCovariantFunctor listCovariantFunctor (+1) [1,2,3] +-- [2,3,4] +-- >>> runCovariantFunctor listCovariantFunctor (*2) [] +-- [] +-- +-- >>> runCovariantFunctor listCovariantFunctor show [1,2,3] +-- ["1","2","3"] +listCovariantFunctor :: CovariantFunctor' [] +listCovariantFunctor = CovariantFunctor fmap + +-- | 'CovariantFunctor'' on 'Proxy': trivially maps the phantom type parameter. +-- +-- >>> runCovariantFunctor proxyCovariantFunctor not (Proxy :: Proxy Bool) +-- Proxy +-- +-- >>> runCovariantFunctor proxyCovariantFunctor show (Proxy :: Proxy Int) +-- Proxy +proxyCovariantFunctor :: CovariantFunctor' Proxy +proxyCovariantFunctor = CovariantFunctor fmap + +-- | 'CovariantFunctor'' on @'Const' r@: trivially maps the phantom second parameter. +-- The constant value is preserved. +-- +-- >>> runCovariantFunctor constCovariantFunctor not (Const 42 :: Const Int Bool) +-- Const 42 +-- +-- >>> runCovariantFunctor constCovariantFunctor show (Const "hello" :: Const String Int) +-- Const "hello" +constCovariantFunctor :: CovariantFunctor' (Const r) +constCovariantFunctor = CovariantFunctor fmap + +-- | The identity law for a 'CovariantFunctor'': mapping the identity morphism +-- must be the identity on @f a@. +-- +-- @ +-- 'runCovariantFunctor' p 'id' x == x +-- @ +-- +-- >>> lawCovariantFunctorIdentity identityCovariantFunctor (Identity 42) +-- True +-- >>> lawCovariantFunctorIdentity maybeCovariantFunctor (Just 42 :: Maybe Int) +-- True +-- >>> lawCovariantFunctorIdentity listCovariantFunctor [1,2,3 :: Int] +-- True +-- >>> lawCovariantFunctorIdentity proxyCovariantFunctor (Proxy :: Proxy Int) +-- True +-- >>> lawCovariantFunctorIdentity constCovariantFunctor (Const 42 :: Const Int Bool) +-- True +lawCovariantFunctorIdentity :: (Eq (f a)) => CovariantFunctor' f -> f a -> Bool +lawCovariantFunctorIdentity p x = + runCovariantFunctor p id x == x + +-- | The composition law for a 'CovariantFunctor'': mapping a composition must +-- equal composing the individual mappings. +-- +-- @ +-- 'runCovariantFunctor' p (g '.' f) x == 'runCovariantFunctor' p g ('runCovariantFunctor' p f x) +-- @ +-- +-- >>> lawCovariantFunctorComposition identityCovariantFunctor (+1) (*2) (Identity 3) +-- True +-- >>> lawCovariantFunctorComposition maybeCovariantFunctor (+1) (*2) (Just 3 :: Maybe Int) +-- True +-- >>> lawCovariantFunctorComposition listCovariantFunctor (+1) (*2) [1,2,3 :: Int] +-- True +-- >>> lawCovariantFunctorComposition proxyCovariantFunctor not (&&True) (Proxy :: Proxy Bool) +-- True +-- >>> lawCovariantFunctorComposition constCovariantFunctor (+1) (*2) (Const "hello" :: Const String Int) +-- True +lawCovariantFunctorComposition :: (Eq (f c)) => CovariantFunctor' f -> (b -> c) -> (a -> b) -> f a -> Bool +lawCovariantFunctorComposition p g f x = + runCovariantFunctor p (g . f) x == runCovariantFunctor p g (runCovariantFunctor p f x) diff --git a/src/Data/Valuation/DomainLattice.hs b/src/Data/Valuation/DomainLattice.hs --- a/src/Data/Valuation/DomainLattice.hs +++ b/src/Data/Valuation/DomainLattice.hs @@ -14,6 +14,7 @@ module Data.Valuation.DomainLattice ( DomainLattice (..), DomainLattice', + DomainLattice'', HasDomainLattice (..), AsDomainLattice (..), runDomainJoin, @@ -75,11 +76,14 @@ -- | meet (/\ / infimum) (Semigroup p sg) -- | partial order - (PartialOrder o) + (PartialOrder p o) -type DomainLattice' x = - DomainLattice (->) x x +type DomainLattice' sg o = + DomainLattice (->) sg o +type DomainLattice'' x = + DomainLattice' x x + -- | Classy lens for types that contain a 'DomainLattice'. class HasDomainLattice c p sg o | c -> p sg o where domainLattice :: Lens' c (DomainLattice p sg o) @@ -100,7 +104,7 @@ instance AsDomainLattice (DomainLattice p sg o) p sg o where _DomainLattice = id -instance HasPartialOrder (DomainLattice p sg o) o where +instance HasPartialOrder (DomainLattice p sg o) p o where partialOrder f (DomainLattice j m o) = fmap (DomainLattice j m) (f o) -- | Apply the domain join (\/): the supremum of two domains. @@ -128,9 +132,9 @@ -- >>> runDomainCompare (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3]) -- Nothing {-# SPECIALIZE runDomainCompare :: - DomainLattice p sg o -> o -> o -> Maybe Ordering + DomainLattice (->) sg o -> o -> o -> Maybe Ordering #-} -runDomainCompare :: (HasPartialOrder lat p) => lat -> p -> p -> Maybe Ordering +runDomainCompare :: (HasPartialOrder lat (->) o) => lat -> o -> o -> Maybe Ordering runDomainCompare = runPartialOrder . view partialOrder -- | Test the domain partial order: @runDomainLeq lat d1 d2@ is 'True' iff @d1 <= d2@. @@ -142,9 +146,9 @@ -- >>> runDomainLeq (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3]) -- False {-# SPECIALIZE runDomainLeq :: - DomainLattice p sg o -> o -> o -> Bool + DomainLattice (->) sg o -> o -> o -> Bool #-} -runDomainLeq :: (HasPartialOrder lat p) => lat -> p -> p -> Bool +runDomainLeq :: (HasPartialOrder lat (->) o) => lat -> o -> o -> Bool runDomainLeq = partialOrderLeq . view partialOrder -- | The canonical 'DomainLattice' for 'Set', with union as join, @@ -160,7 +164,7 @@ -- True -- >>> runDomainCompare lat (Set.fromList ["x","y"]) (Set.fromList ["y","z"]) -- Nothing -setDomainLattice :: (Ord a) => DomainLattice' (Set a) +setDomainLattice :: (Ord a) => DomainLattice'' (Set a) setDomainLattice = DomainLattice (review applySemigroup Set.union) @@ -171,7 +175,7 @@ -- >>> import qualified Data.Set as Set -- >>> lawJoinAssociative (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3]) (Set.fromList [3,4]) -- True -lawJoinAssociative :: (Eq sg) => DomainLattice (->) sg o -> sg -> sg -> sg -> Bool +lawJoinAssociative :: (Eq sg) => DomainLattice' sg o -> sg -> sg -> sg -> Bool lawJoinAssociative lat a b c = let j = runDomainJoin lat in j (j a b) c == j a (j b c) @@ -180,7 +184,7 @@ -- >>> import qualified Data.Set as Set -- >>> lawMeetAssociative (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3]) (Set.fromList [3,4]) -- True -lawMeetAssociative :: (Eq sg) => DomainLattice (->) sg o -> sg -> sg -> sg -> Bool +lawMeetAssociative :: (Eq sg) => DomainLattice' sg o -> sg -> sg -> sg -> Bool lawMeetAssociative lat a b c = let m = runDomainMeet lat in m (m a b) c == m a (m b c) @@ -244,6 +248,6 @@ -- True -- >>> lawLeqFromJoin (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1,3]) (Set.fromList [1,2]) -- True -lawLeqFromJoin :: (Eq d) => DomainLattice' d -> d -> d -> Bool +lawLeqFromJoin :: (Eq d) => DomainLattice'' d -> d -> d -> Bool lawLeqFromJoin lat a b = runDomainLeq lat a b == (runDomainJoin lat a b == b) diff --git a/src/Data/Valuation/PartialOrder.hs b/src/Data/Valuation/PartialOrder.hs --- a/src/Data/Valuation/PartialOrder.hs +++ b/src/Data/Valuation/PartialOrder.hs @@ -1,10 +1,15 @@ +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wall -Werror #-} --- | A partial order on a type, wrapping @a -> a -> 'Maybe' 'Ordering'@. +-- | A partial order on a type, generalised over a 'Profunctor' @p@, +-- wrapping @p a (p a ('Maybe' 'Ordering'))@. +-- When @p ~ (->)@, this specialises to @a -> a -> 'Maybe' 'Ordering'@ +-- (see 'PartialOrder''). -- -- This is the partial order analogue of 'Data.Functor.Contravariant.Comparison' -- (which represents total orders via @a -> a -> 'Ordering'@). @@ -18,42 +23,44 @@ -- @ module Data.Valuation.PartialOrder ( PartialOrder (..), + PartialOrder', -- * optics HasPartialOrder (..), AsPartialOrder (..), - isBinaryFunctionT, -- * combinators semigroupPartialOrder, runPartialOrder, partialOrderLeq, totalOrder, + comparisonTotalOrder, + fromEquivalence, fromLeq, ) where import Control.Lens - ( Iso, - Lens', + ( Lens', Prism', Rewrapped, Wrapped (..), - from, iso, review, - _Wrapped, ) -import Data.Functor.Contravariant (Contravariant (..)) +import Data.Functor.Apply (Apply, liftF2) +import Data.Functor.Contravariant + ( Comparison (Comparison), + Contravariant (contramap), + Equivalence (Equivalence), + ) import Data.Functor.Contravariant.Conclude (Conclude (..)) import Data.Functor.Contravariant.Decide (Decide (..)) import Data.Functor.Contravariant.Divise (Divise (..)) import Data.Functor.Contravariant.Divisible (Decidable (..), Divisible (..)) -import Data.Valuation.BinaryFunction - ( AsBinaryFunctionT (..), - BinaryFunctionT, - HasBinaryFunctionT (..), - ) +import Data.Profunctor (Profunctor (..)) +import qualified Data.Profunctor.Rep as Pro +import Data.Profunctor.Sieve (Sieve (..)) import Data.Valuation.Semigroup ( Semigroup', applySemigroup, @@ -68,74 +75,69 @@ -- >>> import Data.Void (Void) -- | --- >>> runPartialOrder (totalOrder :: PartialOrder Int) 1 2 +-- >>> runPartialOrder (totalOrder :: PartialOrder' Int) 1 2 -- Just LT --- >>> runPartialOrder (totalOrder :: PartialOrder Int) 2 2 +-- >>> runPartialOrder (totalOrder :: PartialOrder' Int) 2 2 -- Just EQ --- >>> runPartialOrder (totalOrder :: PartialOrder Int) 3 2 +-- >>> runPartialOrder (totalOrder :: PartialOrder' Int) 3 2 -- Just GT -- -- >>> import qualified Data.Set as Set -- >>> runPartialOrder (fromLeq Set.isSubsetOf) (Set.fromList [1,2]) (Set.fromList [2,3 :: Int]) -- Nothing -newtype PartialOrder a - = PartialOrder (a -> a -> Maybe Ordering) +newtype PartialOrder p a + = PartialOrder (p a (p a (Maybe Ordering))) -instance (PartialOrder a ~ t) => Rewrapped (PartialOrder a') t +type PartialOrder' a = + PartialOrder (->) a -instance Wrapped (PartialOrder a) where - type Unwrapped (PartialOrder a) = a -> a -> Maybe Ordering +instance (PartialOrder' a ~ t) => Rewrapped (PartialOrder' a') t + +instance Wrapped (PartialOrder' a) where + type Unwrapped (PartialOrder' a) = a -> a -> Maybe Ordering _Wrapped' = iso (\(PartialOrder x) -> x) PartialOrder -- | Classy lens for types that contain a 'PartialOrder'. -class HasPartialOrder c a | c -> a where - partialOrder :: Lens' c (PartialOrder a) +class HasPartialOrder c p a | c -> p a where + partialOrder :: Lens' c (PartialOrder p a) -instance HasPartialOrder (PartialOrder a) a where +instance HasPartialOrder (PartialOrder p a) p a where partialOrder = id -- | Classy prism for types that can be constructed from a 'PartialOrder'. -class AsPartialOrder c a | c -> a where - _PartialOrder :: Prism' c (PartialOrder a) +class AsPartialOrder c p a | c -> p a where + _PartialOrder :: Prism' c (PartialOrder p a) -instance AsPartialOrder (PartialOrder a) a where +instance AsPartialOrder (PartialOrder p a) p a where _PartialOrder = id -instance HasBinaryFunctionT (PartialOrder a) Maybe a Ordering where - binaryFunctionT = isBinaryFunctionT - -instance AsBinaryFunctionT (PartialOrder a) Maybe a Ordering where - _BinaryFunctionT = isBinaryFunctionT - -isBinaryFunctionT :: Iso (PartialOrder a) (PartialOrder a') (BinaryFunctionT Maybe a Ordering) (BinaryFunctionT Maybe a' Ordering) -isBinaryFunctionT = _Wrapped . from _Wrapped - --- | Apply the partial order comparison. +-- | Unwrap the partial order to its underlying profunctor value. +-- For @p ~ (->)@, this gives @a -> a -> 'Maybe' 'Ordering'@. -- --- >>> runPartialOrder (totalOrder :: PartialOrder Int) 1 2 +-- >>> runPartialOrder (totalOrder :: PartialOrder' Int) 1 2 -- Just LT --- >>> runPartialOrder (totalOrder :: PartialOrder Int) 2 2 +-- >>> runPartialOrder (totalOrder :: PartialOrder' Int) 2 2 -- Just EQ --- >>> runPartialOrder (totalOrder :: PartialOrder Int) 3 2 +-- >>> runPartialOrder (totalOrder :: PartialOrder' Int) 3 2 -- Just GT -runPartialOrder :: PartialOrder a -> a -> a -> Maybe Ordering +runPartialOrder :: PartialOrder p a -> p a (p a (Maybe Ordering)) runPartialOrder (PartialOrder f) = f -- | Test whether @a <= b@ in the partial order. -- Returns 'True' iff the comparison yields 'Just' 'LT' or 'Just' 'EQ'. -- Returns 'False' for incomparable elements. -- --- >>> partialOrderLeq (totalOrder :: PartialOrder Int) 1 2 +-- >>> partialOrderLeq (totalOrder :: PartialOrder' Int) 1 2 -- True --- >>> partialOrderLeq (totalOrder :: PartialOrder Int) 2 2 +-- >>> partialOrderLeq (totalOrder :: PartialOrder' Int) 2 2 -- True --- >>> partialOrderLeq (totalOrder :: PartialOrder Int) 3 2 +-- >>> partialOrderLeq (totalOrder :: PartialOrder' Int) 3 2 -- False -- -- >>> import qualified Data.Set as Set -- >>> partialOrderLeq (fromLeq Set.isSubsetOf) (Set.fromList [1,2]) (Set.fromList [2,3 :: Int]) -- False -partialOrderLeq :: PartialOrder a -> a -> a -> Bool +partialOrderLeq :: PartialOrder' a -> a -> a -> Bool partialOrderLeq po a b = case runPartialOrder po a b of Just LT -> True Just EQ -> True @@ -144,15 +146,42 @@ -- | Construct a 'PartialOrder' from a total order ('Ord' instance). -- The result never yields 'Nothing' since all elements are comparable. -- --- >>> runPartialOrder (totalOrder :: PartialOrder Int) 1 2 +-- >>> runPartialOrder (totalOrder :: PartialOrder' Int) 1 2 -- Just LT --- >>> runPartialOrder (totalOrder :: PartialOrder Int) 2 2 +-- >>> runPartialOrder (totalOrder :: PartialOrder' Int) 2 2 -- Just EQ --- >>> runPartialOrder (totalOrder :: PartialOrder Int) 3 2 +-- >>> runPartialOrder (totalOrder :: PartialOrder' Int) 3 2 -- Just GT -totalOrder :: (Ord a) => PartialOrder a +totalOrder :: (Ord a) => PartialOrder' a totalOrder = PartialOrder (\a b -> Just (compare a b)) +-- | Lift a 'Comparison' (a reified total order) into a 'PartialOrder''. +-- Since a total order has no incomparable elements, the result +-- always yields @'Just' o@ for some 'Ordering' @o@, never 'Nothing'. +-- +-- >>> import Data.Functor.Contravariant (Comparison(..)) +-- >>> runPartialOrder (comparisonTotalOrder (Comparison compare)) (1 :: Int) 2 +-- Just LT +-- >>> runPartialOrder (comparisonTotalOrder (Comparison compare)) (2 :: Int) 2 +-- Just EQ +-- >>> runPartialOrder (comparisonTotalOrder (Comparison compare)) (3 :: Int) 2 +-- Just GT +-- +-- >>> import Data.Functor.Contravariant (Comparison(..), contramap) +-- >>> runPartialOrder (comparisonTotalOrder (contramap negate (Comparison compare))) (1 :: Int) 2 +-- Just GT +-- +-- >>> import Data.Functor.Contravariant (Comparison(..)) +-- >>> partialOrderLeq (comparisonTotalOrder (Comparison compare)) (1 :: Int) 2 +-- True +-- >>> partialOrderLeq (comparisonTotalOrder (Comparison compare)) (2 :: Int) 1 +-- False +comparisonTotalOrder :: Comparison a -> PartialOrder' a +comparisonTotalOrder (Comparison cmp) = PartialOrder (\a1 a2 -> Just (cmp a1 a2)) + +fromEquivalence :: (Bool -> Maybe Ordering) -> Equivalence a -> PartialOrder' a +fromEquivalence k (Equivalence p) = PartialOrder (\a1 a2 -> k (p a1 a2)) + -- | Construct a 'PartialOrder' from a less-than-or-equal predicate. -- -- The predicate should satisfy the partial order laws @@ -160,7 +189,7 @@ -- Elements where neither @leq a b@ nor @leq b a@ holds are incomparable ('Nothing'). -- -- >>> import qualified Data.Set as Set --- >>> let po = fromLeq Set.isSubsetOf :: PartialOrder (Set.Set Int) +-- >>> let po = fromLeq Set.isSubsetOf :: PartialOrder' (Set.Set Int) -- >>> runPartialOrder po (Set.fromList [1]) (Set.fromList [1,2]) -- Just LT -- >>> runPartialOrder po (Set.fromList [1,2]) (Set.fromList [1,2]) @@ -169,7 +198,7 @@ -- Just GT -- >>> runPartialOrder po (Set.fromList [1,2]) (Set.fromList [2,3]) -- Nothing -fromLeq :: (a -> a -> Bool) -> PartialOrder a +fromLeq :: (a -> a -> Bool) -> PartialOrder' a fromLeq leq = PartialOrder $ \a b -> case (leq a b, leq b a) of (True, True) -> Just EQ @@ -179,51 +208,56 @@ -- | -- >>> import Data.Functor.Contravariant (contramap) --- >>> runPartialOrder (contramap negate (totalOrder :: PartialOrder Int)) 1 2 +-- >>> runPartialOrder (contramap negate (totalOrder :: PartialOrder' Int)) 1 2 -- Just GT --- >>> runPartialOrder (contramap negate (totalOrder :: PartialOrder Int)) 2 1 +-- >>> runPartialOrder (contramap negate (totalOrder :: PartialOrder' Int)) 2 1 -- Just LT -instance Contravariant PartialOrder where - contramap f (PartialOrder g) = PartialOrder (\a b -> g (f a) (f b)) +instance (Profunctor p) => Contravariant (PartialOrder p) where + contramap f (PartialOrder g) = PartialOrder (dimap f (lmap f) g) -- | Lexicographic composition as a first-class 'Semigroup': compare by the -- first partial order; if equal ('Just' 'EQ'), compare by the second. -- If the first yields 'Nothing' (incomparable), the result is 'Nothing'. -- --- >>> let po = totalOrder :: PartialOrder Int +-- >>> let po = totalOrder :: PartialOrder' Int -- >>> runPartialOrder (runSemigroup semigroupPartialOrder po po) 1 2 -- Just LT -- >>> runPartialOrder (runSemigroup semigroupPartialOrder po po) 2 2 -- Just EQ -semigroupPartialOrder :: Semigroup' (PartialOrder a) -semigroupPartialOrder = review applySemigroup $ \(PartialOrder f) (PartialOrder g) -> PartialOrder $ \a b -> - case f a b of - Just EQ -> g a b - r -> r +semigroupPartialOrder :: (Pro.Representable p, Apply (Pro.Rep p)) => Semigroup' (PartialOrder p a) +semigroupPartialOrder = review applySemigroup $ \(PartialOrder pf) (PartialOrder pg) -> + PartialOrder $ Pro.tabulate $ \a -> + liftF2 + ( \innerF innerG -> Pro.tabulate $ \b -> + liftF2 (\r1 r2 -> case r1 of Just EQ -> r2; _ -> r1) (sieve innerF b) (sieve innerG b) + ) + (sieve pf a) + (sieve pg a) +{-# SPECIALIZE semigroupPartialOrder :: Semigroup' (PartialOrder' a) #-} -- | --- >>> let po = totalOrder :: PartialOrder Int +-- >>> let po = totalOrder :: PartialOrder' Int -- >>> runPartialOrder (po <> po) 1 2 -- Just LT -- >>> runPartialOrder (po <> po) 2 2 -- Just EQ -instance Prelude.Semigroup (PartialOrder a) where +instance (Pro.Representable p, Apply (Pro.Rep p)) => Prelude.Semigroup (PartialOrder p a) where (<>) = runSemigroup semigroupPartialOrder -- | The trivial partial order where all elements are equal. -- --- >>> runPartialOrder (mempty :: PartialOrder Int) 1 2 +-- >>> runPartialOrder (mempty :: PartialOrder' Int) 1 2 -- Just EQ --- >>> runPartialOrder (mempty :: PartialOrder Int) 42 99 +-- >>> runPartialOrder (mempty :: PartialOrder' Int) 42 99 -- Just EQ -instance Monoid (PartialOrder a) where - mempty = PartialOrder (\_ _ -> Just EQ) +instance (Pro.Representable p, Apply (Pro.Rep p), Applicative (Pro.Rep p)) => Monoid (PartialOrder p a) where + mempty = PartialOrder (Pro.tabulate (\_ -> pure (Pro.tabulate (\_ -> pure (Just EQ))))) -- | Lexicographic product: split @a@ into @(b, c)@, compare by @b@ first, -- if equal then compare by @c@. @conquer@ treats all elements as equal. -- -- >>> import Data.Functor.Contravariant.Divisible (divide, conquer) --- >>> let po = divide id (totalOrder :: PartialOrder Int) (totalOrder :: PartialOrder Int) +-- >>> let po = divide id (totalOrder :: PartialOrder' Int) (totalOrder :: PartialOrder' Int) -- >>> runPartialOrder po (1, 2) (1, 3) -- Just LT -- >>> runPartialOrder po (1, 2) (2, 1) @@ -232,9 +266,9 @@ -- Just EQ -- -- >>> import Data.Functor.Contravariant.Divisible (conquer) --- >>> runPartialOrder (conquer :: PartialOrder Int) 1 2 +-- >>> runPartialOrder (conquer :: PartialOrder' Int) 1 2 -- Just EQ -instance Divisible PartialOrder where +instance (Pro.Representable p, Apply (Pro.Rep p), Applicative (Pro.Rep p)) => Divisible (PartialOrder p) where conquer = mempty divide f pb pc = contramap (fst . f) pb <> contramap (snd . f) pc @@ -244,7 +278,7 @@ -- -- >>> import Data.Functor.Contravariant.Divisible (choose, lose) -- >>> import Data.Void (Void, absurd) --- >>> let po = choose id (totalOrder :: PartialOrder Int) (totalOrder :: PartialOrder String) +-- >>> let po = choose id (totalOrder :: PartialOrder' Int) (totalOrder :: PartialOrder' String) -- >>> runPartialOrder po (Left 1) (Left 2) -- Just LT -- >>> runPartialOrder po (Right "a") (Right "b") @@ -256,42 +290,43 @@ -- -- >>> import Data.Functor.Contravariant.Divisible (lose) -- >>> import Data.Void (Void, absurd) --- >>> let po = lose absurd :: PartialOrder Void +-- >>> let po = lose absurd :: PartialOrder' Void -- >>> seq po () -- () -instance Decidable PartialOrder where - lose f = PartialOrder (\a _ -> absurd (f a)) - choose f pb pc = PartialOrder $ \a1 a2 -> - case (f a1, f a2) of - (Left b1, Left b2) -> runPartialOrder pb b1 b2 - (Right c1, Right c2) -> runPartialOrder pc c1 c2 - _ -> Nothing +instance (Pro.Representable p, Apply (Pro.Rep p), Monad (Pro.Rep p)) => Decidable (PartialOrder p) where + lose f = PartialOrder (Pro.tabulate (absurd . f)) + choose f pb pc = PartialOrder $ Pro.tabulate $ \a1 -> + pure $ Pro.tabulate $ \a2 -> + case (f a1, f a2) of + (Left b1, Left b2) -> sieve (runPartialOrder pb) b1 >>= \inner -> sieve inner b2 + (Right c1, Right c2) -> sieve (runPartialOrder pc) c1 >>= \inner -> sieve inner c2 + _ -> pure Nothing -- | -- >>> import Data.Functor.Contravariant.Divise (divise) --- >>> let po = divise id (totalOrder :: PartialOrder Int) (totalOrder :: PartialOrder Int) +-- >>> let po = divise id (totalOrder :: PartialOrder' Int) (totalOrder :: PartialOrder' Int) -- >>> runPartialOrder po (1, 2) (1, 3) -- Just LT -- >>> runPartialOrder po (1, 2) (1, 2) -- Just EQ -instance Divise PartialOrder where - divise = divide +instance (Pro.Representable p, Apply (Pro.Rep p)) => Divise (PartialOrder p) where + divise f pb pc = contramap (fst . f) pb <> contramap (snd . f) pc -- | -- >>> import Data.Functor.Contravariant.Decide (decide) --- >>> let po = decide id (totalOrder :: PartialOrder Int) (totalOrder :: PartialOrder String) +-- >>> let po = decide id (totalOrder :: PartialOrder' Int) (totalOrder :: PartialOrder' String) -- >>> runPartialOrder po (Left 1) (Left 2) -- Just LT -- >>> runPartialOrder po (Left 1) (Right "a") -- Nothing -instance Decide PartialOrder where +instance (Pro.Representable p, Apply (Pro.Rep p), Monad (Pro.Rep p)) => Decide (PartialOrder p) where decide = choose -- | -- >>> import Data.Functor.Contravariant.Conclude (conclude) -- >>> import Data.Void (absurd) --- >>> let po = conclude absurd :: PartialOrder Void +-- >>> let po = conclude absurd :: PartialOrder' Void -- >>> seq po () -- () -instance Conclude PartialOrder where +instance (Pro.Representable p, Apply (Pro.Rep p), Monad (Pro.Rep p)) => Conclude (PartialOrder p) where conclude = lose diff --git a/src/Data/Valuation/Poset.hs b/src/Data/Valuation/Poset.hs new file mode 100644 --- /dev/null +++ b/src/Data/Valuation/Poset.hs @@ -0,0 +1,354 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wall -Werror #-} + +-- | A poset (partial order) on a type, generalised over a 'Profunctor' @p@, +-- wrapping @p a (p a 'Bool')@. +-- When @p ~ (->)@, this specialises to @a -> a -> 'Bool'@ +-- (see 'Poset''). +-- +-- This is a simplified alternative to +-- 'Data.Valuation.PartialOrder.PartialOrder' which wraps +-- @p a (p a ('Maybe' 'Ordering'))@. +-- While 'Data.Valuation.PartialOrder.PartialOrder' distinguishes +-- @LT@, @EQ@, @GT@, and incomparable, +-- 'Poset' only captures the @<=@ relation as a 'Bool'. +-- +-- @ +-- 'True' — a <= b +-- 'False' — a is not <= b (either a > b, or a and b are incomparable) +-- @ +module Data.Valuation.Poset + ( Poset (..), + Poset', + + -- * optics + HasPoset (..), + AsPoset (..), + + -- * combinators + semigroupPoset, + runPoset, + totalPoset, + comparisonPoset, + equivalencePoset, + fromPartialOrder, + toPartialOrder, + ) +where + +import Control.Lens + ( Lens', + Prism', + Rewrapped, + Wrapped (..), + iso, + review, + ) +import Data.Functor.Apply (Apply, liftF2) +import Data.Functor.Contravariant + ( Comparison (Comparison), + Contravariant (contramap), + Equivalence (Equivalence), + ) +import Data.Functor.Contravariant.Conclude (Conclude (..)) +import Data.Functor.Contravariant.Decide (Decide (..)) +import Data.Functor.Contravariant.Divise (Divise (..)) +import Data.Functor.Contravariant.Divisible (Decidable (..), Divisible (..)) +import Data.Profunctor (Profunctor (..)) +import qualified Data.Profunctor.Rep as Pro +import Data.Profunctor.Sieve (Sieve (..)) +import Data.Valuation.PartialOrder + ( PartialOrder', + fromLeq, + partialOrderLeq, + ) +import Data.Valuation.Semigroup + ( Semigroup', + applySemigroup, + runSemigroup, + ) +import Data.Void (absurd) +import Prelude hiding (Semigroup) +import qualified Prelude + +-- $setup +-- >>> :set -Wno-name-shadowing -Wno-type-defaults +-- >>> import Data.Void (Void) + +-- | +-- >>> runPoset (totalPoset :: Poset' Int) 1 2 +-- True +-- >>> runPoset (totalPoset :: Poset' Int) 2 2 +-- True +-- >>> runPoset (totalPoset :: Poset' Int) 3 2 +-- False +-- +-- >>> import qualified Data.Set as Set +-- >>> runPoset (Poset Set.isSubsetOf) (Set.fromList [1,2]) (Set.fromList [2,3 :: Int]) +-- False +newtype Poset p a + = Poset (p a (p a Bool)) + +type Poset' a = + Poset (->) a + +instance (Poset' a ~ t) => Rewrapped (Poset' a') t + +instance Wrapped (Poset' a) where + type Unwrapped (Poset' a) = a -> a -> Bool + _Wrapped' = iso (\(Poset x) -> x) Poset + +-- | Classy lens for types that contain a 'Poset'. +class HasPoset c p a | c -> p a where + poset :: Lens' c (Poset p a) + +instance HasPoset (Poset p a) p a where + poset = id + +-- | Classy prism for types that can be constructed from a 'Poset'. +class AsPoset c p a | c -> p a where + _Poset :: Prism' c (Poset p a) + +instance AsPoset (Poset p a) p a where + _Poset = id + +-- | Unwrap the poset to its underlying profunctor value. +-- For @p ~ (->)@, this gives @a -> a -> 'Bool'@. +-- +-- >>> runPoset (totalPoset :: Poset' Int) 1 2 +-- True +-- >>> runPoset (totalPoset :: Poset' Int) 2 2 +-- True +-- >>> runPoset (totalPoset :: Poset' Int) 3 2 +-- False +runPoset :: Poset p a -> p a (p a Bool) +runPoset (Poset f) = f + +-- | Construct a 'Poset' from a total order ('Ord' instance). +-- The result is the standard @<=@ comparison. +-- +-- >>> runPoset (totalPoset :: Poset' Int) 1 2 +-- True +-- >>> runPoset (totalPoset :: Poset' Int) 2 2 +-- True +-- >>> runPoset (totalPoset :: Poset' Int) 3 2 +-- False +totalPoset :: (Ord a) => Poset' a +totalPoset = Poset (<=) + +-- | Lift a 'Comparison' (a reified total order) into a 'Poset''. +-- The result tests @<=@ according to the comparison. +-- +-- >>> import Data.Functor.Contravariant (Comparison(..)) +-- >>> runPoset (comparisonPoset (Comparison compare)) (1 :: Int) 2 +-- True +-- >>> runPoset (comparisonPoset (Comparison compare)) (2 :: Int) 2 +-- True +-- >>> runPoset (comparisonPoset (Comparison compare)) (3 :: Int) 2 +-- False +-- +-- >>> import Data.Functor.Contravariant (Comparison(..), contramap) +-- >>> runPoset (comparisonPoset (contramap negate (Comparison compare))) (1 :: Int) 2 +-- False +comparisonPoset :: Comparison a -> Poset' a +comparisonPoset (Comparison cmp) = Poset (\a1 a2 -> cmp a1 a2 /= GT) + +-- | Lift an 'Equivalence' (a reified equivalence relation) into a 'Poset''. +-- The result is the discrete order: @a <= b@ iff @a@ is equivalent to @b@. +-- +-- >>> import Data.Functor.Contravariant (Equivalence(..), getEquivalence) +-- >>> let eq = Equivalence (\a b -> a `mod` 3 == b `mod` 3) :: Equivalence Int +-- >>> runPoset (equivalencePoset eq) 1 4 +-- True +-- >>> runPoset (equivalencePoset eq) 1 2 +-- False +equivalencePoset :: Equivalence a -> Poset' a +equivalencePoset (Equivalence p) = Poset p + +-- | Convert a 'PartialOrder'' to a 'Poset'' by extracting the @<=@ relation. +-- Returns 'True' when the partial order yields 'Just' 'LT' or 'Just' 'EQ', +-- 'False' otherwise (including incomparable elements). +-- +-- >>> import Data.Valuation.PartialOrder (totalOrder, runPartialOrder) +-- >>> let po = totalOrder :: PartialOrder' Int +-- >>> runPoset (fromPartialOrder po) 1 2 +-- True +-- >>> runPoset (fromPartialOrder po) 2 2 +-- True +-- >>> runPoset (fromPartialOrder po) 3 2 +-- False +-- +-- >>> import qualified Data.Set as Set +-- >>> import Data.Valuation.PartialOrder (fromLeq) +-- >>> runPoset (fromPartialOrder (fromLeq Set.isSubsetOf)) (Set.fromList [1,2]) (Set.fromList [2,3 :: Int]) +-- False +fromPartialOrder :: PartialOrder' a -> Poset' a +fromPartialOrder po = Poset (partialOrderLeq po) + +-- | Convert a 'Poset'' to a 'PartialOrder'' by inferring the full ordering +-- from the @<=@ relation. +-- +-- * @a <= b@ and @b <= a@ implies @a = b@ ('Just' 'EQ') +-- * @a <= b@ and not @b <= a@ implies @a < b@ ('Just' 'LT') +-- * not @a <= b@ and @b <= a@ implies @a > b@ ('Just' 'GT') +-- * neither implies incomparable ('Nothing') +-- +-- >>> import Data.Valuation.PartialOrder (runPartialOrder) +-- >>> let p = totalPoset :: Poset' Int +-- >>> runPartialOrder (toPartialOrder p) 1 2 +-- Just LT +-- >>> runPartialOrder (toPartialOrder p) 2 2 +-- Just EQ +-- >>> runPartialOrder (toPartialOrder p) 3 2 +-- Just GT +-- +-- >>> import qualified Data.Set as Set +-- >>> import Data.Valuation.PartialOrder (runPartialOrder) +-- >>> runPartialOrder (toPartialOrder (Poset Set.isSubsetOf)) (Set.fromList [1,2]) (Set.fromList [2,3 :: Int]) +-- Nothing +toPartialOrder :: Poset' a -> PartialOrder' a +toPartialOrder (Poset f) = fromLeq f + +-- | +-- >>> import Data.Functor.Contravariant (contramap) +-- >>> runPoset (contramap negate (totalPoset :: Poset' Int)) 1 2 +-- False +-- >>> runPoset (contramap negate (totalPoset :: Poset' Int)) 2 1 +-- True +instance (Profunctor p) => Contravariant (Poset p) where + contramap f (Poset g) = Poset (dimap f (lmap f) g) + +-- | Conjunction as a first-class 'Semigroup': @a <= b@ in the combined +-- poset iff @a <= b@ in /both/ component posets (the product order). +-- +-- >>> let p = totalPoset :: Poset' Int +-- >>> runPoset (runSemigroup semigroupPoset p p) 1 2 +-- True +-- >>> runPoset (runSemigroup semigroupPoset p p) 2 2 +-- True +-- >>> runPoset (runSemigroup semigroupPoset p p) 3 2 +-- False +-- +-- Two independent orderings: +-- +-- >>> let byVal = totalPoset :: Poset' (Int, Int) +-- >>> let byFst = Poset (\(a,_) (b,_) -> a <= b) :: Poset' (Int, Int) +-- >>> runPoset (runSemigroup semigroupPoset byVal byFst) (1, 2) (1, 3) +-- True +-- >>> runPoset (runSemigroup semigroupPoset byVal byFst) (1, 3) (1, 2) +-- False +semigroupPoset :: (Pro.Representable p, Apply (Pro.Rep p)) => Semigroup' (Poset p a) +semigroupPoset = review applySemigroup $ \(Poset pf) (Poset pg) -> + Poset $ Pro.tabulate $ \a -> + liftF2 + ( \innerF innerG -> Pro.tabulate $ \b -> + liftF2 (&&) (sieve innerF b) (sieve innerG b) + ) + (sieve pf a) + (sieve pg a) +{-# SPECIALIZE semigroupPoset :: Semigroup' (Poset' a) #-} + +-- | +-- >>> let p = totalPoset :: Poset' Int +-- >>> runPoset (p <> p) 1 2 +-- True +-- >>> runPoset (p <> p) 2 2 +-- True +-- >>> runPoset (p <> p) 3 2 +-- False +instance (Pro.Representable p, Apply (Pro.Rep p)) => Prelude.Semigroup (Poset p a) where + (<>) = runSemigroup semigroupPoset + +-- | The trivial poset where all elements are related: @a <= b@ for all @a@, @b@. +-- +-- >>> runPoset (mempty :: Poset' Int) 1 2 +-- True +-- >>> runPoset (mempty :: Poset' Int) 42 0 +-- True +instance (Pro.Representable p, Apply (Pro.Rep p), Applicative (Pro.Rep p)) => Monoid (Poset p a) where + mempty = Poset (Pro.tabulate (\_ -> pure (Pro.tabulate (\_ -> pure True)))) + +-- | Product order: split @a@ into @(b, c)@, check @b <= b'@ and @c <= c'@ +-- in both component posets. @conquer@ treats all elements as related. +-- +-- >>> import Data.Functor.Contravariant.Divisible (divide, conquer) +-- >>> let p = divide id (totalPoset :: Poset' Int) (totalPoset :: Poset' Int) +-- >>> runPoset p (1, 2) (1, 3) +-- True +-- >>> runPoset p (1, 2) (2, 1) +-- False +-- >>> runPoset p (1, 2) (1, 2) +-- True +-- +-- >>> import Data.Functor.Contravariant.Divisible (conquer) +-- >>> runPoset (conquer :: Poset' Int) 1 2 +-- True +instance (Pro.Representable p, Apply (Pro.Rep p), Applicative (Pro.Rep p)) => Divisible (Poset p) where + conquer = mempty + divide f pb pc = contramap (fst . f) pb <> contramap (snd . f) pc + +-- | Disjoint sum: classify @a@ as 'Left' @b@ or 'Right' @c@. +-- Elements on the same side are compared by that side's poset. +-- Elements on different sides are not related ('False'). +-- +-- >>> import Data.Functor.Contravariant.Divisible (choose, lose) +-- >>> import Data.Void (Void, absurd) +-- >>> let p = choose id (totalPoset :: Poset' Int) (totalPoset :: Poset' String) +-- >>> runPoset p (Left 1) (Left 2) +-- True +-- >>> runPoset p (Right "a") (Right "b") +-- True +-- >>> runPoset p (Left 1) (Right "a") +-- False +-- >>> runPoset p (Right "a") (Left 1) +-- False +-- +-- >>> import Data.Functor.Contravariant.Divisible (lose) +-- >>> import Data.Void (Void, absurd) +-- >>> let p = lose absurd :: Poset' Void +-- >>> seq p () +-- () +instance (Pro.Representable p, Apply (Pro.Rep p), Monad (Pro.Rep p)) => Decidable (Poset p) where + lose f = Poset (Pro.tabulate (absurd . f)) + choose f pb pc = Poset $ Pro.tabulate $ \a1 -> + pure $ Pro.tabulate $ \a2 -> + case (f a1, f a2) of + (Left b1, Left b2) -> sieve (runPoset pb) b1 >>= \inner -> sieve inner b2 + (Right c1, Right c2) -> sieve (runPoset pc) c1 >>= \inner -> sieve inner c2 + _ -> pure False + +-- | +-- >>> import Data.Functor.Contravariant.Divise (divise) +-- >>> let p = divise id (totalPoset :: Poset' Int) (totalPoset :: Poset' Int) +-- >>> runPoset p (1, 2) (1, 3) +-- True +-- >>> runPoset p (1, 2) (1, 2) +-- True +-- >>> runPoset p (1, 2) (2, 1) +-- False +instance (Pro.Representable p, Apply (Pro.Rep p)) => Divise (Poset p) where + divise f pb pc = contramap (fst . f) pb <> contramap (snd . f) pc + +-- | +-- >>> import Data.Functor.Contravariant.Decide (decide) +-- >>> let p = decide id (totalPoset :: Poset' Int) (totalPoset :: Poset' String) +-- >>> runPoset p (Left 1) (Left 2) +-- True +-- >>> runPoset p (Left 1) (Right "a") +-- False +instance (Pro.Representable p, Apply (Pro.Rep p), Monad (Pro.Rep p)) => Decide (Poset p) where + decide = choose + +-- | +-- >>> import Data.Functor.Contravariant.Conclude (conclude) +-- >>> import Data.Void (absurd) +-- >>> let p = conclude absurd :: Poset' Void +-- >>> seq p () +-- () +instance (Pro.Representable p, Apply (Pro.Rep p), Monad (Pro.Rep p)) => Conclude (Poset p) where + conclude = lose diff --git a/src/Data/Valuation/Presheaf.hs b/src/Data/Valuation/Presheaf.hs new file mode 100644 --- /dev/null +++ b/src/Data/Valuation/Presheaf.hs @@ -0,0 +1,271 @@ +{-# LANGUAGE RankNTypes #-} +{-# OPTIONS_GHC -Wall -Werror #-} + +-- | A reified presheaf: a contravariant mapping from one category to another, +-- wrapping @forall a b. cat a b -> cat' (f b) (f a)@. +-- +-- 'Presheaf' @cat cat' f@ reifies the action of a contravariant functor on +-- a type constructor @f@, generalised over a source category @cat@ and a +-- target category @cat'@. When both 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. +-- +-- @ +-- newtype 'Presheaf' cat cat' f = 'Presheaf' (forall a b. cat a b -> cat' (f b) (f a)) +-- type 'Presheaf'' f = 'Presheaf' (->) (->) f +-- @ +module Data.Valuation.Presheaf + ( Presheaf (..), + Presheaf', + + -- * combinators + runPresheaf, + composePresheafFunctor, + composeFunctorPresheaf, + composePresheaf, + contramapPresheaf, + + -- * presheaf values + predicatePresheaf, + comparisonPresheaf, + equivalencePresheaf, + proxyPresheaf, + constPresheaf, + + -- * laws + lawPresheafIdentity, + lawPresheafComposition, + ) +where + +import Data.Functor.Compose (Compose (..)) +import Data.Functor.Const (Const (..)) +import Data.Functor.Contravariant + ( Comparison (..), + Contravariant (contramap), + Equivalence (..), + Predicate (..), + ) +import Data.Profunctor (Profunctor (dimap)) +import Data.Proxy (Proxy) +import Data.Valuation.CovariantFunctor (CovariantFunctor (..)) + +-- $setup +-- >>> :set -Wno-name-shadowing -Wno-type-defaults +-- >>> import Data.Functor.Contravariant (Predicate(..), getPredicate, Comparison(..), getComparison, Equivalence(..), getEquivalence) +-- >>> import Data.Functor.Const (Const(..)) +-- >>> import Data.Proxy (Proxy(..)) + +-- | +-- >>> getPredicate (runPresheaf predicatePresheaf (+1) (Predicate even)) 3 +-- True +-- >>> getPredicate (runPresheaf predicatePresheaf (+1) (Predicate even)) 4 +-- False +-- +-- >>> getComparison (runPresheaf comparisonPresheaf negate (Comparison compare :: Comparison Int)) 1 2 +-- GT +newtype Presheaf cat cat' f = Presheaf (forall a b. cat a b -> cat' (f b) (f a)) + +-- | A 'Presheaf' specialised to @(->)@ for both categories. +-- Wraps @forall a b. (a -> b) -> f b -> f a@, equivalent to +-- 'Data.Functor.Contravariant.contramap'. +type Presheaf' f = Presheaf (->) (->) f + +-- | Unwrap a 'Presheaf' to its underlying natural transformation. +-- +-- >>> getPredicate (runPresheaf predicatePresheaf (+1) (Predicate even)) 3 +-- True +-- >>> getPredicate (runPresheaf predicatePresheaf (+1) (Predicate even)) 4 +-- False +-- +-- >>> getComparison (runPresheaf comparisonPresheaf negate (Comparison compare :: Comparison Int)) 1 2 +-- GT +-- >>> getComparison (runPresheaf comparisonPresheaf negate (Comparison compare :: Comparison Int)) 2 1 +-- LT +runPresheaf :: Presheaf cat cat' f -> cat a b -> cat' (f b) (f a) +runPresheaf (Presheaf f) = f + +-- | Compose a 'Presheaf' (contravariant) with a 'CovariantFunctor' (covariant). +-- The result is contravariant (contravariant ∘ covariant = contravariant). +-- +-- Given @f@ contravariant from @cat@ to @cat'@ and @g@ covariant from @cat'@ to @cat''@, +-- @g ∘ f@ is contravariant from @cat@ to @cat''@ acting on @'Compose' g f@. +-- +-- >>> import Data.Functor.Compose (Compose(..)) +-- >>> import Data.Valuation.CovariantFunctor (CovariantFunctor(..), proxyCovariantFunctor, maybeCovariantFunctor) +-- >>> let p = composePresheafFunctor constPresheaf proxyCovariantFunctor +-- >>> runPresheaf p not (Compose (Proxy :: Proxy (Const Int Bool))) +-- Compose Proxy +-- +-- >>> import Data.Functor.Compose (Compose(..)) +-- >>> import Data.Valuation.CovariantFunctor (CovariantFunctor(..), maybeCovariantFunctor) +-- >>> let p = composePresheafFunctor constPresheaf maybeCovariantFunctor +-- >>> runPresheaf p not (Compose (Just (Const 42 :: Const Int Bool))) +-- Compose (Just (Const 42)) +-- >>> runPresheaf p not (Compose Nothing :: Compose Maybe (Const Int) Bool) +-- Compose Nothing +composePresheafFunctor :: + (Profunctor cat'') => + Presheaf cat cat' f -> + CovariantFunctor cat' cat'' g -> + Presheaf cat cat'' (Compose g f) +composePresheafFunctor (Presheaf f) (CovariantFunctor g) = + Presheaf (dimap getCompose Compose . g . f) + +-- | Compose a 'CovariantFunctor' (covariant) with a 'Presheaf' (contravariant). +-- The result is contravariant (covariant ∘ contravariant = contravariant). +-- +-- Given @f@ covariant from @cat@ to @cat'@ and @g@ contravariant from @cat'@ to @cat''@, +-- @g ∘ f@ is contravariant from @cat@ to @cat''@ acting on @'Compose' g f@. +-- +-- >>> import Data.Functor.Compose (Compose(..)) +-- >>> import Data.Valuation.CovariantFunctor (CovariantFunctor(..), proxyCovariantFunctor, maybeCovariantFunctor) +-- >>> let p = composeFunctorPresheaf proxyCovariantFunctor constPresheaf +-- >>> runPresheaf p not (Compose (Const 42 :: Const Int (Proxy Bool))) +-- Compose (Const 42) +-- +-- >>> import Data.Functor.Compose (Compose(..)) +-- >>> import Data.Valuation.CovariantFunctor (CovariantFunctor(..), maybeCovariantFunctor) +-- >>> let p = composeFunctorPresheaf maybeCovariantFunctor constPresheaf +-- >>> runPresheaf p not (Compose (Const 42 :: Const Int (Maybe Bool))) +-- Compose (Const 42) +composeFunctorPresheaf :: + (Profunctor cat'') => + CovariantFunctor cat cat' f -> + Presheaf cat' cat'' g -> + Presheaf cat cat'' (Compose g f) +composeFunctorPresheaf (CovariantFunctor f) (Presheaf g) = + Presheaf (dimap getCompose Compose . g . f) + +-- | Compose two presheaves (contravariant functors) to obtain a covariant functor. +-- The result is covariant (contravariant ∘ contravariant = covariant). +-- +-- Given @f@ contravariant from @cat@ to @cat'@ and @g@ contravariant from @cat'@ to @cat''@, +-- @g ∘ f@ is covariant from @cat@ to @cat''@ acting on @'Compose' g f@. +-- +-- >>> import Data.Functor.Compose (Compose(..)) +-- >>> import Data.Valuation.CovariantFunctor (CovariantFunctor(..), runCovariantFunctor) +-- >>> let p = composePresheaf constPresheaf proxyPresheaf +-- >>> runCovariantFunctor p not (Compose (Proxy :: Proxy (Const Int Bool))) +-- Compose Proxy +-- +-- >>> import Data.Functor.Compose (Compose(..)) +-- >>> import Data.Valuation.CovariantFunctor (CovariantFunctor(..), runCovariantFunctor) +-- >>> let p = composePresheaf proxyPresheaf constPresheaf +-- >>> runCovariantFunctor p not (Compose (Const Proxy :: Const (Proxy Bool) (Proxy Bool))) +-- Compose (Const Proxy) +composePresheaf :: + (Profunctor cat'') => + Presheaf cat cat' f -> + Presheaf cat' cat'' g -> + CovariantFunctor cat cat'' (Compose g f) +composePresheaf (Presheaf f) (Presheaf g) = + CovariantFunctor (dimap getCompose Compose . g . f) + +-- | The canonical 'Presheaf'' for any 'Data.Functor.Contravariant.Contravariant' functor, +-- using 'Data.Functor.Contravariant.contramap'. +-- +-- >>> getPredicate (runPresheaf contramapPresheaf abs (Predicate (> 3) :: Predicate Int)) (-5) +-- True +-- >>> getPredicate (runPresheaf contramapPresheaf abs (Predicate (> 3) :: Predicate Int)) (-2) +-- False +-- +-- >>> getEquivalence (runPresheaf contramapPresheaf (`mod` 3) (Equivalence (==) :: Equivalence Int)) 4 7 +-- True +-- >>> getEquivalence (runPresheaf contramapPresheaf (`mod` 3) (Equivalence (==) :: Equivalence Int)) 4 6 +-- False +contramapPresheaf :: (Contravariant f) => Presheaf' f +contramapPresheaf = Presheaf contramap + +-- | 'Presheaf'' on 'Predicate': pulls back a predicate along a function. +-- +-- >>> getPredicate (runPresheaf predicatePresheaf even (Predicate not)) 2 +-- False +-- >>> getPredicate (runPresheaf predicatePresheaf even (Predicate not)) 3 +-- True +-- +-- >>> getPredicate (runPresheaf predicatePresheaf abs (Predicate (> 3) :: Predicate Int)) (-5) +-- True +-- >>> getPredicate (runPresheaf predicatePresheaf abs (Predicate (> 3) :: Predicate Int)) (-2) +-- False +predicatePresheaf :: Presheaf' Predicate +predicatePresheaf = Presheaf contramap + +-- | 'Presheaf'' on 'Comparison': pulls back a comparison along a function. +-- +-- >>> getComparison (runPresheaf comparisonPresheaf negate (Comparison compare :: Comparison Int)) 1 2 +-- GT +-- >>> getComparison (runPresheaf comparisonPresheaf negate (Comparison compare :: Comparison Int)) 2 1 +-- LT +-- +-- >>> getComparison (runPresheaf comparisonPresheaf length (Comparison compare :: Comparison Int)) "hi" "hello" +-- LT +comparisonPresheaf :: Presheaf' Comparison +comparisonPresheaf = Presheaf contramap + +-- | 'Presheaf'' on 'Equivalence': pulls back an equivalence relation along a function. +-- +-- >>> getEquivalence (runPresheaf equivalencePresheaf even (Equivalence (==) :: Equivalence Bool)) 2 4 +-- True +-- >>> getEquivalence (runPresheaf equivalencePresheaf even (Equivalence (==) :: Equivalence Bool)) 2 3 +-- False +-- +-- >>> getEquivalence (runPresheaf equivalencePresheaf (`mod` 3) (Equivalence (==) :: Equivalence Int)) 4 7 +-- True +equivalencePresheaf :: Presheaf' Equivalence +equivalencePresheaf = Presheaf contramap + +-- | 'Presheaf'' on 'Proxy': trivially maps the phantom type parameter. +-- +-- >>> runPresheaf proxyPresheaf not (Proxy :: Proxy Bool) +-- Proxy +-- +-- >>> runPresheaf proxyPresheaf length (Proxy :: Proxy Int) +-- Proxy +proxyPresheaf :: Presheaf' Proxy +proxyPresheaf = Presheaf contramap + +-- | 'Presheaf'' on @'Const' r@: trivially maps the phantom second parameter. +-- The constant value is preserved. +-- +-- >>> runPresheaf constPresheaf not (Const 42 :: Const Int Bool) +-- Const 42 +-- +-- >>> runPresheaf constPresheaf length (Const "hello" :: Const String Int) +-- Const "hello" +constPresheaf :: Presheaf' (Const r) +constPresheaf = Presheaf contramap + +-- | The identity law for a 'Presheaf'': mapping the identity morphism +-- must be the identity on @f a@. +-- +-- @ +-- 'runPresheaf' p 'id' x == x +-- @ +-- +-- >>> lawPresheafIdentity proxyPresheaf (Proxy :: Proxy Int) +-- True +-- >>> lawPresheafIdentity constPresheaf (Const 42 :: Const Int Bool) +-- True +lawPresheafIdentity :: (Eq (f a)) => Presheaf' f -> f a -> Bool +lawPresheafIdentity p x = + runPresheaf p id x == x + +-- | The composition law for a 'Presheaf'': mapping a composition must +-- equal composing the individual mappings, with contravariant reversal. +-- +-- @ +-- 'runPresheaf' p (g '.' f) x == 'runPresheaf' p f ('runPresheaf' p g x) +-- @ +-- +-- >>> lawPresheafComposition proxyPresheaf not (&&True) (Proxy :: Proxy Bool) +-- True +-- >>> lawPresheafComposition constPresheaf (+1) (*2) (Const "hello" :: Const String Int) +-- True +lawPresheafComposition :: (Eq (f a)) => Presheaf' f -> (b -> c) -> (a -> b) -> f c -> Bool +lawPresheafComposition p g f x = + runPresheaf p (g . f) x == runPresheaf p f (runPresheaf p g x) diff --git a/src/Data/Valuation/PresheafValuationAlgebra.hs b/src/Data/Valuation/PresheafValuationAlgebra.hs --- a/src/Data/Valuation/PresheafValuationAlgebra.hs +++ b/src/Data/Valuation/PresheafValuationAlgebra.hs @@ -19,6 +19,7 @@ ( PresheafValuationAlgebra (..), PresheafValuationAlgebra', SetPresheafValuationAlgebra, + SetPresheafValuationAlgebra', HasPresheafValuationAlgebra (..), AsPresheafValuationAlgebra (..), marginalise, @@ -79,53 +80,56 @@ -- | -- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int) -- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v)) --- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) Int Set Int +-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int -- >>> let pva = PresheafValuationAlgebra lat va -- >>> let v1 = Valuation (Set.fromList [1,2]) 10 :: Valuation Set Int Int -- >>> let v2 = Valuation (Set.fromList [2,3]) 20 -- >>> combine pva v1 v2 -- Valuation (fromList [1,2,3]) 30 -data PresheafValuationAlgebra p v set var +data PresheafValuationAlgebra p q r s v set var = PresheafValuationAlgebra -- | lattice structure on domains (DomainLattice p (set var) (set var)) -- | the valuation algebra - (ValuationAlgebra p v set var) + (ValuationAlgebra q r s v set var) type PresheafValuationAlgebra' v set var = - PresheafValuationAlgebra (->) v set var + PresheafValuationAlgebra (->) (->) (->) (->) v set var -- | A 'PresheafValuationAlgebra' specialised to 'Set'. -type SetPresheafValuationAlgebra p v var = - PresheafValuationAlgebra p v Set var +type SetPresheafValuationAlgebra p q r s v var = + PresheafValuationAlgebra p q r s v Set var +type SetPresheafValuationAlgebra' v var = + SetPresheafValuationAlgebra (->) (->) (->) (->) v var + -- | Classy lens for types that contain a 'PresheafValuationAlgebra'. -class HasPresheafValuationAlgebra c p v set var | c -> p v set var where - presheafValuationAlgebra :: Lens' c (PresheafValuationAlgebra p v set var) +class HasPresheafValuationAlgebra c p q r s v set var | c -> p q r s v set var where + presheafValuationAlgebra :: Lens' c (PresheafValuationAlgebra p q r s v set var) -instance HasPresheafValuationAlgebra (PresheafValuationAlgebra p v set var) p v set var where +instance HasPresheafValuationAlgebra (PresheafValuationAlgebra p q r s v set var) p q r s v set var where presheafValuationAlgebra = id -- | Classy prism for types that can be constructed from a 'PresheafValuationAlgebra'. -class AsPresheafValuationAlgebra c p v set var | c -> p v set var where - _PresheafValuationAlgebra :: Prism' c (PresheafValuationAlgebra p v set var) +class AsPresheafValuationAlgebra c p q r s v set var | c -> p q r s v set var where + _PresheafValuationAlgebra :: Prism' c (PresheafValuationAlgebra p q r s v set var) -instance AsPresheafValuationAlgebra (PresheafValuationAlgebra p v set var) p v set var where +instance AsPresheafValuationAlgebra (PresheafValuationAlgebra p q r s v set var) p q r s v set var where _PresheafValuationAlgebra = id -instance HasDomainLattice (PresheafValuationAlgebra p v set var) p (set var) (set var) where +instance HasDomainLattice (PresheafValuationAlgebra p q r s v set var) p (set var) (set var) where domainLattice f (PresheafValuationAlgebra l a) = fmap (`PresheafValuationAlgebra` a) (f l) -instance HasValuationAlgebra (PresheafValuationAlgebra p v set var) p v set var where +instance HasValuationAlgebra (PresheafValuationAlgebra p q r s v set var) q r s v set var where valuationAlgebra f (PresheafValuationAlgebra l a) = fmap (PresheafValuationAlgebra l) (f a) -instance HasSemiValuationAlgebra (PresheafValuationAlgebra p v set var) p v set var where +instance HasSemiValuationAlgebra (PresheafValuationAlgebra p q r s v set var) q r s v set var where semiValuationAlgebra = valuationAlgebra . semiValuationAlgebra -instance HasSemigroup (PresheafValuationAlgebra p v set var) p v where +instance HasSemigroup (PresheafValuationAlgebra p q r s v set var) q v where semigroup = semiValuationAlgebra . semigroup -instance HasProjectValuation (PresheafValuationAlgebra p v set var) p v set var where +instance HasProjectValuation (PresheafValuationAlgebra p q r s v set var) r s v set var where projectValuation = semiValuationAlgebra . projectValuation -- | Marginalise a valuation to a subdomain: the restriction map of the presheaf. @@ -139,14 +143,14 @@ -- -- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int) -- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\s v -> v + Set.size s)) --- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) Int Set Int +-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int -- >>> let pva = PresheafValuationAlgebra lat va -- >>> marginalise pva (Set.fromList [1]) (Valuation (Set.fromList [1,2]) 10) -- Valuation (fromList [1]) 11 {-# SPECIALIZE marginalise :: - PresheafValuationAlgebra (->) v set var -> set var -> Valuation set var v -> Valuation set var v + PresheafValuationAlgebra' v set var -> set var -> Valuation set var v -> Valuation set var v #-} -marginalise :: (HasProjectValuation algebra (->) v set var, HasValuation valuation set' var' v) => algebra -> set var -> valuation -> Valuation set var v +marginalise :: (HasProjectValuation algebra (->) (->) v set var, HasValuation valuation set' var' v) => algebra -> set var -> valuation -> Valuation set var v marginalise algebra targetDomain = Valuation targetDomain . view (projectValuation . _Wrapped) algebra targetDomain . view valuationInformation @@ -159,22 +163,22 @@ -- -- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int) -- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v)) --- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) Int Set Int +-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int -- >>> let pva = PresheafValuationAlgebra lat va -- >>> combine pva (Valuation (Set.fromList [1,2]) 10) (Valuation (Set.fromList [2,3]) 20) -- Valuation (fromList [1,2,3]) 30 -- -- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int) -- >>> let sva = SemiValuationAlgebra (review applySemigroup (*)) (ProjectValuation (\_ v -> v)) --- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 1)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) Int Set Int +-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 1)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int -- >>> let pva = PresheafValuationAlgebra lat va -- >>> combine pva (Valuation (Set.fromList [1]) 3) (Valuation (Set.fromList [2]) 4) -- Valuation (fromList [1,2]) 12 {-# SPECIALIZE combine :: - PresheafValuationAlgebra (->) v set var -> Valuation set var v -> Valuation set var v -> Valuation set var v + PresheafValuationAlgebra' v set var -> Valuation set var v -> Valuation set var v -> Valuation set var v #-} combine :: - (HasSemigroup s1 (->) a, HasDomainLattice s1 (->) (set var) p, HasValuation s2 set var a, HasValuation s3 set var a) => s1 -> s2 -> s3 -> Valuation set var a + (HasSemigroup s1 (->) a, HasDomainLattice s1 (->) (set var) (set var), HasValuation s2 set var a, HasValuation s3 set var a) => s1 -> s2 -> s3 -> Valuation set var a combine alg phi = Valuation . runSemigroup (view domainLatticeJoin alg) (view valuationDomain phi) . view valuationDomain <*> runSemigroup (view semigroup alg) (view valuationInformation phi) . view valuationInformation @@ -183,14 +187,14 @@ -- -- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int) -- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v)) --- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 99)) :: ValuationAlgebra (->) Int Set Int +-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 99)) :: ValuationAlgebra (->) (->) (->) Int Set Int -- >>> let pva = PresheafValuationAlgebra lat va -- >>> neutralValuation pva (Set.fromList [1,2]) -- Valuation (fromList [1,2]) 0 {-# SPECIALIZE neutralValuation :: - PresheafValuationAlgebra (->) v set var -> set var -> Valuation set var v + PresheafValuationAlgebra' v set var -> set var -> Valuation set var v #-} -neutralValuation :: (HasValuationAlgebra s (->) a set var) => s -> set var -> Valuation set var a +neutralValuation :: (HasValuationAlgebra s (->) (->) (->) a set var) => s -> set var -> Valuation set var a neutralValuation algebra = Valuation <*> view (valuationAlgebra . valuationAlgebraUnit . _Wrapped) algebra @@ -199,14 +203,14 @@ -- -- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int) -- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v)) --- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 99)) :: ValuationAlgebra (->) Int Set Int +-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 99)) :: ValuationAlgebra (->) (->) (->) Int Set Int -- >>> let pva = PresheafValuationAlgebra lat va -- >>> nullValuation pva (Set.fromList [1,2]) -- Valuation (fromList [1,2]) 99 {-# SPECIALIZE nullValuation :: - PresheafValuationAlgebra (->) v set var -> set var -> Valuation set var v + PresheafValuationAlgebra' v set var -> set var -> Valuation set var v #-} -nullValuation :: (HasValuationAlgebra s (->) a set var) => s -> set var -> Valuation set var a +nullValuation :: (HasValuationAlgebra s (->) (->) (->) a set var) => s -> set var -> Valuation set var a nullValuation algebra = Valuation <*> view (valuationAlgebra . valuationAlgebraZero . _Wrapped) algebra @@ -215,30 +219,30 @@ -- -- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int) -- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v)) --- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) Int Set Int +-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int -- >>> let pva = PresheafValuationAlgebra lat va -- >>> let sg = presheafCombineSemigroup pva -- >>> runSemigroup sg (Valuation (Set.fromList [1]) 10) (Valuation (Set.fromList [2]) 20) -- Valuation (fromList [1,2]) 30 {-# SPECIALIZE presheafCombineSemigroup :: - PresheafValuationAlgebra (->) v set var -> Semigroup' (Valuation set var v) + PresheafValuationAlgebra' v set var -> Semigroup' (Valuation set var v) #-} -presheafCombineSemigroup :: (HasSemigroup algebra (->) v, HasDomainLattice algebra (->) (set var) p) => algebra -> Semigroup' (Valuation set var v) +presheafCombineSemigroup :: (HasSemigroup algebra (->) v, HasDomainLattice algebra (->) (set var) (set var)) => algebra -> Semigroup' (Valuation set var v) presheafCombineSemigroup = review applySemigroup . combine -- | Transitivity of marginalisation: @(phi↓d')↓d'' = phi↓d''@ for @d'' <= d' <= d(phi)@. -- -- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int) -- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v)) --- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) Int Set Int +-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int -- >>> let pva = PresheafValuationAlgebra lat va -- >>> let phi = Valuation (Set.fromList [1,2,3]) 10 -- >>> lawTransitivity pva (Set.fromList [1,2]) (Set.fromList [1]) phi -- True {-# SPECIALIZE lawTransitivity :: - (Eq v) => PresheafValuationAlgebra (->) v set var -> set var -> set var -> Valuation set var v -> Bool + (Eq v) => PresheafValuationAlgebra' v set var -> set var -> set var -> Valuation set var v -> Bool #-} -lawTransitivity :: (Eq a, HasProjectValuation p (->) a set var, HasValuation q set' var' a) => p -> set var -> set var -> q -> Bool +lawTransitivity :: (Eq a, HasProjectValuation p (->) (->) a set var, HasValuation q set' var' a) => p -> set var -> set var -> q -> Bool lawTransitivity pva d' d'' phi = let step = marginalise pva d'' (marginalise pva d' phi) direct = marginalise pva d'' phi @@ -249,14 +253,14 @@ -- -- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int) -- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v)) --- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) Int Set Int +-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int -- >>> let pva = PresheafValuationAlgebra lat va -- >>> lawCombinationDomain pva (Valuation (Set.fromList [1,2]) 10) (Valuation (Set.fromList [2,3]) 20) -- True {-# SPECIALIZE lawCombinationDomain :: - (Eq (set var)) => PresheafValuationAlgebra (->) v set var -> Valuation set var v -> Valuation set var v -> Bool + (Eq (set var)) => PresheafValuationAlgebra' v set var -> Valuation set var v -> Valuation set var v -> Bool #-} -lawCombinationDomain :: (HasSemigroup s1 (->) a, Eq (set var), HasValuation s2 set var a, HasValuation s3 set var a, HasDomainLattice s1 (->) (set var) p) => s1 -> s2 -> s3 -> Bool +lawCombinationDomain :: (HasSemigroup s1 (->) a, Eq (set var), HasValuation s2 set var a, HasValuation s3 set var a, HasDomainLattice s1 (->) (set var) (set var)) => s1 -> s2 -> s3 -> Bool lawCombinationDomain pva val1 val2 = let lat = view domainLattice pva d1 = view valuationDomain val1 @@ -268,14 +272,14 @@ -- -- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int) -- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v)) --- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) Int Set Int +-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int -- >>> let pva = PresheafValuationAlgebra lat va -- >>> lawMarginalisationIdentity pva (Valuation (Set.fromList [1,2]) 42) -- True {-# SPECIALIZE lawMarginalisationIdentity :: - (Eq (set var), Eq v) => PresheafValuationAlgebra (->) v set var -> Valuation set var v -> Bool + (Eq (set var), Eq v) => PresheafValuationAlgebra' v set var -> Valuation set var v -> Bool #-} -lawMarginalisationIdentity :: (Eq a, Eq (set var), HasValuation s set var a, HasProjectValuation p (->) a set var) => p -> s -> Bool +lawMarginalisationIdentity :: (Eq a, Eq (set var), HasValuation s set var a, HasProjectValuation p (->) (->) a set var) => p -> s -> Bool lawMarginalisationIdentity pva val = let d = view valuationDomain val v = view valuationInformation val @@ -287,15 +291,15 @@ -- -- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int) -- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v)) --- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) Int Set Int +-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int -- >>> let pva = PresheafValuationAlgebra lat va -- >>> let phi = Valuation (Set.fromList [1]) 42 -- >>> lawNeutralCombination pva (Set.fromList [1,2]) phi -- True {-# SPECIALIZE lawNeutralCombination :: - (Eq (set var), Eq v) => PresheafValuationAlgebra (->) v set var -> set var -> Valuation set var v -> Bool + (Eq (set var), Eq v) => PresheafValuationAlgebra' v set var -> set var -> Valuation set var v -> Bool #-} -lawNeutralCombination :: (HasSemigroup s1 (->) a, Eq a, Eq (set var), HasDomainLattice s1 (->) (set var) (set var), HasValuation s2 set var a, HasValuationAlgebra s1 (->) a set var) => s1 -> set var -> s2 -> Bool +lawNeutralCombination :: (HasSemigroup s1 (->) a, Eq a, Eq (set var), HasDomainLattice s1 (->) (set var) (set var), HasValuation s2 set var a, HasValuationAlgebra s1 (->) (->) (->) a set var) => s1 -> set var -> s2 -> Bool lawNeutralCombination pva d phi = let lat = view domainLattice pva dPhi = view valuationDomain phi @@ -309,15 +313,15 @@ -- -- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int) -- >>> let sva = SemiValuationAlgebra (review applySemigroup (*)) (ProjectValuation (\_ v -> v)) --- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 1)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) Int Set Int +-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 1)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int -- >>> let pva = PresheafValuationAlgebra lat va -- >>> let phi = Valuation (Set.fromList [1]) 42 -- >>> lawNullCombination pva (Set.fromList [2]) phi -- True {-# SPECIALIZE lawNullCombination :: - (Eq (set var), Eq v) => PresheafValuationAlgebra (->) v set var -> set var -> Valuation set var v -> Bool + (Eq (set var), Eq v) => PresheafValuationAlgebra' v set var -> set var -> Valuation set var v -> Bool #-} -lawNullCombination :: (HasSemigroup s1 (->) a, Eq a, Eq (set var), HasValuation s2 set var a, HasDomainLattice s1 (->) (set var) p, HasValuationAlgebra s1 (->) a set var) => s1 -> set var -> s2 -> Bool +lawNullCombination :: (HasSemigroup s1 (->) a, Eq a, Eq (set var), HasValuation s2 set var a, HasDomainLattice s1 (->) (set var) (set var), HasValuationAlgebra s1 (->) (->) (->) a set var) => s1 -> set var -> s2 -> Bool lawNullCombination pva d phi = let lat = view domainLattice pva dPhi = view valuationDomain phi @@ -332,14 +336,14 @@ -- -- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int) -- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v)) --- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) Int Set Int +-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int -- >>> let pva = PresheafValuationAlgebra lat va -- >>> lawCombinationCommutative pva (Valuation (Set.fromList [1]) 10) (Valuation (Set.fromList [2]) 20) -- True {-# SPECIALIZE lawCombinationCommutative :: - (Eq (set var), Eq v) => PresheafValuationAlgebra (->) v set var -> Valuation set var v -> Valuation set var v -> Bool + (Eq (set var), Eq v) => PresheafValuationAlgebra' v set var -> Valuation set var v -> Valuation set var v -> Bool #-} -lawCombinationCommutative :: (HasSemigroup s1 (->) a, Eq a, Eq (set var), HasDomainLattice s1 (->) (set var) p, HasValuation s2 set var a, HasValuation s3 set var a) => s1 -> s2 -> s3 -> Bool +lawCombinationCommutative :: (HasSemigroup s1 (->) a, Eq a, Eq (set var), HasDomainLattice s1 (->) (set var) (set var), HasValuation s2 set var a, HasValuation s3 set var a) => s1 -> s2 -> s3 -> Bool lawCombinationCommutative pva phi psi = let Valuation d1 v1 = combine pva phi psi Valuation d2 v2 = combine pva psi phi diff --git a/src/Data/Valuation/ProjectValuation.hs b/src/Data/Valuation/ProjectValuation.hs --- a/src/Data/Valuation/ProjectValuation.hs +++ b/src/Data/Valuation/ProjectValuation.hs @@ -10,6 +10,7 @@ ( ProjectValuation (..), ProjectValuation', SetProjectValuation, + SetProjectValuation', -- * optics HasProjectValuation (..), @@ -59,76 +60,76 @@ -- -- >>> let ProjectValuation f = ProjectValuation (\s v -> v + length s) in f [1,2,3] (10 :: Int) -- 13 -newtype ProjectValuation p v set var - = ProjectValuation (p (set var) (p v v)) +newtype ProjectValuation p q v set var + = ProjectValuation (p (set var) (q v v)) type ProjectValuation' v set var = - ProjectValuation (->) v set var + ProjectValuation (->) (->) v set var instance - (ProjectValuation p v set var ~ t) => - Rewrapped (ProjectValuation p' v' set' var') t + (ProjectValuation p q v set var ~ t) => + Rewrapped (ProjectValuation p' q' v' set' var') t -instance Wrapped (ProjectValuation p v set var) where - type Unwrapped (ProjectValuation p v set var) = p (set var) (p v v) +instance Wrapped (ProjectValuation p q v set var) where + type Unwrapped (ProjectValuation p q v set var) = p (set var) (q v v) _Wrapped' = iso (\(ProjectValuation x) -> x) ProjectValuation -- | Classy lens for types that contain a 'ProjectValuation'. -class HasProjectValuation c p v set var | c -> p v set var where - projectValuation :: Lens' c (ProjectValuation p v set var) +class HasProjectValuation c p q v set var | c -> p q v set var where + projectValuation :: Lens' c (ProjectValuation p q v set var) -instance HasProjectValuation (ProjectValuation p v set var) p v set var where +instance HasProjectValuation (ProjectValuation p q v set var) p q v set var where projectValuation = id -- | Classy prism for types that can be constructed from a 'ProjectValuation'. -class AsProjectValuation c p v set var | c -> p v set var where - _ProjectValuation :: Prism' c (ProjectValuation p v set var) +class AsProjectValuation c p q v set var | c -> p q v set var where + _ProjectValuation :: Prism' c (ProjectValuation p q v set var) -instance AsProjectValuation (ProjectValuation p v set var) p v set var where +instance AsProjectValuation (ProjectValuation p q v set var) p q v set var where _ProjectValuation = id -- | Lens to the underlying function of a 'HasProjectValuation'. -applyHasProjectValuation :: (HasProjectValuation pv p v set var) => Lens' pv (p (set var) (p v v)) +applyHasProjectValuation :: (HasProjectValuation pv p q v set var) => Lens' pv (p (set var) (q v v)) applyHasProjectValuation = projectValuation . _Wrapped -- | Prism to the underlying function of an 'AsProjectValuation'. -applyAsProjectValuation :: (AsProjectValuation pv p v set var) => Prism' pv (p (set var) (p v v)) +applyAsProjectValuation :: (AsProjectValuation pv p q v set var) => Prism' pv (p (set var) (q v v)) applyAsProjectValuation = _ProjectValuation . _Wrapped -- | -- >>> import Data.Functor.Contravariant (contramap) --- >>> let pv = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) Int [] Int +-- >>> let pv = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) (->) Int [] Int -- >>> let ProjectValuation f = contramap (*2) pv in f [1,2,3] 10 -- 22 -- -- >>> import Data.Functor.Contravariant (contramap) --- >>> let pv = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) Int [] Int +-- >>> let pv = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) (->) Int [] Int -- >>> let ProjectValuation f = contramap negate pv in f [1,2,3] 0 -- -6 -instance (Functor set, Profunctor p) => Contravariant (ProjectValuation p v set) where +instance (Functor set, Profunctor p) => Contravariant (ProjectValuation p q v set) where contramap f (ProjectValuation g) = ProjectValuation (lmap (fmap f) g) -- | -- >>> import Data.Functor.Contravariant.Divisible (conquer, divide) --- >>> let ProjectValuation f = conquer :: ProjectValuation (->) Int [] Int in f [1,2,3] 42 +-- >>> let ProjectValuation f = conquer :: ProjectValuation (->) (->) Int [] Int in f [1,2,3] 42 -- 42 -- -- >>> import Data.Functor.Contravariant.Divisible (conquer, divide) --- >>> let ProjectValuation f = conquer :: ProjectValuation (->) String [] Char in f "abc" "hello" +-- >>> let ProjectValuation f = conquer :: ProjectValuation (->) (->) String [] Char in f "abc" "hello" -- "hello" -- -- >>> import Data.Functor.Contravariant.Divisible (conquer, divide) --- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) Int [] Int --- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation (->) Int [] Int +-- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) (->) Int [] Int +-- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation (->) (->) Int [] Int -- >>> let ProjectValuation f = divide (\x -> (x, x * 10)) pvB pvC in f [1,2,3] 5 -- 21 -- -- >>> import Data.Functor.Contravariant.Divisible (conquer, divide) --- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) Int [] Int --- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation (->) Int [] Int +-- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) (->) Int [] Int +-- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation (->) (->) Int [] Int -- >>> let ProjectValuation f = divide (\x -> (x, x)) pvB pvC in f [1,2,3] 5 -- 21 -instance (Functor set, Strong p, Category p) => Divisible (ProjectValuation p v set) where +instance (Functor set, Strong p, Category p, Category q) => Divisible (ProjectValuation p q v set) where conquer = ProjectValuation (rmap (const id) id) divide split (ProjectValuation pb) (ProjectValuation pc) = let pb' = lmap (fmap (fst . split)) pb @@ -138,27 +139,27 @@ -- | -- >>> import Data.Functor.Contravariant.Divisible (choose, lose) -- >>> import Data.Void (Void, absurd) --- >>> let ProjectValuation f = lose absurd :: ProjectValuation (->) Int [] Void in f [] 42 +-- >>> let ProjectValuation f = lose absurd :: ProjectValuation (->) (->) Int [] Void in f [] 42 -- 42 -- -- >>> import Data.Functor.Contravariant.Divisible (choose) --- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) Int [] Int --- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation (->) Int [] Int +-- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) (->) Int [] Int +-- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation (->) (->) Int [] Int -- >>> let ProjectValuation f = choose (\x -> if even x then Left x else Right x) pvB pvC in f [1,2,3,4] 10 -- 26 -- -- >>> import Data.Functor.Contravariant.Divisible (choose) --- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) Int [] Int --- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation (->) Int [] Int +-- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) (->) Int [] Int +-- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation (->) (->) Int [] Int -- >>> let ProjectValuation f = choose Left pvB pvC in f [1,2,3] 10 -- 6 -- -- >>> import Data.Functor.Contravariant.Divisible (choose) --- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) Int [] Int --- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation (->) Int [] Int +-- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) (->) Int [] Int +-- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation (->) (->) Int [] Int -- >>> let ProjectValuation f = choose Right pvB pvC in f [1,2,3] 10 -- 30 -instance (Filterable set, Strong p, Category p) => Decidable (ProjectValuation p v set) where +instance (Filterable set, Strong p, Category p, Category q) => Decidable (ProjectValuation p q v set) where lose _ = ProjectValuation (rmap (const id) id) choose ch (ProjectValuation pb) (ProjectValuation pc) = let pb' = lmap (mapMaybe (either Just (const Nothing) . ch)) pb @@ -167,11 +168,11 @@ -- | -- >>> import Data.Functor.Contravariant.Divise (divise) --- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) Int [] Int --- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation (->) Int [] Int +-- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) (->) Int [] Int +-- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation (->) (->) Int [] Int -- >>> let ProjectValuation f = divise (\x -> (x, x * 10)) pvB pvC in f [1,2,3] 5 -- 21 -instance (Functor set, Strong p, Semigroupoid p) => Divise (ProjectValuation p v set) where +instance (Functor set, Strong p, Semigroupoid p, Semigroupoid q) => Divise (ProjectValuation p q v set) where divise split (ProjectValuation pb) (ProjectValuation pc) = let pb' = lmap (fmap (fst . split)) pb pc' = lmap (fmap (snd . split)) pc @@ -179,11 +180,11 @@ -- | -- >>> import Data.Functor.Contravariant.Decide (decide) --- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) Int [] Int --- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation (->) Int [] Int +-- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) (->) Int [] Int +-- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation (->) (->) Int [] Int -- >>> let ProjectValuation f = decide (\x -> if even x then Left x else Right x) pvB pvC in f [1,2,3,4] 10 -- 26 -instance (Filterable set, Strong p, Semigroupoid p) => Decide (ProjectValuation p v set) where +instance (Filterable set, Strong p, Semigroupoid p, Semigroupoid q) => Decide (ProjectValuation p q v set) where decide ch (ProjectValuation pb) (ProjectValuation pc) = let pb' = lmap (mapMaybe (either Just (const Nothing) . ch)) pb pc' = lmap (mapMaybe (either (const Nothing) Just . ch)) pc @@ -192,32 +193,35 @@ -- | -- >>> import Data.Functor.Contravariant.Conclude (conclude) -- >>> import Data.Void (absurd) --- >>> let ProjectValuation f = conclude absurd :: ProjectValuation (->) Int [] Void in f [] 42 +-- >>> let ProjectValuation f = conclude absurd :: ProjectValuation (->) (->) Int [] Void in f [] 42 -- 42 -instance (Filterable set, Strong p, Semigroupoid p, Category p) => Conclude (ProjectValuation p v set) where +instance (Filterable set, Strong p, Semigroupoid p, Category p, Semigroupoid q, Category q) => Conclude (ProjectValuation p q v set) where conclude _ = ProjectValuation (rmap (const id) id) -- | -- >>> let ProjectValuation f = runSemigroup semigroupProjectValuation (ProjectValuation (\_ v -> v + 1)) (ProjectValuation (\_ v -> v * 2)) in f [] (3 :: Int) -- 7 -semigroupProjectValuation :: Semigroup' (ProjectValuation (->) v set var) +semigroupProjectValuation :: Semigroup' (ProjectValuation' v set var) semigroupProjectValuation = review applySemigroup (\(ProjectValuation p1) (ProjectValuation p2) -> ProjectValuation (\s -> p1 s . p2 s)) -- | --- >>> let p1 = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) Int [] Int --- >>> let p2 = ProjectValuation (\s v -> v * length s) :: ProjectValuation (->) Int [] Int +-- >>> let p1 = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) (->) Int [] Int +-- >>> let p2 = ProjectValuation (\s v -> v * length s) :: ProjectValuation (->) (->) Int [] Int -- >>> let ProjectValuation f = p1 <> p2 in f [1,2,3] 5 -- 21 -instance Prelude.Semigroup (ProjectValuation (->) v set var) where +instance Prelude.Semigroup (ProjectValuation' v set var) where (<>) = runSemigroup semigroupProjectValuation -- | --- >>> let p = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) Int [] Int +-- >>> let p = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) (->) Int [] Int -- >>> let ProjectValuation f = mempty <> p in f [1,2,3] 5 -- 11 -instance Monoid (ProjectValuation (->) v set var) where +instance Monoid (ProjectValuation' v set var) where mempty = ProjectValuation (const id) -- | A 'ProjectValuation' specialised to 'Set'. -type SetProjectValuation p v var = - ProjectValuation p v Set var +type SetProjectValuation p q v var = + ProjectValuation p q v Set var + +type SetProjectValuation' v var = + SetProjectValuation (->) (->) v var diff --git a/src/Data/Valuation/SemiValuationAlgebra.hs b/src/Data/Valuation/SemiValuationAlgebra.hs --- a/src/Data/Valuation/SemiValuationAlgebra.hs +++ b/src/Data/Valuation/SemiValuationAlgebra.hs @@ -7,6 +7,7 @@ ( SemiValuationAlgebra (..), SemiValuationAlgebra', SetSemiValuationAlgebra, + SetSemiValuationAlgebra', -- * optics HasSemiValuationAlgebra (..), @@ -54,75 +55,75 @@ -- >>> import Prelude hiding (Semigroup) -- | --- >>> let SemiValuationAlgebra sg (ProjectValuation p) = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\s v -> v + sum s)) :: SemiValuationAlgebra (->) Int [] Int +-- >>> let SemiValuationAlgebra sg (ProjectValuation p) = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\s v -> v + sum s)) :: SemiValuationAlgebra (->) (->) (->) Int [] Int -- >>> runSemigroup sg 3 4 -- 7 -- >>> p [1,2,3] 10 -- 16 -data SemiValuationAlgebra p v set var +data SemiValuationAlgebra p q r v set var = SemiValuationAlgebra -- | algebra combine (Semigroup p v) -- | algebra project - (ProjectValuation p v set var) + (ProjectValuation q r v set var) type SemiValuationAlgebra' v set var = - SemiValuationAlgebra (->) v set var + SemiValuationAlgebra (->) (->) (->) v set var -- | Type-changing lens to the 'ProjectValuation' component. -projectValuation' :: Lens (SemiValuationAlgebra p v set var) (SemiValuationAlgebra p v set' var') (ProjectValuation p v set var) (ProjectValuation p v set' var') +projectValuation' :: Lens (SemiValuationAlgebra p q r v set var) (SemiValuationAlgebra p q' r' v set' var') (ProjectValuation q r v set var) (ProjectValuation q' r' v set' var') projectValuation' f (SemiValuationAlgebra s p) = fmap (SemiValuationAlgebra s) (f p) -- | Classy lens for types that contain a 'SemiValuationAlgebra'. -class HasSemiValuationAlgebra c p v set var | c -> p v set var where +class HasSemiValuationAlgebra c p q r v set var | c -> p q r v set var where semiValuationAlgebra :: - Lens' c (SemiValuationAlgebra p v set var) + Lens' c (SemiValuationAlgebra p q r v set var) -instance HasSemiValuationAlgebra (SemiValuationAlgebra p v set var) p v set var where +instance HasSemiValuationAlgebra (SemiValuationAlgebra p q r v set var) p q r v set var where semiValuationAlgebra = id -- | Classy prism for types that can be constructed from a 'SemiValuationAlgebra'. -class AsSemiValuationAlgebra c p v set var | c -> p v set var where +class AsSemiValuationAlgebra c p q r v set var | c -> p q r v set var where _SemiValuationAlgebra :: - Prism' c (SemiValuationAlgebra p v set var) + Prism' c (SemiValuationAlgebra p q r v set var) -instance AsSemiValuationAlgebra (SemiValuationAlgebra p v set var) p v set var where +instance AsSemiValuationAlgebra (SemiValuationAlgebra p q r v set var) p q r v set var where _SemiValuationAlgebra = id -instance HasSemigroup (SemiValuationAlgebra p v set var) p v where +instance HasSemigroup (SemiValuationAlgebra p q r v set var) p v where semigroup f (SemiValuationAlgebra s p) = fmap (`SemiValuationAlgebra` p) (f s) -instance HasProjectValuation (SemiValuationAlgebra p v set var) p v set var where +instance HasProjectValuation (SemiValuationAlgebra p q r v set var) q r v set var where projectValuation = projectValuation' -- | -- >>> import Data.Functor.Contravariant (contramap) --- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\s v -> v + sum s)) :: SemiValuationAlgebra (->) Int [] Int +-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\s v -> v + sum s)) :: SemiValuationAlgebra (->) (->) (->) Int [] Int -- >>> let SemiValuationAlgebra sg (ProjectValuation p) = contramap (*2) sva -- >>> runSemigroup sg 3 4 -- 7 -- >>> p [1,2,3] 10 -- 22 -instance (Functor set, Profunctor p) => Contravariant (SemiValuationAlgebra p v set) where +instance (Functor set, Profunctor q) => Contravariant (SemiValuationAlgebra p q r v set) where contramap f (SemiValuationAlgebra s p) = SemiValuationAlgebra s (contramap f p) -- | -- >>> import Data.Functor.Contravariant.Divisible (conquer, divide) --- >>> let SemiValuationAlgebra sg (ProjectValuation p) = conquer :: SemiValuationAlgebra (->) [Int] [] Int +-- >>> let SemiValuationAlgebra sg (ProjectValuation p) = conquer :: SemiValuationAlgebra (->) (->) (->) [Int] [] Int -- >>> runSemigroup sg [1,2] [3,4] -- [1,2,3,4] -- >>> p [10,20,30] [42] -- [42] -- -- >>> import Data.Functor.Contravariant.Divisible (conquer, divide) --- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s)) :: SemiValuationAlgebra (->) [Int] [] Int --- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ reverse s)) :: SemiValuationAlgebra (->) [Int] [] Int +-- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s)) :: SemiValuationAlgebra (->) (->) (->) [Int] [] Int +-- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ reverse s)) :: SemiValuationAlgebra (->) (->) (->) [Int] [] Int -- >>> let SemiValuationAlgebra sg (ProjectValuation p) = divide (\x -> (x, x + 10)) sva1 sva2 -- >>> runSemigroup sg [1] [2] -- [1,2] -- >>> p [1,2,3] [0] -- [0,13,12,11,1,2,3] -instance (Functor set, Strong p, Arrow p, Prelude.Semigroup v) => Divisible (SemiValuationAlgebra p v set) where +instance (Functor set, Strong q, Profunctor p, Arrow p, Category q, Category r, Prelude.Semigroup v) => Divisible (SemiValuationAlgebra p q r v set) where conquer = SemiValuationAlgebra (review applySemigroup (rmap arr (arr (<>)))) conquer divide f (SemiValuationAlgebra s p1) (SemiValuationAlgebra _ p2) = SemiValuationAlgebra s (divide f p1 p2) @@ -130,62 +131,65 @@ -- | -- >>> import Data.Functor.Contravariant.Divisible (choose, lose) -- >>> import Data.Void (Void, absurd) --- >>> let SemiValuationAlgebra sg (ProjectValuation p) = lose absurd :: SemiValuationAlgebra (->) [Int] [] Void +-- >>> let SemiValuationAlgebra sg (ProjectValuation p) = lose absurd :: SemiValuationAlgebra (->) (->) (->) [Int] [] Void -- >>> runSemigroup sg [1,2] [3,4] -- [1,2,3,4] -- >>> p [] [42] -- [42] -- -- >>> import Data.Functor.Contravariant.Divisible (choose) --- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s)) :: SemiValuationAlgebra (->) [Int] [] Int --- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ map negate s)) :: SemiValuationAlgebra (->) [Int] [] Int +-- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s)) :: SemiValuationAlgebra (->) (->) (->) [Int] [] Int +-- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ map negate s)) :: SemiValuationAlgebra (->) (->) (->) [Int] [] Int -- >>> let SemiValuationAlgebra sg (ProjectValuation p) = choose (\x -> if even x then Left x else Right x) sva1 sva2 -- >>> runSemigroup sg [1] [2] -- [1,2] -- >>> p [1,2,3,4] [0] -- [0,-1,-3,2,4] -instance (Filterable set, Strong p, Arrow p, Prelude.Semigroup v) => Decidable (SemiValuationAlgebra p v set) where +instance (Filterable set, Strong q, Profunctor p, Arrow p, Category q, Category r, Prelude.Semigroup v) => Decidable (SemiValuationAlgebra p q r v set) where lose f = SemiValuationAlgebra (review applySemigroup (rmap arr (arr (<>)))) (lose f) choose f (SemiValuationAlgebra s p1) (SemiValuationAlgebra _ p2) = SemiValuationAlgebra s (choose f p1 p2) -- | -- >>> import Data.Functor.Contravariant.Divise (divise) --- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s)) :: SemiValuationAlgebra (->) [Int] [] Int --- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ reverse s)) :: SemiValuationAlgebra (->) [Int] [] Int +-- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s)) :: SemiValuationAlgebra (->) (->) (->) [Int] [] Int +-- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ reverse s)) :: SemiValuationAlgebra (->) (->) (->) [Int] [] Int -- >>> let SemiValuationAlgebra sg (ProjectValuation p) = divise (\x -> (x, x + 10)) sva1 sva2 -- >>> runSemigroup sg [1] [2] -- [1,2] -- >>> p [1,2,3] [0] -- [0,13,12,11,1,2,3] -instance (Functor set, Strong p, Semigroupoid p) => Divise (SemiValuationAlgebra p v set) where +instance (Functor set, Strong q, Semigroupoid q, Semigroupoid r) => Divise (SemiValuationAlgebra p q r v set) where divise f (SemiValuationAlgebra s p1) (SemiValuationAlgebra _ p2) = SemiValuationAlgebra s (divise f p1 p2) -- | -- >>> import Data.Functor.Contravariant.Decide (decide) --- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s)) :: SemiValuationAlgebra (->) [Int] [] Int --- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ map negate s)) :: SemiValuationAlgebra (->) [Int] [] Int +-- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s)) :: SemiValuationAlgebra (->) (->) (->) [Int] [] Int +-- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ map negate s)) :: SemiValuationAlgebra (->) (->) (->) [Int] [] Int -- >>> let SemiValuationAlgebra sg (ProjectValuation p) = decide (\x -> if even x then Left x else Right x) sva1 sva2 -- >>> runSemigroup sg [1] [2] -- [1,2] -- >>> p [1,2,3,4] [0] -- [0,-1,-3,2,4] -instance (Filterable set, Strong p, Semigroupoid p) => Decide (SemiValuationAlgebra p v set) where +instance (Filterable set, Strong q, Semigroupoid q, Semigroupoid r) => Decide (SemiValuationAlgebra p q r v set) where decide f (SemiValuationAlgebra s p1) (SemiValuationAlgebra _ p2) = SemiValuationAlgebra s (decide f p1 p2) -- | -- >>> import Data.Functor.Contravariant.Conclude (conclude) -- >>> import Data.Void (absurd) --- >>> let SemiValuationAlgebra sg (ProjectValuation p) = conclude absurd :: SemiValuationAlgebra (->) [Int] [] Void +-- >>> let SemiValuationAlgebra sg (ProjectValuation p) = conclude absurd :: SemiValuationAlgebra (->) (->) (->) [Int] [] Void -- >>> runSemigroup sg [1,2] [3,4] -- [1,2,3,4] -- >>> p [] [42] -- [42] -instance (Filterable set, Strong p, Semigroupoid p, Arrow p, Prelude.Semigroup v) => Conclude (SemiValuationAlgebra p v set) where +instance (Filterable set, Strong q, Semigroupoid q, Category q, Semigroupoid r, Category r, Profunctor p, Arrow p, Prelude.Semigroup v) => Conclude (SemiValuationAlgebra p q r v set) where conclude f = SemiValuationAlgebra (review applySemigroup (rmap arr (arr (<>)))) (conclude f) -- | A 'SemiValuationAlgebra' specialised to 'Set'. -type SetSemiValuationAlgebra p v var = - SemiValuationAlgebra p v Set var +type SetSemiValuationAlgebra p q r v var = + SemiValuationAlgebra p q r v Set var + +type SetSemiValuationAlgebra' v var = + SetSemiValuationAlgebra (->) (->) (->) v var diff --git a/src/Data/Valuation/Semigroup.hs b/src/Data/Valuation/Semigroup.hs --- a/src/Data/Valuation/Semigroup.hs +++ b/src/Data/Valuation/Semigroup.hs @@ -79,6 +79,8 @@ composeG, productF, composeF, + unionSet, + unionIntSet, -- * laws lawAssociative, @@ -112,9 +114,13 @@ ) import Data.Functor.Identity (Identity) import Data.Functor.Product (Product (..)) +import Data.IntSet (IntSet) +import qualified Data.IntSet as IntSet import Data.List.NonEmpty (NonEmpty (..)) import Data.Ord (Down (..)) import Data.Proxy (Proxy (..)) +import Data.Set (Set) +import qualified Data.Set as Set import Data.Tuple (Solo) import Data.Void (Void, absurd) import GHC.Conc (STM) @@ -675,3 +681,51 @@ -- Compose [[1,2],[3,4]] composeF :: Semigroup' (f (g a)) -> Semigroup' (Compose f g a) composeF = mapSemigroup getCompose Compose + +-- | Semigroup on 'Set' via 'Data.Set.union'. +-- +-- >>> import qualified Data.Set as Set +-- >>> runSemigroup unionSet (Set.fromList [1,2]) (Set.fromList [2,3]) :: Set Int +-- fromList [1,2,3] +-- +-- >>> import qualified Data.Set as Set +-- >>> runSemigroup unionSet (Set.fromList [1,2,3]) Set.empty :: Set Int +-- fromList [1,2,3] +-- +-- >>> import qualified Data.Set as Set +-- >>> runSemigroup unionSet Set.empty (Set.fromList [4,5]) :: Set Int +-- fromList [4,5] +-- +-- >>> import qualified Data.Set as Set +-- >>> runSemigroup unionSet (Set.fromList [1,2]) (Set.fromList [1,2]) :: Set Int +-- fromList [1,2] +-- +-- >>> import qualified Data.Set as Set +-- >>> lawAssociative unionSet (Set.fromList [1,2]) (Set.fromList [2,3]) (Set.fromList [3,4 :: Int]) +-- True +unionSet :: (Ord a) => Semigroup' (Set a) +unionSet = review applySemigroup Set.union + +-- | Semigroup on 'IntSet' via 'Data.IntSet.union'. +-- +-- >>> import qualified Data.IntSet as IntSet +-- >>> runSemigroup unionIntSet (IntSet.fromList [1,2]) (IntSet.fromList [2,3]) +-- fromList [1,2,3] +-- +-- >>> import qualified Data.IntSet as IntSet +-- >>> runSemigroup unionIntSet (IntSet.fromList [1,2,3]) IntSet.empty +-- fromList [1,2,3] +-- +-- >>> import qualified Data.IntSet as IntSet +-- >>> runSemigroup unionIntSet IntSet.empty (IntSet.fromList [4,5]) +-- fromList [4,5] +-- +-- >>> import qualified Data.IntSet as IntSet +-- >>> runSemigroup unionIntSet (IntSet.fromList [1,2]) (IntSet.fromList [1,2]) +-- fromList [1,2] +-- +-- >>> import qualified Data.IntSet as IntSet +-- >>> lawAssociative unionIntSet (IntSet.fromList [1,2]) (IntSet.fromList [2,3]) (IntSet.fromList [3,4]) +-- True +unionIntSet :: Semigroup' IntSet +unionIntSet = review applySemigroup IntSet.union diff --git a/src/Data/Valuation/Valuation.hs b/src/Data/Valuation/Valuation.hs --- a/src/Data/Valuation/Valuation.hs +++ b/src/Data/Valuation/Valuation.hs @@ -20,6 +20,20 @@ combineSemiValuation, combineValuation, semigroupValuation, + + -- * laws + lawFunctorIdentity, + lawFunctorComposition, + lawMonadLeftIdentity, + lawMonadRightIdentity, + lawMonadAssociativity, + lawComonadExtractDuplicate, + lawComonadDuplicateExtract, + lawComonadAssociativity, + lawBifunctorIdentity, + lawBifunctorComposition, + lawCombineVarAssociative, + lawCombineVarCommutative, ) where @@ -48,10 +62,10 @@ import Data.Functor.Extend (Extend (..)) import Data.Semigroup.Traversable.Class (Bitraversable1 (..), Traversable1 (..)) import Data.Set (Set) -import Data.Valuation.ProjectValuation (ProjectValuation (..)) -import Data.Valuation.SemiValuationAlgebra (SemiValuationAlgebra (..)) +import Data.Valuation.ProjectValuation (ProjectValuation (..), ProjectValuation') +import Data.Valuation.SemiValuationAlgebra (SemiValuationAlgebra (..), SemiValuationAlgebra') import Data.Valuation.Semigroup (Semigroup', applySemigroup, runSemigroup, semigroup') -import Data.Valuation.ValuationAlgebra (ValuationAlgebra (..)) +import Data.Valuation.ValuationAlgebra (ValuationAlgebra (..), ValuationAlgebra') import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp (..)) import GHC.Generics (Generic, Generic1) import Prelude hiding (Semigroup) @@ -59,6 +73,9 @@ -- $setup -- >>> :set -Wno-name-shadowing -Wno-type-defaults +-- >>> import qualified Data.Set as Set +-- >>> import Control.Lens (review) +-- >>> import Data.Valuation.Semigroup (applySemigroup) -- | -- >>> Valuation [1,2,3] "hello" @@ -467,15 +484,15 @@ Valuation <$> traverse1 f dom <.> g info -- | --- >>> let pv = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) Int [] Int +-- >>> let pv = ProjectValuation (\s v -> v + sum s) :: ProjectValuation (->) (->) Int [] Int -- >>> projectVar pv (Valuation [1,2,3] 10) -- 16 -- --- >>> let pv = ProjectValuation (\s v -> v * length s) :: ProjectValuation (->) Int [] Int +-- >>> let pv = ProjectValuation (\s v -> v * length s) :: ProjectValuation (->) (->) Int [] Int -- >>> projectVar pv (Valuation [1,2,3] 5) -- 15 projectVar :: - ProjectValuation (->) v set var -> + ProjectValuation' v set var -> Valuation set var v -> v projectVar (ProjectValuation p) (Valuation dom info) = @@ -501,18 +518,18 @@ -- | -- >>> import Control.Lens (review) -- >>> import qualified Data.Valuation.Semigroup as S --- >>> let sva = SemiValuationAlgebra (review S.applySemigroup (+)) (ProjectValuation (\s v -> v + sum s)) :: SemiValuationAlgebra (->) Int [] Int +-- >>> let sva = SemiValuationAlgebra (review S.applySemigroup (+)) (ProjectValuation (\s v -> v + sum s)) :: SemiValuationAlgebra (->) (->) (->) Int [] Int -- >>> combineSemiValuation S.list sva (Valuation [1,2] 10) (Valuation [3,4] 20) -- Valuation [1,2,3,4] 40 -- -- >>> import Control.Lens (review) -- >>> import qualified Data.Valuation.Semigroup as S --- >>> let sva = SemiValuationAlgebra (review S.applySemigroup (*)) (ProjectValuation (\s v -> v + length s)) :: SemiValuationAlgebra (->) Int [] Int +-- >>> let sva = SemiValuationAlgebra (review S.applySemigroup (*)) (ProjectValuation (\s v -> v + length s)) :: SemiValuationAlgebra (->) (->) (->) Int [] Int -- >>> combineSemiValuation S.list sva (Valuation [1,2] 3) (Valuation [3] 4) -- Valuation [1,2,3] 15 combineSemiValuation :: Semigroup' (set var) -> - SemiValuationAlgebra (->) v set var -> + SemiValuationAlgebra' v set var -> Valuation set var v -> Valuation set var v -> Valuation set var v @@ -525,7 +542,7 @@ -- >>> import qualified Data.Valuation.Semigroup as S -- >>> let sva = SemiValuationAlgebra (review S.applySemigroup (+)) (ProjectValuation (\s v -> v + sum s)) -- >>> import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp(..)) --- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp sum) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) Int [] Int +-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp sum) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int [] Int -- >>> combineValuation S.list va (Valuation [1,2] 10) (Valuation [3,4] 20) -- Valuation [1,2,3,4] 50 -- @@ -533,12 +550,12 @@ -- >>> import qualified Data.Valuation.Semigroup as S -- >>> let sva = SemiValuationAlgebra (review S.applySemigroup (*)) (ProjectValuation (\s v -> v + length s)) -- >>> import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp(..)) --- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 1)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) Int [] Int +-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 1)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int [] Int -- >>> combineValuation S.list va (Valuation [1,2] 3) (Valuation [3] 4) -- Valuation [1,2,3] 15 combineValuation :: Semigroup' (set var) -> - ValuationAlgebra (->) v set var -> + ValuationAlgebra' v set var -> Valuation set var v -> Valuation set var v -> Valuation set var v @@ -579,3 +596,180 @@ Semigroup' (Valuation set var a) semigroupValuation sd sa = review applySemigroup (\(Valuation d1 a1) (Valuation d2 a2) -> Valuation (runSemigroup sd d1 d2) (runSemigroup sa a1 a2)) + +-- | Functor identity law: @fmap id v == v@. +-- +-- >>> lawFunctorIdentity (Valuation [1,2,3] "hello" :: Valuation [] Int String) +-- True +-- +-- >>> lawFunctorIdentity (Valuation [1] (42 :: Int) :: Valuation [] Int Int) +-- True +lawFunctorIdentity :: (Eq (set var), Eq a) => Valuation set var a -> Bool +lawFunctorIdentity v = + fmap id v == v + +-- | Functor composition law: @fmap (f . g) v == fmap f (fmap g v)@. +-- +-- >>> lawFunctorComposition length show (Valuation [1,2] (42 :: Int) :: Valuation [] Int Int) +-- True +-- +-- >>> lawFunctorComposition (*2) (+1) (Valuation [1,2,3] 10 :: Valuation [] Int Int) +-- True +lawFunctorComposition :: (Eq (set var), Eq c) => (b -> c) -> (a -> b) -> Valuation set var a -> Bool +lawFunctorComposition f g v = + fmap (f . g) v == fmap f (fmap g v) + +-- | Monad left identity law: @return a >>= f == f a@. +-- +-- >>> lawMonadLeftIdentity 42 (\x -> Valuation [x] (show x)) :: Bool +-- True +-- +-- >>> lawMonadLeftIdentity "hi" (\s -> Valuation [length s] s) :: Bool +-- True +lawMonadLeftIdentity :: (Eq (set var), Eq b, Monoid (set var)) => a -> (a -> Valuation set var b) -> Bool +lawMonadLeftIdentity a f = + (return a >>= f) == f a + +-- | Monad right identity law: @m >>= return == m@. +-- +-- >>> lawMonadRightIdentity (Valuation [1,2,3] "hello" :: Valuation [] Int String) +-- True +-- +-- >>> lawMonadRightIdentity (Valuation [] (42 :: Int) :: Valuation [] Int Int) +-- True +lawMonadRightIdentity :: (Eq (set var), Eq a, Monoid (set var)) => Valuation set var a -> Bool +lawMonadRightIdentity m = + (m >>= return) == m + +-- | Monad associativity law: @(m >>= f) >>= g == m >>= (\\x -> f x >>= g)@. +-- +-- >>> let f x = Valuation [x] (show x) :: Valuation [] Int String +-- >>> let g s = Valuation [length s] s +-- >>> lawMonadAssociativity (Valuation [0] (42 :: Int)) f g +-- True +-- +-- >>> let f x = Valuation [1] (x * 2) :: Valuation [] Int Int +-- >>> let g x = Valuation [2] (x + 1) +-- >>> lawMonadAssociativity (Valuation [0] 10 :: Valuation [] Int Int) f g +-- True +lawMonadAssociativity :: (Eq (set var), Eq c, Monoid (set var)) => Valuation set var a -> (a -> Valuation set var b) -> (b -> Valuation set var c) -> Bool +lawMonadAssociativity m f g = + ((m >>= f) >>= g) == (m >>= (\x -> f x >>= g)) + +-- | Comonad left identity law: @extract (duplicate v) == v@. +-- +-- >>> lawComonadExtractDuplicate (Valuation [1,2] "hello" :: Valuation [] Int String) +-- True +-- +-- >>> lawComonadExtractDuplicate (Valuation [] (42 :: Int) :: Valuation [] Int Int) +-- True +lawComonadExtractDuplicate :: (Eq (set var), Eq a) => Valuation set var a -> Bool +lawComonadExtractDuplicate v = + extract (duplicate v) == v + +-- | Comonad right identity law: @fmap extract (duplicate v) == v@. +-- +-- >>> lawComonadDuplicateExtract (Valuation [1,2] "hello" :: Valuation [] Int String) +-- True +-- +-- >>> lawComonadDuplicateExtract (Valuation [1] (42 :: Int) :: Valuation [] Int Int) +-- True +lawComonadDuplicateExtract :: (Eq (set var), Eq a) => Valuation set var a -> Bool +lawComonadDuplicateExtract v = + fmap extract (duplicate v) == v + +-- | Comonad associativity law: @duplicate (duplicate v) == fmap duplicate (duplicate v)@. +-- +-- >>> lawComonadAssociativity (Valuation [1,2] "hello" :: Valuation [] Int String) +-- True +-- +-- >>> lawComonadAssociativity (Valuation [1] (42 :: Int) :: Valuation [] Int Int) +-- True +lawComonadAssociativity :: (Eq (set var), Eq a) => Valuation set var a -> Bool +lawComonadAssociativity v = + duplicate (duplicate v) == fmap duplicate (duplicate v) + +-- | Bifunctor identity law: @bimap id id v == v@. +-- +-- >>> lawBifunctorIdentity (Valuation [1,2,3] "hello" :: Valuation [] Int String) +-- True +-- +-- >>> lawBifunctorIdentity (Valuation [1] (42 :: Int) :: Valuation [] Int Int) +-- True +lawBifunctorIdentity :: (Functor set, Eq (set var), Eq a) => Valuation set var a -> Bool +lawBifunctorIdentity v = + bimap id id v == v + +-- | Bifunctor composition law: +-- @bimap f1 g1 (bimap f2 g2 v) == bimap (f1 . f2) (g1 . g2) v@. +-- +-- >>> lawBifunctorComposition (*2) length (+1) show (Valuation [1,2,3] (42 :: Int) :: Valuation [] Int Int) +-- True +-- +-- >>> lawBifunctorComposition negate reverse (+1) (:[]) (Valuation [1,2] 'a' :: Valuation [] Int Char) +-- True +lawBifunctorComposition :: + (Functor set, Eq (set var''), Eq c) => + (var' -> var'') -> + (b -> c) -> + (var -> var') -> + (a -> b) -> + Valuation set var a -> + Bool +lawBifunctorComposition f1 g1 f2 g2 v = + bimap f1 g1 (bimap f2 g2 v) == bimap (f1 . f2) (g1 . g2) v + +-- | Associativity of 'combineVar': given two 'Semigroup''s, +-- @combineVar sd sv (combineVar sd sv a b) c == combineVar sd sv a (combineVar sd sv b c)@. +-- +-- >>> import qualified Data.Valuation.Semigroup as S +-- >>> let a = Valuation [1] 10 :: Valuation [] Int Int +-- >>> let b = Valuation [2] 20 +-- >>> let c = Valuation [3] 30 +-- >>> lawCombineVarAssociative S.list S.sum a b c +-- True +-- +-- >>> import qualified Data.Valuation.Semigroup as S +-- >>> let a = Valuation [1] 2 :: Valuation [] Int Int +-- >>> let b = Valuation [2] 3 +-- >>> let c = Valuation [3] 4 +-- >>> lawCombineVarAssociative S.list S.product a b c +-- True +lawCombineVarAssociative :: + (Eq (set var), Eq v) => + Semigroup' (set var) -> + Semigroup' v -> + Valuation set var v -> + Valuation set var v -> + Valuation set var v -> + Bool +lawCombineVarAssociative sd sv a b c = + combineVar sd sv (combineVar sd sv a b) c == combineVar sd sv a (combineVar sd sv b c) + +-- | Commutativity of 'combineVar': given two commutative 'Semigroup''s, +-- @combineVar sd sv a b == combineVar sd sv b a@. +-- +-- The caller should ensure the semigroups are commutative; this function +-- tests whether the property holds for the given inputs. +-- +-- >>> import qualified Data.Valuation.Semigroup as S +-- >>> let a = Valuation [1] 10 :: Valuation [] Int Int +-- >>> let b = Valuation [2] 20 +-- >>> lawCombineVarCommutative S.list S.sum a b +-- False +-- +-- >>> import qualified Data.Valuation.Semigroup as S +-- >>> import qualified Data.Set as Set +-- >>> let a = Valuation (Set.fromList [1]) 10 :: Valuation Set Int Int +-- >>> let b = Valuation (Set.fromList [2]) 20 +-- >>> lawCombineVarCommutative (review applySemigroup Set.union) S.sum a b +-- True +lawCombineVarCommutative :: + (Eq (set var), Eq v) => + Semigroup' (set var) -> + Semigroup' v -> + Valuation set var v -> + Valuation set var v -> + Bool +lawCombineVarCommutative sd sv a b = + combineVar sd sv a b == combineVar sd sv b a diff --git a/src/Data/Valuation/ValuationAlgebra.hs b/src/Data/Valuation/ValuationAlgebra.hs --- a/src/Data/Valuation/ValuationAlgebra.hs +++ b/src/Data/Valuation/ValuationAlgebra.hs @@ -7,6 +7,7 @@ ( ValuationAlgebra (..), ValuationAlgebra', SetValuationAlgebra, + SetValuationAlgebra', -- * optics HasValuationAlgebra (..), @@ -47,7 +48,7 @@ -- >>> import Control.Lens (review) -- >>> import Data.Valuation.Semigroup (Semigroup, applySemigroup, runSemigroup) -- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\s v -> v + sum s)) --- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp sum) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) Int [] Int +-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp sum) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int [] Int -- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = va -- >>> runSemigroup sg 3 4 -- 7 @@ -57,44 +58,44 @@ -- 6 -- >>> z [1,2,3] -- 0 -data ValuationAlgebra p v set var +data ValuationAlgebra p q r v set var = ValuationAlgebra - (SemiValuationAlgebra p v set var) + (SemiValuationAlgebra p q r v set var) -- | algebra unit (ValuationAlgebraOp p set var v) -- | algebra zero (ValuationAlgebraOp p set var v) type ValuationAlgebra' v set var = - ValuationAlgebra (->) v set var + ValuationAlgebra (->) (->) (->) v set var -- | Classy lens for types that contain a 'ValuationAlgebra'. -class HasValuationAlgebra c p v set var | c -> p v set var where - valuationAlgebra :: Lens' c (ValuationAlgebra p v set var) +class HasValuationAlgebra c p q r v set var | c -> p q r v set var where + valuationAlgebra :: Lens' c (ValuationAlgebra p q r v set var) valuationAlgebraUnit :: Lens' c (ValuationAlgebraOp p set var v) valuationAlgebraUnit = valuationAlgebra . valuationAlgebraUnit valuationAlgebraZero :: Lens' c (ValuationAlgebraOp p set var v) valuationAlgebraZero = valuationAlgebra . valuationAlgebraZero -instance HasValuationAlgebra (ValuationAlgebra p v set var) p v set var where +instance HasValuationAlgebra (ValuationAlgebra p q r v set var) p q r v set var where valuationAlgebra = id valuationAlgebraUnit f (ValuationAlgebra s u z) = fmap (\u' -> ValuationAlgebra s u' z) (f u) valuationAlgebraZero f (ValuationAlgebra s u z) = fmap (ValuationAlgebra s u) (f z) -- | Classy prism for types that can be constructed from a 'ValuationAlgebra'. -class AsValuationAlgebra c p v set var | c -> p v set var where - _ValuationAlgebra :: Prism' c (ValuationAlgebra p v set var) +class AsValuationAlgebra c p q r v set var | c -> p q r v set var where + _ValuationAlgebra :: Prism' c (ValuationAlgebra p q r v set var) -instance AsValuationAlgebra (ValuationAlgebra p v set var) p v set var where +instance AsValuationAlgebra (ValuationAlgebra p q r v set var) p q r v set var where _ValuationAlgebra = id -instance HasSemiValuationAlgebra (ValuationAlgebra p v set var) p v set var where +instance HasSemiValuationAlgebra (ValuationAlgebra p q r v set var) p q r v set var where semiValuationAlgebra f (ValuationAlgebra a u z) = fmap (\a' -> ValuationAlgebra a' u z) (f a) -instance HasSemigroup (ValuationAlgebra p v set var) p v where +instance HasSemigroup (ValuationAlgebra p q r v set var) p v where semigroup = semiValuationAlgebra . semigroup -instance HasProjectValuation (ValuationAlgebra p v set var) p v set var where +instance HasProjectValuation (ValuationAlgebra p q r v set var) q r v set var where projectValuation = semiValuationAlgebra . projectValuation -- | @@ -105,7 +106,7 @@ -- >>> import Control.Lens (review) -- >>> import Data.Valuation.Semigroup (Semigroup, applySemigroup, runSemigroup) -- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\s v -> v + sum s)) --- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp sum) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) Int [] Int +-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp sum) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int [] Int -- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = contramap (*2) va -- >>> runSemigroup sg 3 4 -- 7 @@ -115,7 +116,7 @@ -- 12 -- >>> z [1,2,3] -- 0 -instance (Profunctor p, Functor set) => Contravariant (ValuationAlgebra p v set) where +instance (Profunctor p, Profunctor q, Functor set) => Contravariant (ValuationAlgebra p q r v set) where contramap f (ValuationAlgebra s (ValuationAlgebraOp u) (ValuationAlgebraOp z)) = ValuationAlgebra (contramap f s) (ValuationAlgebraOp (lmap (fmap f) u)) (ValuationAlgebraOp (lmap (fmap f) z)) @@ -126,7 +127,7 @@ -- >>> import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp(..)) -- >>> import Control.Lens (review) -- >>> import Data.Valuation.Semigroup (Semigroup, applySemigroup, runSemigroup) --- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = conquer :: ValuationAlgebra (->) [Int] [] Int +-- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = conquer :: ValuationAlgebra (->) (->) (->) [Int] [] Int -- >>> runSemigroup sg [1] [2] -- [1,2] -- >>> p [10,20] [42] @@ -143,9 +144,9 @@ -- >>> import Control.Lens (review) -- >>> import Data.Valuation.Semigroup (Semigroup, applySemigroup, runSemigroup) -- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s)) --- >>> let va1 = ValuationAlgebra sva1 (ValuationAlgebraOp id) (ValuationAlgebraOp (map negate)) :: ValuationAlgebra (->) [Int] [] Int +-- >>> let va1 = ValuationAlgebra sva1 (ValuationAlgebraOp id) (ValuationAlgebraOp (map negate)) :: ValuationAlgebra (->) (->) (->) [Int] [] Int -- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ reverse s)) --- >>> let va2 = ValuationAlgebra sva2 (ValuationAlgebraOp reverse) (ValuationAlgebraOp (const [])) :: ValuationAlgebra (->) [Int] [] Int +-- >>> let va2 = ValuationAlgebra sva2 (ValuationAlgebraOp reverse) (ValuationAlgebraOp (const [])) :: ValuationAlgebra (->) (->) (->) [Int] [] Int -- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = divide (\x -> (x, x + 10)) va1 va2 -- >>> runSemigroup sg [1] [2] -- [1,2] @@ -153,7 +154,7 @@ -- [1,2,3,13,12,11] -- >>> z [1,2,3] -- [-1,-2,-3] -instance (Functor set, Strong p, Arrow p, Prelude.Semigroup v, Prelude.Monoid v) => Divisible (ValuationAlgebra p v set) where +instance (Functor set, Strong p, Strong q, Arrow p, Category q, Category r, Prelude.Semigroup v, Prelude.Monoid v) => Divisible (ValuationAlgebra p q r v set) where conquer = ValuationAlgebra conquer (ValuationAlgebraOp (rmap (const mempty) id)) (ValuationAlgebraOp (rmap (const mempty) id)) divide f (ValuationAlgebra s1 (ValuationAlgebraOp u1) (ValuationAlgebraOp z1)) (ValuationAlgebra s2 (ValuationAlgebraOp u2) (ValuationAlgebraOp z2)) = let combine g1 g2 = @@ -170,7 +171,7 @@ -- >>> import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp(..)) -- >>> import Control.Lens (review) -- >>> import Data.Valuation.Semigroup (Semigroup, applySemigroup, runSemigroup) --- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = lose absurd :: ValuationAlgebra (->) [Int] [] Void +-- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = lose absurd :: ValuationAlgebra (->) (->) (->) [Int] [] Void -- >>> runSemigroup sg [1] [2] -- [1,2] -- >>> p [] [42] @@ -187,9 +188,9 @@ -- >>> import Control.Lens (review) -- >>> import Data.Valuation.Semigroup (Semigroup, applySemigroup, runSemigroup) -- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s)) --- >>> let va1 = ValuationAlgebra sva1 (ValuationAlgebraOp id) (ValuationAlgebraOp (map negate)) :: ValuationAlgebra (->) [Int] [] Int +-- >>> let va1 = ValuationAlgebra sva1 (ValuationAlgebraOp id) (ValuationAlgebraOp (map negate)) :: ValuationAlgebra (->) (->) (->) [Int] [] Int -- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ reverse s)) --- >>> let va2 = ValuationAlgebra sva2 (ValuationAlgebraOp reverse) (ValuationAlgebraOp (const [])) :: ValuationAlgebra (->) [Int] [] Int +-- >>> let va2 = ValuationAlgebra sva2 (ValuationAlgebraOp reverse) (ValuationAlgebraOp (const [])) :: ValuationAlgebra (->) (->) (->) [Int] [] Int -- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = choose (\x -> if even x then Left x else Right x) va1 va2 -- >>> runSemigroup sg [1] [2] -- [1,2] @@ -197,7 +198,7 @@ -- [2,4,3,1] -- >>> z [1,2,3,4] -- [-2,-4] -instance (Filterable set, Strong p, Arrow p, Prelude.Semigroup v, Prelude.Monoid v) => Decidable (ValuationAlgebra p v set) where +instance (Filterable set, Strong p, Strong q, Arrow p, Category q, Category r, Prelude.Semigroup v, Prelude.Monoid v) => Decidable (ValuationAlgebra p q r v set) where lose f = ValuationAlgebra (lose f) (ValuationAlgebraOp (rmap (const mempty) id)) (ValuationAlgebraOp (rmap (const mempty) id)) choose ch (ValuationAlgebra s1 (ValuationAlgebraOp u1) (ValuationAlgebraOp z1)) (ValuationAlgebra s2 (ValuationAlgebraOp u2) (ValuationAlgebraOp z2)) = let lefts = mapMaybe (either Just (const Nothing) . ch) @@ -216,9 +217,9 @@ -- >>> import Control.Lens (review) -- >>> import Data.Valuation.Semigroup (Semigroup, applySemigroup, runSemigroup) -- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s)) --- >>> let va1 = ValuationAlgebra sva1 (ValuationAlgebraOp id) (ValuationAlgebraOp (map negate)) :: ValuationAlgebra (->) [Int] [] Int +-- >>> let va1 = ValuationAlgebra sva1 (ValuationAlgebraOp id) (ValuationAlgebraOp (map negate)) :: ValuationAlgebra (->) (->) (->) [Int] [] Int -- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ reverse s)) --- >>> let va2 = ValuationAlgebra sva2 (ValuationAlgebraOp reverse) (ValuationAlgebraOp (const [])) :: ValuationAlgebra (->) [Int] [] Int +-- >>> let va2 = ValuationAlgebra sva2 (ValuationAlgebraOp reverse) (ValuationAlgebraOp (const [])) :: ValuationAlgebra (->) (->) (->) [Int] [] Int -- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = divise (\x -> (x, x + 10)) va1 va2 -- >>> runSemigroup sg [1] [2] -- [1,2] @@ -226,7 +227,7 @@ -- [1,2,3,13,12,11] -- >>> z [1,2,3] -- [-1,-2,-3] -instance (Functor set, Strong p, Semigroupoid p, Prelude.Semigroup v) => Divise (ValuationAlgebra p v set) where +instance (Functor set, Strong p, Semigroupoid p, Strong q, Semigroupoid q, Semigroupoid r, Prelude.Semigroup v) => Divise (ValuationAlgebra p q r v set) where divise f (ValuationAlgebra s1 (ValuationAlgebraOp u1) (ValuationAlgebraOp z1)) (ValuationAlgebra s2 (ValuationAlgebraOp u2) (ValuationAlgebraOp z2)) = let combine g1 g2 = let g1' = lmap (fmap (fst . f)) g1 @@ -242,9 +243,9 @@ -- >>> import Control.Lens (review) -- >>> import Data.Valuation.Semigroup (Semigroup, applySemigroup, runSemigroup) -- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s)) --- >>> let va1 = ValuationAlgebra sva1 (ValuationAlgebraOp id) (ValuationAlgebraOp (map negate)) :: ValuationAlgebra (->) [Int] [] Int +-- >>> let va1 = ValuationAlgebra sva1 (ValuationAlgebraOp id) (ValuationAlgebraOp (map negate)) :: ValuationAlgebra (->) (->) (->) [Int] [] Int -- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ reverse s)) --- >>> let va2 = ValuationAlgebra sva2 (ValuationAlgebraOp reverse) (ValuationAlgebraOp (const [])) :: ValuationAlgebra (->) [Int] [] Int +-- >>> let va2 = ValuationAlgebra sva2 (ValuationAlgebraOp reverse) (ValuationAlgebraOp (const [])) :: ValuationAlgebra (->) (->) (->) [Int] [] Int -- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = decide (\x -> if even x then Left x else Right x) va1 va2 -- >>> runSemigroup sg [1] [2] -- [1,2] @@ -252,7 +253,7 @@ -- [2,4,3,1] -- >>> z [1,2,3,4] -- [-2,-4] -instance (Filterable set, Strong p, Semigroupoid p, Prelude.Semigroup v) => Decide (ValuationAlgebra p v set) where +instance (Filterable set, Strong p, Semigroupoid p, Strong q, Semigroupoid q, Semigroupoid r, Prelude.Semigroup v) => Decide (ValuationAlgebra p q r v set) where decide ch (ValuationAlgebra s1 (ValuationAlgebraOp u1) (ValuationAlgebraOp z1)) (ValuationAlgebra s2 (ValuationAlgebraOp u2) (ValuationAlgebraOp z2)) = let lefts = mapMaybe (either Just (const Nothing) . ch) rights = mapMaybe (either (const Nothing) Just . ch) @@ -270,16 +271,19 @@ -- >>> import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp(..)) -- >>> import Control.Lens (review) -- >>> import Data.Valuation.Semigroup (Semigroup, applySemigroup, runSemigroup) --- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = conclude absurd :: ValuationAlgebra (->) [Int] [] Void +-- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = conclude absurd :: ValuationAlgebra (->) (->) (->) [Int] [] Void -- >>> runSemigroup sg [1] [2] -- [1,2] -- >>> u [] -- [] -- >>> z [] -- [] -instance (Filterable set, Strong p, Semigroupoid p, Arrow p, Prelude.Semigroup v, Prelude.Monoid v) => Conclude (ValuationAlgebra p v set) where +instance (Filterable set, Strong p, Semigroupoid p, Arrow p, Strong q, Semigroupoid q, Category q, Semigroupoid r, Category r, Prelude.Semigroup v, Prelude.Monoid v) => Conclude (ValuationAlgebra p q r v set) where conclude f = ValuationAlgebra (conclude f) (ValuationAlgebraOp (rmap (const mempty) id)) (ValuationAlgebraOp (rmap (const mempty) id)) -- | A 'ValuationAlgebra' specialised to 'Set'. -type SetValuationAlgebra p v var = - ValuationAlgebra p v Set var +type SetValuationAlgebra p q r v var = + ValuationAlgebra p q r v Set var + +type SetValuationAlgebra' v var = + SetValuationAlgebra (->) (->) (->) v var diff --git a/src/Data/Valuation/ValuationAlgebraOp.hs b/src/Data/Valuation/ValuationAlgebraOp.hs --- a/src/Data/Valuation/ValuationAlgebraOp.hs +++ b/src/Data/Valuation/ValuationAlgebraOp.hs @@ -92,7 +92,7 @@ _ValuationAlgebraOp = Prelude.id -- | Iso between a 'ValuationAlgebraOp' producing an endomorphism and a 'ProjectValuation'. -valuationAlgebraOpProjectValuation :: Iso (ValuationAlgebraOp p set var (p v v)) (ValuationAlgebraOp p' set' var' (p' v' v')) (ProjectValuation p v set var) (ProjectValuation p' v' set' var') +valuationAlgebraOpProjectValuation :: Iso (ValuationAlgebraOp p set var (q v v)) (ValuationAlgebraOp p' set' var' (q' v' v')) (ProjectValuation p q v set var) (ProjectValuation p' q' v' set' var') valuationAlgebraOpProjectValuation = iso (\(ValuationAlgebraOp k) -> ProjectValuation k) diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,15 @@ +{-# OPTIONS_GHC -Wall -Werror -Wno-orphans #-} + +module Main where + +import System.Exit (exitWith) +import System.Process (rawSystem) + +main :: IO () +main = exitWith =<< rawSystem "cabal" + [ "repl" + , "--with-compiler=doctest" + , "--repl-options=-w" + , "--repl-options=-Wdefault" + , "lib:valuations" + ] diff --git a/valuations.cabal b/valuations.cabal --- a/valuations.cabal +++ b/valuations.cabal @@ -1,16 +1,16 @@ +cabal-version: 2.4 name: valuations -version: 0.0.3 +version: 0.0.4 synopsis: Valuations description: Valuations: Valuation and Valuation Algebra -license: BSD3 +license: BSD-3-Clause license-file: LICENCE author: Tony Morris <ʇǝu˙sıɹɹoɯʇ@ןןǝʞsɐɥ> maintainer: Tony Morris <ʇǝu˙sıɹɹoɯʇ@ןןǝʞsɐɥ> copyright: Copyright (C) 2026 Tony Morris -category: Test +category: Math build-type: Simple -extra-source-files: changelog.md -cabal-version: >=1.10 +extra-doc-files: changelog.md homepage: https://gitlab.com/tonymorris/valuations bug-reports: https://gitlab.com/tonymorris/valuations/issues tested-with: GHC == 9.6.7 @@ -22,9 +22,11 @@ library exposed-modules: Data.Valuation - Data.Valuation.BinaryFunction + Data.Valuation.CovariantFunctor Data.Valuation.DomainLattice Data.Valuation.PartialOrder + Data.Valuation.Poset + Data.Valuation.Presheaf Data.Valuation.PresheafValuationAlgebra Data.Valuation.ProjectValuation Data.Valuation.Semigroup @@ -51,4 +53,14 @@ default-language: Haskell2010 + ghc-options: -Wall + +test-suite doctest + type: exitcode-stdio-1.0 + hs-source-dirs: test + main-is: Main.hs + build-depends: base >= 4.8 && < 6 + , process >= 1 && < 2 + build-tool-depends: doctest:doctest >= 0.22 + default-language: Haskell2010 ghc-options: -Wall