{-# 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

-- | NB: Since this requires both a `Corecursive` and `Eq` instance on the same
--       type, it _likely_ requires instances from yaya-unsafe.
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_cataFusion ::
--   (Eq a, Show a, Recursive (->) t f, Functor f, MonadTest m) =>
--   (a -> a) ->
--   Algebra (->) f a ->
--   f a ->
--   t ->
--   m ()
-- law_cataFusion f φ fa t =
--   uncurry (==) (bimap (f . φ) (φ . fmap f) $ diagonal fa)
--     ==> uncurry (===) (bimap (f . cata φ) (cata φ) $ diagonal t)

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

-- | Creates a generator for any `Steppable` type whose pattern functor has
--   terminal cases (e.g., not `Data.Functor.Identity` or `((,) a)`). @leaf@ can
--   only generate terminal cases, and `branch` can generate any case. If the
--   provided `branch` generates terminal cases, then the resulting tree may
--   have a height less than the `Size`, otherwise it will be a perfect tree
--   with a height of exactly the provided `Size`.
--
--   This is similar to `Gen.recursive` in that it separates the non-recursive
--   cases from the recursive ones, except
--
-- * the types here also ensure that the non-recursive cases aren’t recursive,
--
-- * different generator distributions may be used for rec & non-rec cases, and
--
-- * the non-recursive cases aren’t included in recursive calls (see above for
--   why).
--
--   If there’s no existing @Gen (f Void)@ for your pattern functor, you can
--   either create one manually, or pass `Hedgehog.Gen.discard` to the usual
--  @Gen a -> Gen (f a)@ generator.
--
--  NB: Hedgehog’s `Size` is signed, so this can raise an exception if given a
--      negative `Size`.
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)

-- | Builds a generic tree generator of a certain height.
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)

-- | Creates a generator for potentially-infinite values.
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

-- | Show that using a `Recursive` structure corecursively can lead to
--   non-termination.
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 properly-finite data structure will diverge on infinite unfolding
    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
    -- but using a lazy functor loses this property
    (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

-- | Show that using a `Corecursive` structure recursively can lead to
--   non-termination.
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
    -- We can easily get the first element of a corecursive infinite sequence
    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
    -- Of course, you can’t fold it.
    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
    -- But again, if you use a lazy functor, you lose that property, and you can
    -- short-circuit.
    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