1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
|
{-# 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)
|
