{-# LANGUAGE Safe #-}

-- | Definitions and instances that use direct recursion, which (because of
--   laziness) can lead to non-termination.
module Yaya.Unsafe.Fold
  ( anaM,
    corecursivePrism,
    ganaM,
    ghylo,
    ghyloM,
    hylo,
    hyloM,
    stream',
    streamAna,
    streamGApo,
    unsafeAna,
    unsafeCata,
  )
where

import "base" Control.Applicative (Applicative (pure))
import "base" Control.Category (Category ((.)))
import "base" Control.Monad (Monad, (<=<))
import "base" Data.Bifunctor (Bifunctor (first))
import "base" Data.Function (flip)
import "base" Data.Functor (Functor (fmap))
import "base" Data.Functor.Compose (Compose (Compose, getCompose))
import "base" Data.Traversable (Traversable (sequenceA))
import "comonad" Control.Comonad (Comonad (extract))
import "lens" Control.Lens (Prism', matching, prism, review, (&))
import "yaya" Yaya.Fold
  ( Algebra,
    AlgebraM,
    Coalgebra,
    CoalgebraM,
    CoalgebraPrism,
    Corecursive (ana),
    DistributiveLaw,
    GAlgebra,
    GAlgebraM,
    GCoalgebra,
    GCoalgebraM,
    Projectable (project),
    Recursive (cata),
    Steppable (embed),
    lowerAlgebra,
    lowerAlgebraM,
    lowerCoalgebra,
    lowerCoalgebraM,
  )
import "yaya" Yaya.Pattern (Maybe, Pair, maybe, uncurry)

-- | Instances leak transitively, so while "Yaya.Unsafe.Fold.Instances" exists,
--   it should only be used when it is unavoidable. If you are explicitly
--   folding a structure unsafely, use this function instead of importing that
--   module.
unsafeAna :: (Steppable (->) t f, Functor f) => Coalgebra (->) f a -> a -> t
unsafeAna :: forall t (f :: * -> *) a.
(Steppable (->) t f, Functor f) =>
Coalgebra (->) f a -> a -> t
unsafeAna = Algebra (->) f t -> Coalgebra (->) f a -> a -> t
forall (f :: * -> *) b a.
Functor f =>
Algebra (->) f b -> Coalgebra (->) f a -> a -> b
hylo Algebra (->) f t
forall {k} (c :: k -> k -> *) (t :: k) (f :: k -> k).
Steppable c t f =>
Algebra c f t
embed

-- | Instances leak transitively, so while "Yaya.Unsafe.Fold.Instances" exists,
--   it should only be used when it is unavoidable. If you are explicitly
--   unfolding a structure unsafely, use this function instead of importing that
--   module.
--
--   Should one prefer `unsafeAna` or `unsafeCata` in cases where both are
--   applicable?
-- - one may provide weaker constraints than the other in certain cases (e.g.,
--   on its own, `unsafeCata` only requires `Projectable` on the source, but
--  `unsafeAna` requires `Steppable` on the target. Depending on what other
--   constraints already exist on the function, either one may ultimately be
--   less constrained.
-- - they may fail differently: `unsafeCata` (folding a potentially-infinite
--   structure) is likely to result in non-termination, whereas `unsafeAna`
--   (building a potentially-infinite structure strictly) is likely to use up
--   the memory or overflow the stack.
unsafeCata :: (Projectable (->) t f, Functor f) => Algebra (->) f a -> t -> a
unsafeCata :: forall t (f :: * -> *) a.
(Projectable (->) t f, Functor f) =>
Algebra (->) f a -> t -> a
unsafeCata = (Algebra (->) f a -> Coalgebra (->) f t -> t -> a)
-> Coalgebra (->) f t -> Algebra (->) f a -> t -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Algebra (->) f a -> Coalgebra (->) f t -> t -> a
forall (f :: * -> *) b a.
Functor f =>
Algebra (->) f b -> Coalgebra (->) f a -> a -> b
hylo Coalgebra (->) f t
forall {k} {k1} (c :: k -> k1 -> *) (t :: k) (f :: k -> k1).
Projectable c t f =>
Coalgebra c f t
project

-- | This can’t be implemented in a total fashion. There is a /similar/ approach
--   that can be total – with `ψ :: CoalgebraM (->) m f a`, `ana (Compose . ψ)`
--   results in something like `Nu (Compose m f)` which is akin to an effectful
--   stream.
anaM ::
  (Monad m, Steppable (->) t f, Traversable f) =>
  CoalgebraM (->) m f a ->
  a ->
  m t
anaM :: forall (m :: * -> *) t (f :: * -> *) a.
(Monad m, Steppable (->) t f, Traversable f) =>
CoalgebraM (->) m f a -> a -> m t
anaM = AlgebraM (->) m f t -> CoalgebraM (->) m f a -> a -> m t
forall (m :: * -> *) (f :: * -> *) b a.
(Monad m, Traversable f) =>
AlgebraM (->) m f b -> CoalgebraM (->) m f a -> a -> m b
hyloM (t -> m t
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> m t) -> (f t -> t) -> AlgebraM (->) m f 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
. f t -> t
forall {k} (c :: k -> k -> *) (t :: k) (f :: k -> k).
Steppable c t f =>
Algebra c f t
embed)

ganaM ::
  (Monad m, Monad n, Traversable n, Steppable (->) t f, Traversable f) =>
  DistributiveLaw (->) n f ->
  GCoalgebraM (->) m n f a ->
  a ->
  m t
ganaM :: forall (m :: * -> *) (n :: * -> *) t (f :: * -> *) a.
(Monad m, Monad n, Traversable n, Steppable (->) t f,
 Traversable f) =>
DistributiveLaw (->) n f -> GCoalgebraM (->) m n f a -> a -> m t
ganaM DistributiveLaw (->) n f
k GCoalgebraM (->) m n f a
ψ = CoalgebraM (->) m f (n a) -> n a -> m t
forall (m :: * -> *) t (f :: * -> *) a.
(Monad m, Steppable (->) t f, Traversable f) =>
CoalgebraM (->) m f a -> a -> m t
anaM (DistributiveLaw (->) n f
-> GCoalgebraM (->) m n f a -> CoalgebraM (->) m f (n a)
forall (m :: * -> *) (f :: * -> *) (n :: * -> *) a.
(Applicative m, Traversable f, Monad n, Traversable n) =>
DistributiveLaw (->) n f
-> GCoalgebraM (->) m n f a -> CoalgebraM (->) m f (n a)
lowerCoalgebraM n (f a) -> f (n a)
DistributiveLaw (->) n f
k GCoalgebraM (->) m n f a
ψ) (n a -> m t) -> (a -> n a) -> a -> m 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 -> n a
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | Fusion of an 'ana' and 'cata'.
hylo :: (Functor f) => Algebra (->) f b -> Coalgebra (->) f a -> a -> b
hylo :: forall (f :: * -> *) b a.
Functor f =>
Algebra (->) f b -> Coalgebra (->) f a -> a -> b
hylo Algebra (->) f b
φ Coalgebra (->) f a
ψ = a -> b
go
  where
    go :: a -> b
go = Algebra (->) f b
φ Algebra (->) f b -> (a -> f 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) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
go (f a -> f b) -> Coalgebra (->) f a -> a -> 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
. Coalgebra (->) f a
ψ

ghylo ::
  (Comonad w, Monad m, Functor f) =>
  DistributiveLaw (->) f w ->
  DistributiveLaw (->) m f ->
  GAlgebra (->) w f b ->
  GCoalgebra (->) m f a ->
  a ->
  b
ghylo :: forall (w :: * -> *) (m :: * -> *) (f :: * -> *) b a.
(Comonad w, Monad m, Functor f) =>
DistributiveLaw (->) f w
-> DistributiveLaw (->) m f
-> GAlgebra (->) w f b
-> GCoalgebra (->) m f a
-> a
-> b
ghylo DistributiveLaw (->) f w
w DistributiveLaw (->) m f
m GAlgebra (->) w f b
φ GCoalgebra (->) m f a
ψ =
  w b -> b
forall a. w a -> a
forall (w :: * -> *) a. Comonad w => w a -> a
extract (w b -> b) -> (a -> w 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
. Algebra (->) f (w b) -> Coalgebra (->) f (m a) -> m a -> w b
forall (f :: * -> *) b a.
Functor f =>
Algebra (->) f b -> Coalgebra (->) f a -> a -> b
hylo (DistributiveLaw (->) f w
-> GAlgebra (->) w f b -> Algebra (->) f (w b)
forall (f :: * -> *) (w :: * -> *) a.
(Functor f, Comonad w) =>
DistributiveLaw (->) f w
-> GAlgebra (->) w f a -> Algebra (->) f (w a)
lowerAlgebra f (w a) -> w (f a)
DistributiveLaw (->) f w
w GAlgebra (->) w f b
φ) (DistributiveLaw (->) m f
-> GCoalgebra (->) m f a -> Coalgebra (->) f (m a)
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, Monad m) =>
DistributiveLaw (->) m f
-> GCoalgebra (->) m f a -> Coalgebra (->) f (m a)
lowerCoalgebra m (f a) -> f (m a)
DistributiveLaw (->) m f
m GCoalgebra (->) m f a
ψ) (m a -> w b) -> (a -> m a) -> a -> w 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 -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

hyloM ::
  (Monad m, Traversable f) =>
  AlgebraM (->) m f b ->
  CoalgebraM (->) m f a ->
  a ->
  m b
hyloM :: forall (m :: * -> *) (f :: * -> *) b a.
(Monad m, Traversable f) =>
AlgebraM (->) m f b -> CoalgebraM (->) m f a -> a -> m b
hyloM AlgebraM (->) m f b
φ CoalgebraM (->) m f a
ψ = Algebra (->) (Compose m f) (m b)
-> Coalgebra (->) (Compose m f) a -> a -> m b
forall (f :: * -> *) b a.
Functor f =>
Algebra (->) f b -> Coalgebra (->) f a -> a -> b
hylo (AlgebraM (->) m f b
φ AlgebraM (->) m f b
-> (Compose m f (m b) -> m (f b))
-> Algebra (->) (Compose m f) (m b)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f (m b) -> m (f b)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => f (f a) -> f (f a)
sequenceA (f (m b) -> m (f b))
-> (Compose m f (m b) -> m (f (m b)))
-> Compose m f (m b)
-> m (f b)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Compose m f (m b) -> m (f (m b))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose) (m (f a) -> Compose m f a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (m (f a) -> Compose m f a)
-> CoalgebraM (->) m f a -> Coalgebra (->) (Compose m f) 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
. CoalgebraM (->) m f a
ψ)

ghyloM ::
  (Comonad w, Traversable w, Monad m, Traversable f, Monad n, Traversable n) =>
  DistributiveLaw (->) f w ->
  DistributiveLaw (->) n f ->
  GAlgebraM (->) m w f b ->
  GCoalgebraM (->) m n f a ->
  a ->
  m b
ghyloM :: forall (w :: * -> *) (m :: * -> *) (f :: * -> *) (n :: * -> *) b a.
(Comonad w, Traversable w, Monad m, Traversable f, Monad n,
 Traversable n) =>
DistributiveLaw (->) f w
-> DistributiveLaw (->) n f
-> GAlgebraM (->) m w f b
-> GCoalgebraM (->) m n f a
-> a
-> m b
ghyloM DistributiveLaw (->) f w
w DistributiveLaw (->) n f
n GAlgebraM (->) m w f b
φ GCoalgebraM (->) m n f a
ψ =
  (w b -> b) -> m (w b) -> m b
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap w b -> b
forall a. w a -> a
forall (w :: * -> *) a. Comonad w => w a -> a
extract (m (w b) -> m b) -> (a -> m (w b)) -> a -> m 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
. AlgebraM (->) m f (w b)
-> CoalgebraM (->) m f (n a) -> n a -> m (w b)
forall (m :: * -> *) (f :: * -> *) b a.
(Monad m, Traversable f) =>
AlgebraM (->) m f b -> CoalgebraM (->) m f a -> a -> m b
hyloM (DistributiveLaw (->) f w
-> GAlgebraM (->) m w f b -> AlgebraM (->) m f (w b)
forall (m :: * -> *) (f :: * -> *) (w :: * -> *) a.
(Applicative m, Traversable f, Comonad w, Traversable w) =>
DistributiveLaw (->) f w
-> GAlgebraM (->) m w f a -> AlgebraM (->) m f (w a)
lowerAlgebraM f (w a) -> w (f a)
DistributiveLaw (->) f w
w GAlgebraM (->) m w f b
φ) (DistributiveLaw (->) n f
-> GCoalgebraM (->) m n f a -> CoalgebraM (->) m f (n a)
forall (m :: * -> *) (f :: * -> *) (n :: * -> *) a.
(Applicative m, Traversable f, Monad n, Traversable n) =>
DistributiveLaw (->) n f
-> GCoalgebraM (->) m n f a -> CoalgebraM (->) m f (n a)
lowerCoalgebraM n (f a) -> f (n a)
DistributiveLaw (->) n f
n GCoalgebraM (->) m n f a
ψ) (n a -> m (w b)) -> (a -> n a) -> a -> m (w 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 -> n a
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

stream' ::
  (Projectable (->) t f, Steppable (->) u g, Functor g) =>
  CoalgebraM (->) Maybe g b ->
  (b -> (Pair (b -> b) t -> u) -> f t -> u) ->
  b ->
  t ->
  u
stream' :: forall t (f :: * -> *) u (g :: * -> *) b.
(Projectable (->) t f, Steppable (->) u g, Functor g) =>
CoalgebraM (->) Maybe g b
-> (b -> (Pair (b -> b) t -> u) -> f t -> u) -> b -> t -> u
stream' CoalgebraM (->) Maybe g b
ψ b -> (Pair (b -> b) t -> u) -> f t -> u
f = b -> t -> u
go
  where
    go :: b -> t -> u
go b
c t
x =
      u -> (g b -> u) -> Maybe (g b) -> u
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
        (b -> (Pair (b -> b) t -> u) -> f t -> u
f b
c ((b -> t -> u) -> Pair b t -> u
forall a b c. (a -> b -> c) -> Pair a b -> c
uncurry b -> t -> u
go (Pair b t -> u)
-> (Pair (b -> b) t -> Pair b t) -> Pair (b -> b) t -> 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
. ((b -> b) -> b) -> Pair (b -> b) t -> Pair b 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 (b
c &)) (Coalgebra (->) f t
forall {k} {k1} (c :: k -> k1 -> *) (t :: k) (f :: k -> k1).
Projectable c t f =>
Coalgebra c f t
project t
x))
        (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 -> (g b -> g u) -> g b -> 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
. (b -> u) -> g b -> g u
forall a b. (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (b -> t -> u
`go` t
x))
        (CoalgebraM (->) Maybe g b
ψ b
c)

-- | Gibbons’ metamorphism. It lazily folds a (necessarily infinite) value,
--   incrementally re-expanding that value into some new representation.
--
--  __NB__: See https://gist.github.com/sellout/4709e723cb649110af00217486c4466b
--          for some commentary and explanation.
streamAna ::
  (Projectable (->) t f, Steppable (->) u g, Functor g) =>
  CoalgebraM (->) Maybe g b ->
  AlgebraM (->) (Pair (b -> b)) f t ->
  b ->
  t ->
  u
streamAna :: forall t (f :: * -> *) u (g :: * -> *) b.
(Projectable (->) t f, Steppable (->) u g, Functor g) =>
CoalgebraM (->) Maybe g b
-> AlgebraM (->) (Pair (b -> b)) f t -> b -> t -> u
streamAna CoalgebraM (->) Maybe g b
process AlgebraM (->) (Pair (b -> b)) f t
accum = CoalgebraM (->) Maybe g b
-> (b -> (Pair (b -> b) t -> u) -> f t -> u) -> b -> t -> u
forall t (f :: * -> *) u (g :: * -> *) b.
(Projectable (->) t f, Steppable (->) u g, Functor g) =>
CoalgebraM (->) Maybe g b
-> (b -> (Pair (b -> b) t -> u) -> f t -> u) -> b -> t -> u
stream' CoalgebraM (->) Maybe g b
process (\b
_ Pair (b -> b) t -> u
f -> Pair (b -> b) t -> u
f (Pair (b -> b) t -> u)
-> AlgebraM (->) (Pair (b -> b)) f t -> f t -> 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
. AlgebraM (->) (Pair (b -> b)) f t
accum)

-- | Another form of Gibbons’ metamorphism. This one can be applied to non-
--   infinite inputs and takes an additional “flushing” coalgebra to be applied
--   after all the input has been consumed.
--
--  __NB__: See https://gist.github.com/sellout/4709e723cb649110af00217486c4466b
--          for some commentary and explanation.
streamGApo ::
  (Projectable (->) t f, Steppable (->) u g, Corecursive (->) u g, Functor g) =>
  Coalgebra (->) g b ->
  CoalgebraM (->) Maybe g b ->
  (f t -> Maybe (Pair (b -> b) t)) ->
  b ->
  t ->
  u
streamGApo :: forall t (f :: * -> *) u (g :: * -> *) b.
(Projectable (->) t f, Steppable (->) u g, Corecursive (->) u g,
 Functor g) =>
Coalgebra (->) g b
-> CoalgebraM (->) Maybe g b
-> (f t -> Maybe (Pair (b -> b) t))
-> b
-> t
-> u
streamGApo Coalgebra (->) g b
flush CoalgebraM (->) Maybe g b
process f t -> Maybe (Pair (b -> b) t)
accum =
  CoalgebraM (->) Maybe g b
-> (b -> (Pair (b -> b) t -> u) -> f t -> u) -> b -> t -> u
forall t (f :: * -> *) u (g :: * -> *) b.
(Projectable (->) t f, Steppable (->) u g, Functor g) =>
CoalgebraM (->) Maybe g b
-> (b -> (Pair (b -> b) t -> u) -> f t -> u) -> b -> t -> u
stream' CoalgebraM (->) Maybe g b
process (\b
c Pair (b -> b) t -> u
f -> u -> (Pair (b -> b) t -> u) -> Maybe (Pair (b -> b) t) -> u
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Coalgebra (->) g b -> b -> u
forall a. Coalgebra (->) g a -> a -> u
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 (->) g b
flush b
c) Pair (b -> b) t -> u
f (Maybe (Pair (b -> b) t) -> u)
-> (f t -> Maybe (Pair (b -> b) t)) -> f t -> 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 t -> Maybe (Pair (b -> b) t)
accum)

corecursivePrism ::
  (Steppable (->) t f, Recursive (->) t f, Traversable f) =>
  CoalgebraPrism f a ->
  Prism' a t
corecursivePrism :: forall t (f :: * -> *) a.
(Steppable (->) t f, Recursive (->) t f, Traversable f) =>
CoalgebraPrism f a -> Prism' a t
corecursivePrism CoalgebraPrism f a
alg = (t -> a) -> (a -> Either a t) -> Prism a a t t
forall b t s a. (b -> t) -> (s -> Either t a) -> Prism s t a b
prism (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 (AReview a (f a) -> Algebra (->) f a
forall b (m :: * -> *) t. MonadReader b m => AReview t b -> m t
review AReview a (f a)
CoalgebraPrism f a
alg)) (CoalgebraM (->) (Either a) f a -> a -> Either a t
forall (m :: * -> *) t (f :: * -> *) a.
(Monad m, Steppable (->) t f, Traversable f) =>
CoalgebraM (->) m f a -> a -> m t
anaM (APrism a a (f a) (f a) -> CoalgebraM (->) (Either a) f a
forall s t a b. APrism s t a b -> s -> Either t a
matching APrism a a (f a) (f a)
CoalgebraPrism f a
alg))