packages feed

monoid-semiring-0.1.0.0: test/OrdContract.hs

-- | The @Ord m@ contract of the core, executable (haddock of
-- "Data.MonoidSemiring", section "The role of @Ord m@"). The claim
-- splits the API in two halves, each with its own witness:
--
-- * /invariance/: re-keying a value between two orders on the same
--   carrier commutes with the algebra — QuickCheck properties;
-- * /observability/: 'toList' and 'support' reflect the order — one
--   value, two orders, two supports.
module OrdContract
  ( Rev (..)
  , reKey
  , invarianceLaws
  , witnessValue
  , observedSupport
  , observedSupportRev
  ) where

import           Data.Monoid     (Sum (..))
import           Numeric.Natural (Natural)
import           Test.QuickCheck

import           Data.MonoidSemiring
import           Data.Semiring (Semiring (..))

-- SNIPPET:rekey
-- | The same carrier under the opposite order: the monoid is unchanged,
-- only 'compare' flips.
newtype Rev = Rev { unRev :: Sum Natural }
  deriving (Eq, Show)

instance Ord Rev where compare (Rev a) (Rev b) = compare b a

instance Semigroup Rev where Rev a <> Rev b = Rev (a <> b)
instance Monoid    Rev where mempty = Rev mempty

-- | Transport along the identity of carriers, between the two orders.
reKey :: (Semiring s, Eq s)
      => MonoidSemiring (Sum Natural) s -> MonoidSemiring Rev s
reKey = fromList . map (\(m, c) -> (Rev m, c)) . toList
-- END:rekey

-- SNIPPET:ord-invariance
-- The algebra cannot tell the two orders apart: re-keying commutes
-- with every algebraic operation.
invarianceLaws :: Gen (MonoidSemiring (Sum Natural) Integer)
               -> Gen (Sum Natural)
               -> [(String, Property)]
invarianceLaws g gm =
  [ ("rekey-plus",  p2 (\f h -> reKey (f `plus` h)  == reKey f `plus` reKey h))
  , ("rekey-times", p2 (\f h -> reKey (f `times` h) == reKey f `times` reKey h))
  , ("rekey-coefficient",
      forAll g (\f -> forAll gm (\m ->
        coefficient (Rev m) (reKey f) == coefficient m f)))
  ]
  where p2 f = forAll g (\a -> forAll g (f a))
-- END:ord-invariance

-- SNIPPET:ord-observable
-- The observations can: the same value, x + x^2, enumerates its
-- support ascending — which list that is depends on the order.
witnessValue :: MonoidSemiring (Sum Natural) Integer
witnessValue = fromList [(Sum 1, 1), (Sum 2, 1)]

observedSupport :: [Natural]                  -- [1, 2]
observedSupport = map getSum (support witnessValue)

observedSupportRev :: [Natural]               -- [2, 1]
observedSupportRev = map (getSum . unRev) (support (reKey witnessValue))
-- END:ord-observable