{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Control.Comonad.Coideal
-- Copyright   :  (C) 2008 Edward Kmett, (C) 2024 Koji Miyazato
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Koji Miyazato <viercc@gmail.com>
-- Stability   :  experimental
module Control.Comonad.Coideal
  ( -- * Coideal Comonads
    ComonadCoideal (..),
    Coideal(..),
    buildCoideal,

    -- * Mutual recursion for (co)ideal (co)monad (co)products
    Mutual (..),

    -- * Coideal Comonad Product
    (:*)(..),
    project1, project2,
    (&&&&)
  )
where

import Control.Arrow ((&&&))
import Control.Comonad

import Control.Functor.Internal.Mutual
import Data.Bifoldable (bifoldMap)
import Data.Bitraversable (bitraverse)

newtype Coideal f a = Coideal { forall (f :: * -> *) a. Coideal f a -> (a, f a)
runCoideal :: (a, f a) }
  deriving ((forall a b. (a -> b) -> Coideal f a -> Coideal f b)
-> (forall a b. a -> Coideal f b -> Coideal f a)
-> Functor (Coideal f)
forall a b. a -> Coideal f b -> Coideal f a
forall a b. (a -> b) -> Coideal f a -> Coideal f b
forall (f :: * -> *) a b.
Functor f =>
a -> Coideal f b -> Coideal f a
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Coideal f a -> Coideal f b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Coideal f a -> Coideal f b
fmap :: forall a b. (a -> b) -> Coideal f a -> Coideal f b
$c<$ :: forall (f :: * -> *) a b.
Functor f =>
a -> Coideal f b -> Coideal f a
<$ :: forall a b. a -> Coideal f b -> Coideal f a
Functor, (forall m. Monoid m => Coideal f m -> m)
-> (forall m a. Monoid m => (a -> m) -> Coideal f a -> m)
-> (forall m a. Monoid m => (a -> m) -> Coideal f a -> m)
-> (forall a b. (a -> b -> b) -> b -> Coideal f a -> b)
-> (forall a b. (a -> b -> b) -> b -> Coideal f a -> b)
-> (forall b a. (b -> a -> b) -> b -> Coideal f a -> b)
-> (forall b a. (b -> a -> b) -> b -> Coideal f a -> b)
-> (forall a. (a -> a -> a) -> Coideal f a -> a)
-> (forall a. (a -> a -> a) -> Coideal f a -> a)
-> (forall a. Coideal f a -> [a])
-> (forall a. Coideal f a -> Bool)
-> (forall a. Coideal f a -> Int)
-> (forall a. Eq a => a -> Coideal f a -> Bool)
-> (forall a. Ord a => Coideal f a -> a)
-> (forall a. Ord a => Coideal f a -> a)
-> (forall a. Num a => Coideal f a -> a)
-> (forall a. Num a => Coideal f a -> a)
-> Foldable (Coideal f)
forall a. Eq a => a -> Coideal f a -> Bool
forall a. Num a => Coideal f a -> a
forall a. Ord a => Coideal f a -> a
forall m. Monoid m => Coideal f m -> m
forall a. Coideal f a -> Bool
forall a. Coideal f a -> Int
forall a. Coideal f a -> [a]
forall a. (a -> a -> a) -> Coideal f a -> a
forall m a. Monoid m => (a -> m) -> Coideal f a -> m
forall b a. (b -> a -> b) -> b -> Coideal f a -> b
forall a b. (a -> b -> b) -> b -> Coideal f a -> b
forall (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> Coideal f a -> Bool
forall (f :: * -> *) a. (Foldable f, Num a) => Coideal f a -> a
forall (f :: * -> *) a. (Foldable f, Ord a) => Coideal f a -> a
forall (f :: * -> *) m. (Foldable f, Monoid m) => Coideal f m -> m
forall (f :: * -> *) a. Foldable f => Coideal f a -> Bool
forall (f :: * -> *) a. Foldable f => Coideal f a -> Int
forall (f :: * -> *) a. Foldable f => Coideal f a -> [a]
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Coideal f a -> a
forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Coideal f a -> m
forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Coideal f a -> b
forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Coideal f a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall (f :: * -> *) m. (Foldable f, Monoid m) => Coideal f m -> m
fold :: forall m. Monoid m => Coideal f m -> m
$cfoldMap :: forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Coideal f a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Coideal f a -> m
$cfoldMap' :: forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Coideal f a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Coideal f a -> m
$cfoldr :: forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Coideal f a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Coideal f a -> b
$cfoldr' :: forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Coideal f a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Coideal f a -> b
$cfoldl :: forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Coideal f a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Coideal f a -> b
$cfoldl' :: forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Coideal f a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Coideal f a -> b
$cfoldr1 :: forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Coideal f a -> a
foldr1 :: forall a. (a -> a -> a) -> Coideal f a -> a
$cfoldl1 :: forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Coideal f a -> a
foldl1 :: forall a. (a -> a -> a) -> Coideal f a -> a
$ctoList :: forall (f :: * -> *) a. Foldable f => Coideal f a -> [a]
toList :: forall a. Coideal f a -> [a]
$cnull :: forall (f :: * -> *) a. Foldable f => Coideal f a -> Bool
null :: forall a. Coideal f a -> Bool
$clength :: forall (f :: * -> *) a. Foldable f => Coideal f a -> Int
length :: forall a. Coideal f a -> Int
$celem :: forall (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> Coideal f a -> Bool
elem :: forall a. Eq a => a -> Coideal f a -> Bool
$cmaximum :: forall (f :: * -> *) a. (Foldable f, Ord a) => Coideal f a -> a
maximum :: forall a. Ord a => Coideal f a -> a
$cminimum :: forall (f :: * -> *) a. (Foldable f, Ord a) => Coideal f a -> a
minimum :: forall a. Ord a => Coideal f a -> a
$csum :: forall (f :: * -> *) a. (Foldable f, Num a) => Coideal f a -> a
sum :: forall a. Num a => Coideal f a -> a
$cproduct :: forall (f :: * -> *) a. (Foldable f, Num a) => Coideal f a -> a
product :: forall a. Num a => Coideal f a -> a
Foldable, Functor (Coideal f)
Foldable (Coideal f)
(Functor (Coideal f), Foldable (Coideal f)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Coideal f a -> f (Coideal f b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Coideal f (f a) -> f (Coideal f a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Coideal f a -> m (Coideal f b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Coideal f (m a) -> m (Coideal f a))
-> Traversable (Coideal f)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (f :: * -> *). Traversable f => Functor (Coideal f)
forall (f :: * -> *). Traversable f => Foldable (Coideal f)
forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
Coideal f (m a) -> m (Coideal f a)
forall (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
Coideal f (f a) -> f (Coideal f a)
forall (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Coideal f a -> m (Coideal f b)
forall (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Coideal f a -> f (Coideal f b)
forall (m :: * -> *) a.
Monad m =>
Coideal f (m a) -> m (Coideal f a)
forall (f :: * -> *) a.
Applicative f =>
Coideal f (f a) -> f (Coideal f a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Coideal f a -> m (Coideal f b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Coideal f a -> f (Coideal f b)
$ctraverse :: forall (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Coideal f a -> f (Coideal f b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Coideal f a -> f (Coideal f b)
$csequenceA :: forall (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
Coideal f (f a) -> f (Coideal f a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Coideal f (f a) -> f (Coideal f a)
$cmapM :: forall (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Coideal f a -> m (Coideal f b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Coideal f a -> m (Coideal f b)
$csequence :: forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
Coideal f (m a) -> m (Coideal f a)
sequence :: forall (m :: * -> *) a.
Monad m =>
Coideal f (m a) -> m (Coideal f a)
Traversable)

class (Functor w) => ComonadCoideal w where
  coidealExtend :: (Coideal w a -> b) -> w a -> w b

coidealize :: (ComonadCoideal w) => w a -> w (Coideal w a)
coidealize :: forall (w :: * -> *) a. ComonadCoideal w => w a -> w (Coideal w a)
coidealize = (Coideal w a -> Coideal w a) -> w a -> w (Coideal w a)
forall a b. (Coideal w a -> b) -> w a -> w b
forall (w :: * -> *) a b.
ComonadCoideal w =>
(Coideal w a -> b) -> w a -> w b
coidealExtend Coideal w a -> Coideal w a
forall a. a -> a
id

instance (ComonadCoideal w) => Comonad (Coideal w) where
  extract :: forall a. Coideal w a -> a
extract = (a, w a) -> a
forall a b. (a, b) -> a
fst ((a, w a) -> a) -> (Coideal w a -> (a, w a)) -> Coideal w a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coideal w a -> (a, w a)
forall (f :: * -> *) a. Coideal f a -> (a, f a)
runCoideal
  extend :: forall a b. (Coideal w a -> b) -> Coideal w a -> Coideal w b
extend Coideal w a -> b
f = (Coideal w a -> b) -> Coideal w (Coideal w a) -> Coideal w b
forall a b. (a -> b) -> Coideal w a -> Coideal w b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Coideal w a -> b
f (Coideal w (Coideal w a) -> Coideal w b)
-> (Coideal w a -> Coideal w (Coideal w a))
-> Coideal w a
-> Coideal w b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Coideal w a, w (Coideal w a)) -> Coideal w (Coideal w a)
forall (f :: * -> *) a. (a, f a) -> Coideal f a
Coideal ((Coideal w a, w (Coideal w a)) -> Coideal w (Coideal w a))
-> (Coideal w a -> (Coideal w a, w (Coideal w a)))
-> Coideal w a
-> Coideal w (Coideal w a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Coideal w a -> Coideal w a
forall a. a -> a
id (Coideal w a -> Coideal w a)
-> (Coideal w a -> w (Coideal w a))
-> Coideal w a
-> (Coideal w a, w (Coideal w a))
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& w a -> w (Coideal w a)
forall (w :: * -> *) a. ComonadCoideal w => w a -> w (Coideal w a)
coidealize (w a -> w (Coideal w a))
-> (Coideal w a -> w a) -> Coideal w a -> w (Coideal w a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, w a) -> w a
forall a b. (a, b) -> b
snd ((a, w a) -> w a)
-> (Coideal w a -> (a, w a)) -> Coideal w a -> w a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coideal w a -> (a, w a)
forall (f :: * -> *) a. Coideal f a -> (a, f a)
runCoideal)

buildCoideal :: (a -> w a) -> a -> Coideal w a
buildCoideal :: forall a (w :: * -> *). (a -> w a) -> a -> Coideal w a
buildCoideal a -> w a
phi = (a, w a) -> Coideal w a
forall (f :: * -> *) a. (a, f a) -> Coideal f a
Coideal ((a, w a) -> Coideal w a) -> (a -> (a, w a)) -> a -> Coideal w a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a
forall a. a -> a
id (a -> a) -> (a -> w a) -> a -> (a, w a)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& a -> w a
phi)

-- * (Co)ideal (Co)products

newtype (:*) w v a = CoidealProduct { forall (w :: * -> *) (v :: * -> *) a.
(:*) w v a -> (Mutual (,) w v a, Mutual (,) v w a)
runCoidealProduct :: (Mutual (,) w v a, Mutual (,) v w a) }
  deriving (forall a b. (a -> b) -> (:*) w v a -> (:*) w v b)
-> (forall a b. a -> (:*) w v b -> (:*) w v a) -> Functor (w :* v)
forall a b. a -> (:*) w v b -> (:*) w v a
forall a b. (a -> b) -> (:*) w v a -> (:*) w v b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (w :: * -> *) (v :: * -> *) a b.
(Functor w, Functor v) =>
a -> (:*) w v b -> (:*) w v a
forall (w :: * -> *) (v :: * -> *) a b.
(Functor w, Functor v) =>
(a -> b) -> (:*) w v a -> (:*) w v b
$cfmap :: forall (w :: * -> *) (v :: * -> *) a b.
(Functor w, Functor v) =>
(a -> b) -> (:*) w v a -> (:*) w v b
fmap :: forall a b. (a -> b) -> (:*) w v a -> (:*) w v b
$c<$ :: forall (w :: * -> *) (v :: * -> *) a b.
(Functor w, Functor v) =>
a -> (:*) w v b -> (:*) w v a
<$ :: forall a b. a -> (:*) w v b -> (:*) w v a
Functor

deriving instance
  (
    Eq (m0 ((,) a (Mutual (,) n0 m0 a))),
    Eq (n0 ((,) a (Mutual (,) m0 n0 a)))
  ) => Eq ((:*) m0 n0 a)
deriving instance
  (
    Show (m0 ((,) a (Mutual (,) n0 m0 a))),
    Show (n0 ((,) a (Mutual (,) m0 n0 a)))
  ) => Show ((:*) m0 n0 a)

instance (Foldable m0, Foldable n0) => Foldable (m0 :* n0) where
  foldMap :: forall m a. Monoid m => (a -> m) -> (:*) m0 n0 a -> m
foldMap a -> m
f = (Mutual (,) m0 n0 a -> m)
-> (Mutual (,) n0 m0 a -> m)
-> (Mutual (,) m0 n0 a, Mutual (,) n0 m0 a)
-> m
forall m a b. Monoid m => (a -> m) -> (b -> m) -> (a, b) -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap ((a -> m) -> Mutual (,) m0 n0 a -> m
forall m a. Monoid m => (a -> m) -> Mutual (,) m0 n0 a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f) ((a -> m) -> Mutual (,) n0 m0 a -> m
forall m a. Monoid m => (a -> m) -> Mutual (,) n0 m0 a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f) ((Mutual (,) m0 n0 a, Mutual (,) n0 m0 a) -> m)
-> ((:*) m0 n0 a -> (Mutual (,) m0 n0 a, Mutual (,) n0 m0 a))
-> (:*) m0 n0 a
-> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:*) m0 n0 a -> (Mutual (,) m0 n0 a, Mutual (,) n0 m0 a)
forall (w :: * -> *) (v :: * -> *) a.
(:*) w v a -> (Mutual (,) w v a, Mutual (,) v w a)
runCoidealProduct

instance (Traversable m0, Traversable n0) => Traversable (m0 :* n0) where
  traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (:*) m0 n0 a -> f ((:*) m0 n0 b)
traverse a -> f b
f = ((Mutual (,) m0 n0 b, Mutual (,) n0 m0 b) -> (:*) m0 n0 b)
-> f (Mutual (,) m0 n0 b, Mutual (,) n0 m0 b) -> f ((:*) m0 n0 b)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Mutual (,) m0 n0 b, Mutual (,) n0 m0 b) -> (:*) m0 n0 b
forall (w :: * -> *) (v :: * -> *) a.
(Mutual (,) w v a, Mutual (,) v w a) -> (:*) w v a
CoidealProduct (f (Mutual (,) m0 n0 b, Mutual (,) n0 m0 b) -> f ((:*) m0 n0 b))
-> ((:*) m0 n0 a -> f (Mutual (,) m0 n0 b, Mutual (,) n0 m0 b))
-> (:*) m0 n0 a
-> f ((:*) m0 n0 b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Mutual (,) m0 n0 a -> f (Mutual (,) m0 n0 b))
-> (Mutual (,) n0 m0 a -> f (Mutual (,) n0 m0 b))
-> (Mutual (,) m0 n0 a, Mutual (,) n0 m0 a)
-> f (Mutual (,) m0 n0 b, Mutual (,) n0 m0 b)
forall (f :: * -> *) a c b d.
Applicative f =>
(a -> f c) -> (b -> f d) -> (a, b) -> f (c, d)
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse ((a -> f b) -> Mutual (,) m0 n0 a -> f (Mutual (,) m0 n0 b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Mutual (,) m0 n0 a -> f (Mutual (,) m0 n0 b)
traverse a -> f b
f) ((a -> f b) -> Mutual (,) n0 m0 a -> f (Mutual (,) n0 m0 b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Mutual (,) n0 m0 a -> f (Mutual (,) n0 m0 b)
traverse a -> f b
f) ((Mutual (,) m0 n0 a, Mutual (,) n0 m0 a)
 -> f (Mutual (,) m0 n0 b, Mutual (,) n0 m0 b))
-> ((:*) m0 n0 a -> (Mutual (,) m0 n0 a, Mutual (,) n0 m0 a))
-> (:*) m0 n0 a
-> f (Mutual (,) m0 n0 b, Mutual (,) n0 m0 b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:*) m0 n0 a -> (Mutual (,) m0 n0 a, Mutual (,) n0 m0 a)
forall (w :: * -> *) (v :: * -> *) a.
(:*) w v a -> (Mutual (,) w v a, Mutual (,) v w a)
runCoidealProduct

project1 :: (Functor w) => (w :* v) a -> w a
project1 :: forall (w :: * -> *) (v :: * -> *) a.
Functor w =>
(:*) w v a -> w a
project1 = ((a, Mutual (,) v w a) -> a) -> w (a, Mutual (,) v w a) -> w a
forall a b. (a -> b) -> w a -> w b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, Mutual (,) v w a) -> a
forall a b. (a, b) -> a
fst (w (a, Mutual (,) v w a) -> w a)
-> ((:*) w v a -> w (a, Mutual (,) v w a)) -> (:*) w v a -> w a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mutual (,) w v a -> w (a, Mutual (,) v w a)
forall (p :: * -> * -> *) (m :: * -> *) (n :: * -> *) a.
Mutual p m n a -> m (p a (Mutual p n m a))
runMutual (Mutual (,) w v a -> w (a, Mutual (,) v w a))
-> ((:*) w v a -> Mutual (,) w v a)
-> (:*) w v a
-> w (a, Mutual (,) v w a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Mutual (,) w v a, Mutual (,) v w a) -> Mutual (,) w v a
forall a b. (a, b) -> a
fst ((Mutual (,) w v a, Mutual (,) v w a) -> Mutual (,) w v a)
-> ((:*) w v a -> (Mutual (,) w v a, Mutual (,) v w a))
-> (:*) w v a
-> Mutual (,) w v a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:*) w v a -> (Mutual (,) w v a, Mutual (,) v w a)
forall (w :: * -> *) (v :: * -> *) a.
(:*) w v a -> (Mutual (,) w v a, Mutual (,) v w a)
runCoidealProduct

project2 :: (Functor v) => (w :* v) a -> v a
project2 :: forall (v :: * -> *) (w :: * -> *) a.
Functor v =>
(:*) w v a -> v a
project2 = ((a, Mutual (,) w v a) -> a) -> v (a, Mutual (,) w v a) -> v a
forall a b. (a -> b) -> v a -> v b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, Mutual (,) w v a) -> a
forall a b. (a, b) -> a
fst (v (a, Mutual (,) w v a) -> v a)
-> ((:*) w v a -> v (a, Mutual (,) w v a)) -> (:*) w v a -> v a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mutual (,) v w a -> v (a, Mutual (,) w v a)
forall (p :: * -> * -> *) (m :: * -> *) (n :: * -> *) a.
Mutual p m n a -> m (p a (Mutual p n m a))
runMutual (Mutual (,) v w a -> v (a, Mutual (,) w v a))
-> ((:*) w v a -> Mutual (,) v w a)
-> (:*) w v a
-> v (a, Mutual (,) w v a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Mutual (,) w v a, Mutual (,) v w a) -> Mutual (,) v w a
forall a b. (a, b) -> b
snd ((Mutual (,) w v a, Mutual (,) v w a) -> Mutual (,) v w a)
-> ((:*) w v a -> (Mutual (,) w v a, Mutual (,) v w a))
-> (:*) w v a
-> Mutual (,) v w a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:*) w v a -> (Mutual (,) w v a, Mutual (,) v w a)
forall (w :: * -> *) (v :: * -> *) a.
(:*) w v a -> (Mutual (,) w v a, Mutual (,) v w a)
runCoidealProduct

instance (ComonadCoideal w, ComonadCoideal v) => ComonadCoideal (w :* v) where
  coidealExtend :: forall a b. (Coideal (w :* v) a -> b) -> (:*) w v a -> (:*) w v b
coidealExtend Coideal (w :* v) a -> b
k (CoidealProduct (Mutual (,) w v a
wv, Mutual (,) v w a
vw)) = (Mutual (,) w v b, Mutual (,) v w b) -> (:*) w v b
forall (w :: * -> *) (v :: * -> *) a.
(Mutual (,) w v a, Mutual (,) v w a) -> (:*) w v a
CoidealProduct ((Coideal (w :* v) a -> b) -> Mutual (,) w v a -> Mutual (,) w v b
forall (w :: * -> *) (v :: * -> *) a b.
(ComonadCoideal w, ComonadCoideal v) =>
(Coideal (w :* v) a -> b) -> Mutual (,) w v a -> Mutual (,) w v b
extendMutual1 Coideal (w :* v) a -> b
k Mutual (,) w v a
wv, (Coideal (w :* v) a -> b) -> Mutual (,) v w a -> Mutual (,) v w b
forall (w :: * -> *) (v :: * -> *) a b.
(ComonadCoideal w, ComonadCoideal v) =>
(Coideal (v :* w) a -> b) -> Mutual (,) w v a -> Mutual (,) w v b
extendMutual2 Coideal (w :* v) a -> b
k Mutual (,) v w a
vw)

extendMutual1 ::
  (ComonadCoideal w, ComonadCoideal v) =>
  (Coideal (w :* v) a -> b) ->
  Mutual (,) w v a ->
  Mutual (,) w v b
extendMutual1 :: forall (w :: * -> *) (v :: * -> *) a b.
(ComonadCoideal w, ComonadCoideal v) =>
(Coideal (w :* v) a -> b) -> Mutual (,) w v a -> Mutual (,) w v b
extendMutual1 Coideal (w :* v) a -> b
k (Mutual w (a, Mutual (,) v w a)
wv) =
  w (b, Mutual (,) v w b) -> Mutual (,) w v b
forall (p :: * -> * -> *) (m :: * -> *) (n :: * -> *) a.
m (p a (Mutual p n m a)) -> Mutual p m n a
Mutual (w (b, Mutual (,) v w b) -> Mutual (,) w v b)
-> w (b, Mutual (,) v w b) -> Mutual (,) w v b
forall a b. (a -> b) -> a -> b
$ (Coideal w (a, Mutual (,) v w a) -> (b, Mutual (,) v w b))
-> w (a, Mutual (,) v w a) -> w (b, Mutual (,) v w b)
forall a b. (Coideal w a -> b) -> w a -> w b
forall (w :: * -> *) a b.
ComonadCoideal w =>
(Coideal w a -> b) -> w a -> w b
coidealExtend (\(Coideal ((a
a, Mutual (,) v w a
vw), w (a, Mutual (,) v w a)
w')) -> (Coideal (w :* v) a -> b
k ((a, (:*) w v a) -> Coideal (w :* v) a
forall (f :: * -> *) a. (a, f a) -> Coideal f a
Coideal (a
a, (Mutual (,) w v a, Mutual (,) v w a) -> (:*) w v a
forall (w :: * -> *) (v :: * -> *) a.
(Mutual (,) w v a, Mutual (,) v w a) -> (:*) w v a
CoidealProduct (w (a, Mutual (,) v w a) -> Mutual (,) w v a
forall (p :: * -> * -> *) (m :: * -> *) (n :: * -> *) a.
m (p a (Mutual p n m a)) -> Mutual p m n a
Mutual w (a, Mutual (,) v w a)
w', Mutual (,) v w a
vw))), (Coideal (w :* v) a -> b) -> Mutual (,) v w a -> Mutual (,) v w b
forall (w :: * -> *) (v :: * -> *) a b.
(ComonadCoideal w, ComonadCoideal v) =>
(Coideal (v :* w) a -> b) -> Mutual (,) w v a -> Mutual (,) w v b
extendMutual2 Coideal (w :* v) a -> b
k Mutual (,) v w a
vw)) w (a, Mutual (,) v w a)
wv

extendMutual2 ::
  (ComonadCoideal w, ComonadCoideal v) =>
  (Coideal (v :* w) a -> b) ->
  Mutual (,) w v a ->
  Mutual (,) w v b
extendMutual2 :: forall (w :: * -> *) (v :: * -> *) a b.
(ComonadCoideal w, ComonadCoideal v) =>
(Coideal (v :* w) a -> b) -> Mutual (,) w v a -> Mutual (,) w v b
extendMutual2 Coideal (v :* w) a -> b
k (Mutual w (a, Mutual (,) v w a)
wv) =
  w (b, Mutual (,) v w b) -> Mutual (,) w v b
forall (p :: * -> * -> *) (m :: * -> *) (n :: * -> *) a.
m (p a (Mutual p n m a)) -> Mutual p m n a
Mutual (w (b, Mutual (,) v w b) -> Mutual (,) w v b)
-> w (b, Mutual (,) v w b) -> Mutual (,) w v b
forall a b. (a -> b) -> a -> b
$ (Coideal w (a, Mutual (,) v w a) -> (b, Mutual (,) v w b))
-> w (a, Mutual (,) v w a) -> w (b, Mutual (,) v w b)
forall a b. (Coideal w a -> b) -> w a -> w b
forall (w :: * -> *) a b.
ComonadCoideal w =>
(Coideal w a -> b) -> w a -> w b
coidealExtend (\(Coideal ((a
a, Mutual (,) v w a
vw), w (a, Mutual (,) v w a)
w')) -> (Coideal (v :* w) a -> b
k ((a, (:*) v w a) -> Coideal (v :* w) a
forall (f :: * -> *) a. (a, f a) -> Coideal f a
Coideal (a
a, (Mutual (,) v w a, Mutual (,) w v a) -> (:*) v w a
forall (w :: * -> *) (v :: * -> *) a.
(Mutual (,) w v a, Mutual (,) v w a) -> (:*) w v a
CoidealProduct (Mutual (,) v w a
vw, w (a, Mutual (,) v w a) -> Mutual (,) w v a
forall (p :: * -> * -> *) (m :: * -> *) (n :: * -> *) a.
m (p a (Mutual p n m a)) -> Mutual p m n a
Mutual w (a, Mutual (,) v w a)
w'))), (Coideal (v :* w) a -> b) -> Mutual (,) v w a -> Mutual (,) v w b
forall (w :: * -> *) (v :: * -> *) a b.
(ComonadCoideal w, ComonadCoideal v) =>
(Coideal (w :* v) a -> b) -> Mutual (,) w v a -> Mutual (,) w v b
extendMutual1 Coideal (v :* w) a -> b
k Mutual (,) v w a
vw)) w (a, Mutual (,) v w a)
wv

(&&&&) :: (ComonadCoideal s) => (forall a. s a -> w a) -> (forall a. s a -> v a) -> s b -> (w :* v) b
forall a. s a -> w a
tw &&&& :: forall (s :: * -> *) (w :: * -> *) (v :: * -> *) b.
ComonadCoideal s =>
(forall a. s a -> w a)
-> (forall a. s a -> v a) -> s b -> (:*) w v b
&&&& forall a. s a -> v a
tv = (Mutual (,) w v b, Mutual (,) v w b) -> (:*) w v b
forall (w :: * -> *) (v :: * -> *) a.
(Mutual (,) w v a, Mutual (,) v w a) -> (:*) w v a
CoidealProduct ((Mutual (,) w v b, Mutual (,) v w b) -> (:*) w v b)
-> (s b -> (Mutual (,) w v b, Mutual (,) v w b))
-> s b
-> (:*) w v b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((forall a. s a -> w a)
-> (forall a. s a -> v a) -> s b -> Mutual (,) w v b
forall (s :: * -> *) (w :: * -> *) (v :: * -> *) b.
ComonadCoideal s =>
(forall a. s a -> w a)
-> (forall a. s a -> v a) -> s b -> Mutual (,) w v b
unfoldMutual' s a -> w a
forall a. s a -> w a
tw s a -> v a
forall a. s a -> v a
tv (s b -> Mutual (,) w v b)
-> (s b -> Mutual (,) v w b)
-> s b
-> (Mutual (,) w v b, Mutual (,) v w b)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& (forall a. s a -> v a)
-> (forall a. s a -> w a) -> s b -> Mutual (,) v w b
forall (s :: * -> *) (w :: * -> *) (v :: * -> *) b.
ComonadCoideal s =>
(forall a. s a -> w a)
-> (forall a. s a -> v a) -> s b -> Mutual (,) w v b
unfoldMutual' s a -> v a
forall a. s a -> v a
tv s a -> w a
forall a. s a -> w a
tw)

unfoldMutual' :: (ComonadCoideal s) => (forall a. s a -> w a) -> (forall a. s a -> v a) -> s b -> Mutual (,) w v b
unfoldMutual' :: forall (s :: * -> *) (w :: * -> *) (v :: * -> *) b.
ComonadCoideal s =>
(forall a. s a -> w a)
-> (forall a. s a -> v a) -> s b -> Mutual (,) w v b
unfoldMutual' = (forall a b. ((a, s a) -> b) -> s a -> s b)
-> (forall a. s a -> w a)
-> (forall a. s a -> v a)
-> s b
-> Mutual (,) w v b
forall (p :: * -> * -> *) (s :: * -> *) (w :: * -> *) (v :: * -> *)
       c.
Bifunctor p =>
(forall a b. (p a (s a) -> b) -> s a -> s b)
-> (forall a. s a -> w a)
-> (forall a. s a -> v a)
-> s c
-> Mutual p w v c
unfoldMutual (\(a, s a) -> b
k s a
sa -> (Coideal s a -> b) -> s a -> s b
forall a b. (Coideal s a -> b) -> s a -> s b
forall (w :: * -> *) a b.
ComonadCoideal w =>
(Coideal w a -> b) -> w a -> w b
coidealExtend ((a, s a) -> b
k ((a, s a) -> b) -> (Coideal s a -> (a, s a)) -> Coideal s a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coideal s a -> (a, s a)
forall (f :: * -> *) a. Coideal f a -> (a, f a)
runCoideal) s a
sa)