module IsomorphismClass.Laws
( isSomeLawsProperties,
isLawsProperties,
)
where
import IsomorphismClass.Classes
import IsomorphismClass.Prelude
import Test.QuickCheck
isSomeLawsProperties ::
(IsSome a b, Eq a, Eq b, Show a, Arbitrary b, Show b) =>
Proxy a ->
Proxy b ->
[(String, Property)]
isSomeLawsProperties :: forall a b.
(IsSome a b, Eq a, Eq b, Show a, Arbitrary b, Show b) =>
Proxy a -> Proxy b -> [(String, Property)]
isSomeLawsProperties Proxy a
superp Proxy b
subp =
[ ( String
"'to' is injective",
(b -> b -> Property) -> Property
forall prop. Testable prop => prop -> Property
property \b
a b
b ->
b
a b -> b -> Bool
forall a. Eq a => a -> a -> Bool
/= b
b Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==>
b -> a
to' b
a a -> a -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=/= b -> a
to' b
b
),
( String
"'maybeFrom' is an inverse of 'to'",
(b -> Property) -> Property
forall prop. Testable prop => prop -> Property
property \b
a ->
a -> Maybe b
maybeFrom' (b -> a
to' b
a) Maybe b -> Maybe b -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== b -> Maybe b
forall a. a -> Maybe a
Just b
a
)
]
where
to' :: b -> a
to' = Proxy a -> a -> a
forall {proxy :: * -> *} {c}. proxy c -> c -> c
as Proxy a
superp (a -> a) -> (b -> a) -> b -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. b -> a
forall sup sub. IsSome sup sub => sub -> sup
to (b -> a) -> (b -> b) -> b -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Proxy b -> b -> b
forall {proxy :: * -> *} {c}. proxy c -> c -> c
as Proxy b
subp
maybeFrom' :: a -> Maybe b
maybeFrom' = (b -> b) -> Maybe b -> Maybe b
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Proxy b -> b -> b
forall {proxy :: * -> *} {c}. proxy c -> c -> c
as Proxy b
subp) (Maybe b -> Maybe b) -> (a -> Maybe b) -> a -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> Maybe b
forall sup sub. IsSome sup sub => sup -> Maybe sub
maybeFrom (a -> Maybe b) -> (a -> a) -> a -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Proxy a -> a -> a
forall {proxy :: * -> *} {c}. proxy c -> c -> c
as Proxy a
superp
as :: proxy c -> c -> c
as = (c -> proxy c -> c) -> proxy c -> c -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip c -> proxy c -> c
forall a (proxy :: * -> *). a -> proxy a -> a
asProxyTypeOf
isLawsProperties ::
(Is a b, Eq a, Eq b, Arbitrary a, Show a, Arbitrary b, Show b) =>
Proxy a ->
Proxy b ->
[(String, Property)]
isLawsProperties :: forall a b.
(Is a b, Eq a, Eq b, Arbitrary a, Show a, Arbitrary b, Show b) =>
Proxy a -> Proxy b -> [(String, Property)]
isLawsProperties Proxy a
superp Proxy b
subp =
[ String -> Proxy a -> Proxy b -> [(String, Property)]
forall {b} {a}.
(Arbitrary b, IsSome b a, IsSome a b, Eq b, Eq a, Show b,
Show a) =>
String -> Proxy a -> Proxy b -> [(String, Property)]
directedLaws String
"↻" Proxy a
superp Proxy b
subp,
String -> Proxy b -> Proxy a -> [(String, Property)]
forall {b} {a}.
(Arbitrary b, IsSome b a, IsSome a b, Eq b, Eq a, Show b,
Show a) =>
String -> Proxy a -> Proxy b -> [(String, Property)]
directedLaws String
"↺" Proxy b
subp Proxy a
superp
]
[[(String, Property)]]
-> ([[(String, Property)]] -> [(String, Property)])
-> [(String, Property)]
forall a b. a -> (a -> b) -> b
& [[(String, Property)]] -> [(String, Property)]
forall a. Monoid a => [a] -> a
mconcat
where
directedLaws :: String -> Proxy a -> Proxy b -> [(String, Property)]
directedLaws String
prefix Proxy a
ap Proxy b
bp =
( ( String
"Isomorphic: Law 1",
(b -> Property) -> Property
forall prop. Testable prop => prop -> Property
property \b
b ->
b
b b -> b -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== a -> b
forall sup sub. IsSome sup sub => sub -> sup
to (a -> Proxy a -> a
forall a (proxy :: * -> *). a -> proxy a -> a
asProxyTypeOf (b -> a
forall sup sub. IsSome sup sub => sub -> sup
to (b -> Proxy b -> b
forall a (proxy :: * -> *). a -> proxy a -> a
asProxyTypeOf b
b Proxy b
bp)) Proxy a
ap)
)
(String, Property) -> [(String, Property)] -> [(String, Property)]
forall a. a -> [a] -> [a]
: String -> [(String, Property)] -> [(String, Property)]
prefixEachName String
"Partially isomorphic: " (Proxy a -> Proxy b -> [(String, Property)]
forall a b.
(IsSome a b, Eq a, Eq b, Show a, Arbitrary b, Show b) =>
Proxy a -> Proxy b -> [(String, Property)]
isSomeLawsProperties Proxy a
ap Proxy b
bp)
)
[(String, Property)]
-> ([(String, Property)] -> [(String, Property)])
-> [(String, Property)]
forall a b. a -> (a -> b) -> b
& String -> [(String, Property)] -> [(String, Property)]
prefixEachName (String
prefix String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
": ")
prefixEachName ::
String ->
[(String, Property)] ->
[(String, Property)]
prefixEachName :: String -> [(String, Property)] -> [(String, Property)]
prefixEachName String
prefix =
(((String, Property) -> (String, Property))
-> [(String, Property)] -> [(String, Property)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((String, Property) -> (String, Property))
-> [(String, Property)] -> [(String, Property)])
-> ((String -> String) -> (String, Property) -> (String, Property))
-> (String -> String)
-> [(String, Property)]
-> [(String, Property)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (String -> String) -> (String, Property) -> (String, Property)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first) (String -> String -> String
forall a. Monoid a => a -> a -> a
mappend String
prefix)