{-# LANGUAGE FlexibleInstances, TupleSections, TypeApplications #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Laws where
import Control.Arrow hiding (first, second)
import qualified Control.Monad.Trans.Except as Transformers
import Control.Monad.Trans.Writer
import Control.Selective
import Control.Selective.Trans.Except
import Data.Bifunctor (bimap, first, second)
import Data.Function
import Data.Functor.Identity
import Test.QuickCheck hiding (Failure, Success)
import Text.Show.Functions()
-- | TODO:
-- ifS (pure x) a1 b1 *> ifS (pure x) a2 b2 = ifS (pure x) (a1 *> a2) (b1 *> b2)
--------------------------------------------------------------------------------
------------------------ Laws --------------------------------------------------
--------------------------------------------------------------------------------
-- | Identity
lawIdentity :: (Selective f, Eq (f a)) => f (Either a a) -> Bool
lawIdentity x = (x <*? pure id) == (either id id <$> x)
-- | Distributivity
lawDistributivity :: (Selective f, Eq (f b)) => Either a b -> f (a -> b) -> f (a -> b) -> Bool
lawDistributivity x y z = (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))
-- | Associativity
lawAssociativity :: (Selective f, Eq (f c)) =>
f (Either b c) -> f (Either a (b -> c)) -> f (a -> b -> c) -> Bool
lawAssociativity x y z =
(x <*? (y <*? z)) == ((f <$> x) <*? (g <$> y) <*? (h <$> z))
where
f = fmap Right
g y a = bimap (,a) ($a) y
h = uncurry
{- | If 'f' is a 'Monad' |-}
lawMonad :: (Selective f, Monad f, Eq (f b)) => f (Either a b) -> f (a -> b) -> Bool
lawMonad x f = select x f == selectM x f
selectALaw :: (Selective f, Eq (f b)) => f (Either a b) -> f (a -> b) -> Bool
selectALaw x f = select x f == selectA x f
--------------------------------------------------------------------------------
------------------------ Theorems ----------------------------------------------
--------------------------------------------------------------------------------
{-| Theorems about selective applicative functors, see Fig. 4 of the paper |-}
-- | Apply a pure function to the result:
theorem1 :: (Selective f, Eq (f c)) => (a -> c) -> f (Either b a) -> f (b -> a) -> Bool
theorem1 f x y = (f <$> select x y) == select (second f <$> x) ((f .) <$> y)
-- | Apply a pure function to the Left case of the first argument:
theorem2 :: (Selective f, Eq (f c)) => (a -> b) -> f (Either a c) -> f (b -> c) -> Bool
theorem2 f x y = select (first f <$> x) y == select x ((. f) <$> y)
-- | Apply a pure function to the second argument:
theorem3 :: (Selective f, Eq (f c)) => (a -> b -> c) -> f (Either b c) -> f a -> Bool
theorem3 f x y = select x (f <$> y) == select (first (flip f) <$> x) ((&) <$> y)
-- | Generalised identity:
theorem4 :: (Selective f, Eq (f b)) => f (Either a b) -> (a -> b) -> Bool
theorem4 x y = (x <*? pure y) == (either y id <$> x)
{-| For rigid selective functors (in particular, for monads) |-}
-- | Selective apply
theorem5 :: (Selective f, Eq (f b)) => f (a -> b) -> f a -> Bool
theorem5 f g = (f <*> g) == (f `apS` g)
-- | Interchange
theorem6 :: (Selective f, Eq (f c)) => f a -> f (Either b c) -> f (b -> c) -> Bool
theorem6 x y z = (x *> (y <*? z)) == ((x *> y) <*? z)
--------------------------------------------------------------------------------
------------------------ Properties ----------------------------------------------
--------------------------------------------------------------------------------
-- | Pure-Right: pure (Right x) <*? y = pure x
propertyPureRight :: (Selective f, Eq (f a)) => a -> f (b -> a) -> Bool
propertyPureRight x y = (pure (Right x) <*? y) == pure x
-- | Pure-Left: pure (Left x) <*? y = ($x) <$> y
propertyPureLeft :: (Selective f, Eq (f b)) => a -> f (a -> b) -> Bool
propertyPureLeft x y = (pure (Left x) <*? y) == (($x) <$> y)
--------------------------------------------------------------------------------
------------------------ Over --------------------------------------------------
--------------------------------------------------------------------------------
instance Arbitrary a => Arbitrary (Over a b) where
arbitrary = Over <$> arbitrary
shrink = map Over . shrink . getOver
propertyPureRightOver :: IO ()
propertyPureRightOver = quickCheck (propertyPureRight @(Over String) @Int)
--------------------------------------------------------------------------------
------------------------ Under -------------------------------------------------
--------------------------------------------------------------------------------
instance Arbitrary a => Arbitrary (Under a b) where
arbitrary = Under <$> arbitrary
shrink = map Under . shrink . getUnder
propertyPureRightUnder :: IO ()
propertyPureRightUnder = quickCheck (propertyPureRight @(Under String) @Int)
--------------------------------------------------------------------------------
------------------------ Validation --------------------------------------------
--------------------------------------------------------------------------------
instance (Arbitrary e, Arbitrary a) => Arbitrary (Validation e a) where
arbitrary = oneof [Failure <$> arbitrary, Success <$> arbitrary]
shrink (Failure x) = [ Failure x' | x' <- shrink x ]
shrink (Success y) = [ Success y' | y' <- shrink y ]
--------------------------------------------------------------------------------
------------------------ ArrowMonad --------------------------------------------
--------------------------------------------------------------------------------
instance Eq a => Eq (ArrowMonad (->) a) where
ArrowMonad f == ArrowMonad g = f () == g ()
instance Arbitrary a => Arbitrary (ArrowMonad (->) a) where
arbitrary = ArrowMonad . const <$> arbitrary
instance Show a => Show (ArrowMonad (->) a) where
show (ArrowMonad f) = show (f ())
--------------------------------------------------------------------------------
------------------------ Maybe -------------------------------------------------
--------------------------------------------------------------------------------
propertyPureRightMaybe :: IO ()
propertyPureRightMaybe = quickCheck (propertyPureRight @Maybe @Int @Int)
--------------------------------------------------------------------------------
------------------------ Identity ----------------------------------------------
--------------------------------------------------------------------------------
propertyPureRightIdentity :: IO ()
propertyPureRightIdentity = quickCheck (propertyPureRight @Identity @Int @Int)
--------------------------------------------------------------------------------
------------------------ Writer ------------------------------------------------
--------------------------------------------------------------------------------
instance (Arbitrary w, Arbitrary a) => Arbitrary (Writer w a) where
arbitrary = curry writer <$> arbitrary <*> arbitrary
deriving instance (Arbitrary e, Arbitrary a) => Arbitrary (Transformers.Except e a)
deriving instance (Arbitrary e, Arbitrary a) => Arbitrary (Except e a)