{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE Unsafe #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
module Yaya.Hedgehog.Fold
( corecursiveIsUnsafe,
embeddableOfHeight,
genAlgebra,
genCorecursive,
law_anaRefl,
law_cataCancel,
law_cataCompose,
law_cataRefl,
recursiveIsUnsafe,
)
where
import safe "base" Control.Category (Category ((.)))
import safe "base" Data.Bifunctor (Bifunctor (bimap, first))
import safe "base" Data.Eq (Eq)
import safe "base" Data.Function (($))
import safe "base" Data.Functor (Functor (fmap))
import safe "base" Data.Proxy (Proxy (Proxy))
import safe qualified "base" Data.Tuple as Tuple
import safe "base" Data.Void (Void, absurd)
import safe "base" Numeric.Natural (Natural)
import safe "base" Text.Show (Show)
import "hedgehog" Hedgehog
( Gen,
MonadTest,
Property,
Size,
property,
withTests,
(===),
)
import "yaya" Yaya.Fold
( Algebra,
Corecursive (ana),
Projectable (project),
Recursive (cata),
Steppable (embed),
)
import safe "yaya" Yaya.Fold.Common (diagonal)
import safe "yaya" Yaya.Fold.Native ()
import safe "yaya" Yaya.Pattern (Maybe, Pair ((:!:)), fst, maybe, uncurry)
import "this" Yaya.Hedgehog (evalNonterminating)
import safe "base" Prelude (fromIntegral)
{-# HLINT ignore "Use camelCase" #-}
law_cataCancel ::
( Eq a,
Show a,
Steppable (->) t f,
Recursive (->) t f,
Functor f,
MonadTest m
) =>
Algebra (->) f a ->
f t ->
m ()
law_cataCancel :: forall a t (f :: * -> *) (m :: * -> *).
(Eq a, Show a, Steppable (->) t f, Recursive (->) t f, Functor f,
MonadTest m) =>
Algebra (->) f a -> f t -> m ()
law_cataCancel Algebra (->) f a
φ =
(a -> a -> m ()) -> Pair a a -> m ()
forall a b c. (a -> b -> c) -> Pair a b -> c
uncurry a -> a -> m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
(===) (Pair a a -> m ()) -> (f t -> Pair a a) -> f t -> m ()
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
. (f t -> a) -> (f t -> a) -> Pair (f t) (f t) -> Pair a a
forall a b c d. (a -> b) -> (c -> d) -> Pair a c -> Pair b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (Algebra (->) f a -> t -> a
forall a. Algebra (->) f a -> t -> a
forall {k} {k1} (c :: k -> k1 -> *) (t :: k) (f :: k1 -> k)
(a :: k1).
Recursive c t f =>
Algebra c f a -> c t a
cata Algebra (->) f a
φ (t -> a) -> (f t -> t) -> f t -> 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
. f t -> t
forall {k} (c :: k -> k -> *) (t :: k) (f :: k -> k).
Steppable c t f =>
Algebra c f t
embed) (Algebra (->) f a
φ Algebra (->) f a -> (f t -> f a) -> f t -> 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
. (t -> a) -> f t -> f a
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Algebra (->) f a -> t -> a
forall a. Algebra (->) f a -> t -> a
forall {k} {k1} (c :: k -> k1 -> *) (t :: k) (f :: k1 -> k)
(a :: k1).
Recursive c t f =>
Algebra c f a -> c t a
cata Algebra (->) f a
φ)) (Pair (f t) (f t) -> Pair a a)
-> (f t -> Pair (f t) (f t)) -> f t -> Pair a 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
. f t -> Pair (f t) (f t)
forall a. a -> Pair a a
diagonal
law_cataRefl ::
(Eq t, Show t, Steppable (->) t f, Recursive (->) t f, MonadTest m) =>
t ->
m ()
law_cataRefl :: forall t (f :: * -> *) (m :: * -> *).
(Eq t, Show t, Steppable (->) t f, Recursive (->) t f,
MonadTest m) =>
t -> m ()
law_cataRefl = (t -> t -> m ()) -> Pair t t -> m ()
forall a b c. (a -> b -> c) -> Pair a b -> c
uncurry t -> t -> m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
(===) (Pair t t -> m ()) -> (t -> Pair t t) -> t -> m ()
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
. (t -> t) -> Pair t t -> Pair t t
forall a b c. (a -> b) -> Pair a c -> Pair b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Algebra (->) f t -> t -> t
forall a. Algebra (->) f a -> t -> a
forall {k} {k1} (c :: k -> k1 -> *) (t :: k) (f :: k1 -> k)
(a :: k1).
Recursive c t f =>
Algebra c f a -> c t a
cata Algebra (->) f t
forall {k} (c :: k -> k -> *) (t :: k) (f :: k -> k).
Steppable c t f =>
Algebra c f t
embed) (Pair t t -> Pair t t) -> (t -> Pair t t) -> t -> Pair t t
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
. t -> Pair t t
forall a. a -> Pair a a
diagonal
law_anaRefl ::
(Eq t, Show t, Steppable (->) t f, Corecursive (->) t f, MonadTest m) =>
t ->
m ()
law_anaRefl :: forall t (f :: * -> *) (m :: * -> *).
(Eq t, Show t, Steppable (->) t f, Corecursive (->) t f,
MonadTest m) =>
t -> m ()
law_anaRefl = (t -> t -> m ()) -> Pair t t -> m ()
forall a b c. (a -> b -> c) -> Pair a b -> c
uncurry t -> t -> m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
(===) (Pair t t -> m ()) -> (t -> Pair t t) -> t -> m ()
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
. (t -> t) -> Pair t t -> Pair t t
forall a b c. (a -> b) -> Pair a c -> Pair b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Coalgebra (->) f t -> t -> t
forall a. Coalgebra (->) f a -> a -> t
forall {k} {k1} (c :: k -> k1 -> *) (t :: k1) (f :: k -> k1)
(a :: k).
Corecursive c t f =>
Coalgebra c f a -> c a t
ana Coalgebra (->) f t
forall {k} {k1} (c :: k -> k1 -> *) (t :: k) (f :: k -> k1).
Projectable c t f =>
Coalgebra c f t
project) (Pair t t -> Pair t t) -> (t -> Pair t t) -> t -> Pair t t
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
. t -> Pair t t
forall a. a -> Pair a a
diagonal
law_cataCompose ::
forall t f u g m b.
( Eq b,
Show b,
Recursive (->) t f,
Steppable (->) u g,
Recursive (->) u g,
MonadTest m
) =>
Proxy u ->
Algebra (->) g b ->
(forall a. f a -> g a) ->
t ->
m ()
law_cataCompose :: forall t (f :: * -> *) u (g :: * -> *) (m :: * -> *) b.
(Eq b, Show b, Recursive (->) t f, Steppable (->) u g,
Recursive (->) u g, MonadTest m) =>
Proxy u -> Algebra (->) g b -> (forall a. f a -> g a) -> t -> m ()
law_cataCompose Proxy u
Proxy Algebra (->) g b
φ forall a. f a -> g a
ε =
(b -> b -> m ()) -> Pair b b -> m ()
forall a b c. (a -> b -> c) -> Pair a b -> c
uncurry b -> b -> m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
(===)
(Pair b b -> m ()) -> (t -> Pair b b) -> t -> m ()
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
. (t -> b) -> (t -> b) -> Pair t t -> Pair b b
forall a b c d. (a -> b) -> (c -> d) -> Pair a c -> Pair b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (Algebra (->) g b -> u -> b
forall a. Algebra (->) g a -> u -> a
forall {k} {k1} (c :: k -> k1 -> *) (t :: k) (f :: k1 -> k)
(a :: k1).
Recursive c t f =>
Algebra c f a -> c t a
cata Algebra (->) g b
φ (u -> b) -> (t -> u) -> t -> 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
. Algebra (->) f u -> t -> u
forall a. Algebra (->) f a -> t -> a
forall {k} {k1} (c :: k -> k1 -> *) (t :: k) (f :: k1 -> k)
(a :: k1).
Recursive c t f =>
Algebra c f a -> c t a
cata (Algebra (->) g u
forall {k} (c :: k -> k -> *) (t :: k) (f :: k -> k).
Steppable c t f =>
Algebra c f t
embed Algebra (->) g u -> (f u -> g u) -> Algebra (->) f u
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
. f u -> g u
forall a. f a -> g a
ε :: f u -> u)) (Algebra (->) f b -> t -> b
forall a. Algebra (->) f a -> t -> a
forall {k} {k1} (c :: k -> k1 -> *) (t :: k) (f :: k1 -> k)
(a :: k1).
Recursive c t f =>
Algebra c f a -> c t a
cata (Algebra (->) g b
φ Algebra (->) g b -> (f b -> g b) -> Algebra (->) f 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
. f b -> g b
forall a. f a -> g a
ε))
(Pair t t -> Pair b b) -> (t -> Pair t t) -> t -> Pair b 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
. t -> Pair t t
forall a. a -> Pair a a
diagonal
embeddableOfHeight ::
(Steppable (->) t f, Functor f) =>
Gen (f Void) ->
(Gen t -> Gen (f t)) ->
Size ->
Gen t
embeddableOfHeight :: forall t (f :: * -> *).
(Steppable (->) t f, Functor f) =>
Gen (f Void) -> (Gen t -> Gen (f t)) -> Size -> Gen t
embeddableOfHeight Gen (f Void)
leaf Gen t -> Gen (f t)
branch Size
size =
Algebra (->) Maybe (Gen t) -> Natural -> Gen t
forall a. Algebra (->) Maybe a -> Natural -> a
forall {k} {k1} (c :: k -> k1 -> *) (t :: k) (f :: k1 -> k)
(a :: k1).
Recursive c t f =>
Algebra c f a -> c t a
cata (Gen (f Void) -> (Gen t -> Gen (f t)) -> Algebra (->) Maybe (Gen t)
forall t (f :: * -> *).
(Steppable (->) t f, Functor f) =>
Gen (f Void) -> (Gen t -> Gen (f t)) -> Algebra (->) Maybe (Gen t)
genAlgebra Gen (f Void)
leaf Gen t -> Gen (f t)
branch) (Size -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
size :: Natural)
genAlgebra ::
(Steppable (->) t f, Functor f) =>
Gen (f Void) ->
(Gen t -> Gen (f t)) ->
Algebra (->) Maybe (Gen t)
genAlgebra :: forall t (f :: * -> *).
(Steppable (->) t f, Functor f) =>
Gen (f Void) -> (Gen t -> Gen (f t)) -> Algebra (->) Maybe (Gen t)
genAlgebra Gen (f Void)
leaf Gen t -> Gen (f t)
branch =
Gen t -> (Gen t -> Gen t) -> Maybe (Gen t) -> Gen t
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((f Void -> t) -> Gen (f Void) -> Gen t
forall a b. (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Algebra (->) f t
forall {k} (c :: k -> k -> *) (t :: k) (f :: k -> k).
Steppable c t f =>
Algebra c f t
embed Algebra (->) f t -> (f Void -> f t) -> f Void -> t
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
. (Void -> t) -> f Void -> f t
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Void -> t
forall a. Void -> a
absurd) Gen (f Void)
leaf) (Algebra (->) f t -> Gen (f t) -> Gen t
forall a b. (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Algebra (->) f t
forall {k} (c :: k -> k -> *) (t :: k) (f :: k -> k).
Steppable c t f =>
Algebra c f t
embed (Gen (f t) -> Gen t) -> (Gen t -> Gen (f t)) -> Gen t -> Gen t
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
. Gen t -> Gen (f t)
branch)
genCorecursive :: (Corecursive (->) t f) => (a -> f a) -> Gen a -> Gen t
genCorecursive :: forall t (f :: * -> *) a.
Corecursive (->) t f =>
(a -> f a) -> Gen a -> Gen t
genCorecursive = (a -> t) -> Gen a -> Gen t
forall a b. (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> t) -> Gen a -> Gen t)
-> ((a -> f a) -> a -> t) -> (a -> f a) -> Gen a -> Gen t
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 -> f a) -> a -> t
forall a. Coalgebra (->) f a -> a -> t
forall {k} {k1} (c :: k -> k1 -> *) (t :: k1) (f :: k -> k1)
(a :: k).
Corecursive c t f =>
Coalgebra c f a -> c a t
ana
corecursiveIsUnsafe ::
forall t a.
( Corecursive (->) (t (Pair a)) (Pair a),
Projectable (->) (t (Pair a)) (Pair a),
Corecursive (->) (t ((,) a)) ((,) a),
Projectable (->) (t ((,) a)) ((,) a),
Eq a,
Show a
) =>
Proxy t ->
a ->
Property
corecursiveIsUnsafe :: forall (t :: (* -> *) -> *) a.
(Corecursive (->) (t (Pair a)) (Pair a),
Projectable (->) (t (Pair a)) (Pair a),
Corecursive (->) (t ((,) a)) ((,) a),
Projectable (->) (t ((,) a)) ((,) a), Eq a, Show a) =>
Proxy t -> a -> Property
corecursiveIsUnsafe Proxy t
Proxy a
x =
TestLimit -> Property -> Property
withTests TestLimit
1 (Property -> Property)
-> (PropertyT IO () -> Property) -> PropertyT IO () -> 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
. HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
a -> PropertyT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadIO m, MonadTest m, Show a) =>
a -> m ()
evalNonterminating (a -> PropertyT IO ())
-> (t (Pair a) -> a) -> t (Pair a) -> PropertyT IO ()
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
. Pair a (t (Pair a)) -> a
forall a b. Pair a b -> a
fst (Pair a (t (Pair a)) -> a)
-> (t (Pair a) -> Pair a (t (Pair a))) -> t (Pair a) -> 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
. forall {k} {k1} (c :: k -> k1 -> *) (t :: k) (f :: k -> k1).
Projectable c t f =>
Coalgebra c f t
forall (c :: * -> * -> *) t (f :: * -> *).
Projectable c t f =>
Coalgebra c f t
project @_ @(t (Pair a)) (t (Pair a) -> PropertyT IO ()) -> t (Pair a) -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ Coalgebra (->) (Pair a) a -> a -> t (Pair a)
forall a. Coalgebra (->) (Pair a) a -> a -> t (Pair a)
forall {k} {k1} (c :: k -> k1 -> *) (t :: k1) (f :: k -> k1)
(a :: k).
Corecursive c t f =>
Coalgebra c f a -> c a t
ana (\a
y -> a
y a -> Coalgebra (->) (Pair a) a
forall a b. a -> b -> Pair a b
:!: a
y) a
x
(a, t ((,) a)) -> a
forall a b. (a, b) -> a
Tuple.fst (forall {k} {k1} (c :: k -> k1 -> *) (t :: k) (f :: k -> k1).
Projectable c t f =>
Coalgebra c f t
forall (c :: * -> * -> *) t (f :: * -> *).
Projectable c t f =>
Coalgebra c f t
project @_ @(t ((,) a)) Coalgebra (->) ((,) a) (t ((,) a))
-> Coalgebra (->) ((,) a) (t ((,) a))
forall a b. (a -> b) -> a -> b
$ Coalgebra (->) ((,) a) a -> a -> t ((,) a)
forall a. Coalgebra (->) ((,) a) a -> a -> t ((,) a)
forall {k} {k1} (c :: k -> k1 -> *) (t :: k1) (f :: k -> k1)
(a :: k).
Corecursive c t f =>
Coalgebra c f a -> c a t
ana (\a
y -> (a
y, a
y)) a
x) a -> a -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== a
x
recursiveIsUnsafe ::
forall t a.
( Corecursive (->) (t (Pair a)) (Pair a),
Projectable (->) (t (Pair a)) (Pair a),
Recursive (->) (t (Pair a)) (Pair a),
Corecursive (->) (t ((,) a)) ((,) a),
Recursive (->) (t ((,) a)) ((,) a),
Eq a,
Show a
) =>
Proxy t ->
a ->
Property
recursiveIsUnsafe :: forall (t :: (* -> *) -> *) a.
(Corecursive (->) (t (Pair a)) (Pair a),
Projectable (->) (t (Pair a)) (Pair a),
Recursive (->) (t (Pair a)) (Pair a),
Corecursive (->) (t ((,) a)) ((,) a),
Recursive (->) (t ((,) a)) ((,) a), Eq a, Show a) =>
Proxy t -> a -> Property
recursiveIsUnsafe Proxy t
Proxy a
x =
TestLimit -> Property -> Property
withTests TestLimit
1 (Property -> Property)
-> (PropertyT IO () -> Property) -> PropertyT IO () -> 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
. HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
Pair a (t (Pair a)) -> a
forall a b. Pair a b -> a
fst (Coalgebra (->) (Pair a) (t (Pair a))
forall {k} {k1} (c :: k -> k1 -> *) (t :: k) (f :: k -> k1).
Projectable c t f =>
Coalgebra c f t
project Coalgebra (->) (Pair a) (t (Pair a))
-> Coalgebra (->) (Pair a) (t (Pair a))
forall a b. (a -> b) -> a -> b
$ forall {k} {k1} (c :: k -> k1 -> *) (t :: k1) (f :: k -> k1)
(a :: k).
Corecursive c t f =>
Coalgebra c f a -> c a t
forall (c :: * -> * -> *) t (f :: * -> *) a.
Corecursive c t f =>
Coalgebra c f a -> c a t
ana @_ @(t (Pair a)) (\a
y -> a
y a -> Coalgebra (->) (Pair a) a
forall a b. a -> b -> Pair a b
:!: a
y) a
x) a -> a -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== a
x
a -> PropertyT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadIO m, MonadTest m, Show a) =>
a -> m ()
evalNonterminating (a -> PropertyT IO ())
-> (t (Pair a) -> a) -> t (Pair a) -> PropertyT IO ()
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
. Algebra (->) (Pair a) a -> t (Pair a) -> a
forall a. Algebra (->) (Pair a) a -> t (Pair a) -> a
forall {k} {k1} (c :: k -> k1 -> *) (t :: k) (f :: k1 -> k)
(a :: k1).
Recursive c t f =>
Algebra c f a -> c t a
cata Algebra (->) (Pair a) a
forall a b. Pair a b -> a
fst (t (Pair a) -> PropertyT IO ()) -> t (Pair a) -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ forall {k} {k1} (c :: k -> k1 -> *) (t :: k1) (f :: k -> k1)
(a :: k).
Corecursive c t f =>
Coalgebra c f a -> c a t
forall (c :: * -> * -> *) t (f :: * -> *) a.
Corecursive c t f =>
Coalgebra c f a -> c a t
ana @_ @(t (Pair a)) (\a
y -> a
y a -> Coalgebra (->) (Pair a) a
forall a b. a -> b -> Pair a b
:!: a
y) a
x
Algebra (->) ((,) a) a -> t ((,) a) -> a
forall a. Algebra (->) ((,) a) a -> t ((,) a) -> a
forall {k} {k1} (c :: k -> k1 -> *) (t :: k) (f :: k1 -> k)
(a :: k1).
Recursive c t f =>
Algebra c f a -> c t a
cata Algebra (->) ((,) a) a
forall a b. (a, b) -> a
Tuple.fst (forall {k} {k1} (c :: k -> k1 -> *) (t :: k1) (f :: k -> k1)
(a :: k).
Corecursive c t f =>
Coalgebra c f a -> c a t
forall (c :: * -> * -> *) t (f :: * -> *) a.
Corecursive c t f =>
Coalgebra c f a -> c a t
ana @_ @(t ((,) a)) (\a
y -> (a
y, a
y)) a
x) a -> a -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== a
x