module IsomorphismClass.Properties
( isomorphicToProperties,
)
where
import IsomorphismClass.Classes
import IsomorphismClass.Prelude
import Test.QuickCheck
isomorphicToProperties ::
(IsomorphicTo a b, Eq a, Eq b, Arbitrary a, Show a, Arbitrary b, Show b) =>
Proxy a ->
Proxy b ->
[(String, Property)]
isomorphicToProperties :: forall a b.
(IsomorphicTo a b, Eq a, Eq b, Arbitrary a, Show a, Arbitrary b,
Show b) =>
Proxy a -> Proxy b -> [(String, Property)]
isomorphicToProperties Proxy a
aProxy Proxy b
bProxy =
[ ( String
"from . to = id",
(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
from' (b -> a
to' b
b)
),
( String
"to . from = id",
(a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property \a
b -> a
b a -> a -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== b -> a
to' (a -> b
from' a
b)
)
]
where
to' :: b -> a
to' = Proxy a -> a -> a
forall {proxy :: * -> *} {c}. proxy c -> c -> c
as Proxy a
aProxy (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 a b. IsomorphicTo a b => b -> a
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
bProxy
from' :: a -> b
from' = Proxy b -> b -> b
forall {proxy :: * -> *} {c}. proxy c -> c -> c
as Proxy b
bProxy (b -> b) -> (a -> b) -> a -> 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 -> b
forall a b. IsomorphicTo a b => a -> b
from (a -> b) -> (a -> a) -> a -> 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
aProxy
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