{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

-- | Comonads in the cateogory of @Functor@s.
module FComonad
  ( type (~>),
    FFunctor (..),
    FComonad (..),
    fduplicate
  ) where

import Control.Comonad

import Data.Functor.Product
import Data.Functor.Compose
import qualified Data.Bifunctor.Sum as Bi
import Control.Comonad.Trans.Identity
import Control.Comonad.Env ( EnvT(..) )
import Control.Comonad.Traced (TracedT(..))
import Control.Comonad.Cofree (Cofree(..))
import qualified Control.Comonad.Cofree as Cofree

import FFunctor
import Data.Coerce (coerce)

-- | @FComonad@ is to 'FFunctor' what 'Comonad' is to 'Functor'.
class FFunctor ff => FComonad ff where
    fextract :: Functor g => ff g ~> g
    fextend :: (Functor g, Functor h) => (ff g ~> h) -> (ff g ~> ff h)

fduplicate :: (FComonad ff, Functor g) => ff g ~> ff (ff g)
fduplicate :: forall (ff :: FF) (g :: * -> *).
(FComonad ff, Functor g) =>
ff g ~> ff (ff g)
fduplicate = (ff g ~> ff g) -> ff g ~> ff (ff g)
forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(ff g ~> h) -> ff g ~> ff h
forall (ff :: FF) (g :: * -> *) (h :: * -> *).
(FComonad ff, Functor g, Functor h) =>
(ff g ~> h) -> ff g ~> ff h
fextend ff g x -> ff g x
forall a. a -> a
ff g ~> ff g
id

instance FComonad IdentityT where
    fextract :: forall (g :: * -> *). Functor g => IdentityT g ~> g
fextract = IdentityT g x -> g x
forall a b. Coercible a b => a -> b
coerce
    fextend :: forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(IdentityT g ~> h) -> IdentityT g ~> IdentityT h
fextend IdentityT g ~> h
tr = h x -> IdentityT h x
forall a b. Coercible a b => a -> b
coerce (h x -> IdentityT h x)
-> (IdentityT g x -> h x) -> IdentityT g x -> IdentityT h x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IdentityT g x -> h x
IdentityT g ~> h
tr

instance Functor f => FComonad (Product f) where
    fextract :: forall (g :: * -> *). Functor g => Product f g ~> g
fextract (Pair f x
_ g x
g) = g x
g
    fextend :: forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(Product f g ~> h) -> Product f g ~> Product f h
fextend Product f g ~> h
tr fg :: Product f g x
fg@(Pair f x
f g x
_) = f x -> h x -> Product f h x
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair f x
f (Product f g x -> h x
Product f g ~> h
tr Product f g x
fg)

instance Comonad f => FComonad (Compose f) where
    fextract :: forall (g :: * -> *). Functor g => Compose f g ~> g
fextract = f (g x) -> g x
forall a. f a -> a
forall (w :: * -> *) a. Comonad w => w a -> a
extract (f (g x) -> g x)
-> (Compose f g x -> f (g x)) -> Compose f g x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f g x -> f (g x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose
    fextend :: forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(Compose f g ~> h) -> Compose f g ~> Compose f h
fextend Compose f g ~> h
tr = f (h x) -> Compose f h x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (h x) -> Compose f h x)
-> (Compose f g x -> f (h x)) -> Compose f g x -> Compose f h x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (g x) -> h x) -> f (g x) -> f (h x)
forall a b. (f a -> b) -> f a -> f b
forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend (Compose f g x -> h x
Compose f g ~> h
tr (Compose f g x -> h x)
-> (f (g x) -> Compose f g x) -> f (g x) -> h x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (g x) -> Compose f g x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose) (f (g x) -> f (h x))
-> (Compose f g x -> f (g x)) -> Compose f g x -> f (h x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f g x -> f (g x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose

instance (FComonad ff, FComonad gg) => FComonad (Bi.Sum ff gg) where
    fextract :: forall (g :: * -> *). Functor g => Sum ff gg g ~> g
fextract (Bi.L2 ff g x
ffx) = ff g x -> g x
ff g ~> g
forall (g :: * -> *). Functor g => ff g ~> g
forall (ff :: FF) (g :: * -> *).
(FComonad ff, Functor g) =>
ff g ~> g
fextract ff g x
ffx
    fextract (Bi.R2 gg g x
ggx) = gg g x -> g x
gg g ~> g
forall (g :: * -> *). Functor g => gg g ~> g
forall (ff :: FF) (g :: * -> *).
(FComonad ff, Functor g) =>
ff g ~> g
fextract gg g x
ggx

    fextend :: forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(Sum ff gg g ~> h) -> Sum ff gg g ~> Sum ff gg h
fextend Sum ff gg g ~> h
tr Sum ff gg g x
ffgg = case Sum ff gg g x
ffgg of
      Bi.L2 ff g x
ffx -> ff h x -> Sum ff gg h x
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
p a b -> Sum p q a b
Bi.L2 ((ff g ~> h) -> ff g ~> ff h
forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(ff g ~> h) -> ff g ~> ff h
forall (ff :: FF) (g :: * -> *) (h :: * -> *).
(FComonad ff, Functor g, Functor h) =>
(ff g ~> h) -> ff g ~> ff h
fextend (Sum ff gg g x -> h x
Sum ff gg g ~> h
tr (Sum ff gg g x -> h x)
-> (ff g x -> Sum ff gg g x) -> ff g x -> h x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ff g x -> Sum ff gg g x
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
p a b -> Sum p q a b
Bi.L2) ff g x
ffx)
      Bi.R2 gg g x
ggx -> gg h x -> Sum ff gg h x
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
q a b -> Sum p q a b
Bi.R2 ((gg g ~> h) -> gg g ~> gg h
forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(gg g ~> h) -> gg g ~> gg h
forall (ff :: FF) (g :: * -> *) (h :: * -> *).
(FComonad ff, Functor g, Functor h) =>
(ff g ~> h) -> ff g ~> ff h
fextend (Sum ff gg g x -> h x
Sum ff gg g ~> h
tr (Sum ff gg g x -> h x)
-> (gg g x -> Sum ff gg g x) -> gg g x -> h x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. gg g x -> Sum ff gg g x
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
q a b -> Sum p q a b
Bi.R2) gg g x
ggx)

instance FComonad (EnvT e) where
  fextract :: forall (g :: * -> *). Functor g => EnvT e g ~> g
fextract (EnvT e
_ g x
gx) = g x
gx
  fextend :: forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(EnvT e g ~> h) -> EnvT e g ~> EnvT e h
fextend EnvT e g ~> h
tr eg :: EnvT e g x
eg@(EnvT e
e g x
_) = e -> h x -> EnvT e h x
forall e (w :: * -> *) a. e -> w a -> EnvT e w a
EnvT e
e (EnvT e g x -> h x
EnvT e g ~> h
tr EnvT e g x
eg)

instance Monoid m => FComonad (TracedT m) where
  fextract :: forall (g :: * -> *). Functor g => TracedT m g ~> g
fextract (TracedT g (m -> x)
g) = ((m -> x) -> m -> x
forall a b. (a -> b) -> a -> b
$ m
forall a. Monoid a => a
mempty) ((m -> x) -> x) -> g (m -> x) -> g x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g (m -> x)
g
  fextend :: forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(TracedT m g ~> h) -> TracedT m g ~> TracedT m h
fextend TracedT m g ~> h
tr (TracedT g (m -> x)
g) = h (m -> x) -> TracedT m h x
forall m (w :: * -> *) a. w (m -> a) -> TracedT m w a
TracedT (h (m -> x) -> TracedT m h x) -> h (m -> x) -> TracedT m h x
forall a b. (a -> b) -> a -> b
$ TracedT m g (m -> x) -> h (m -> x)
TracedT m g ~> h
tr (g (m -> m -> x) -> TracedT m g (m -> x)
forall m (w :: * -> *) a. w (m -> a) -> TracedT m w a
TracedT (g (m -> m -> x) -> TracedT m g (m -> x))
-> g (m -> m -> x) -> TracedT m g (m -> x)
forall a b. (a -> b) -> a -> b
$ ((m -> x) -> m -> m -> x) -> g (m -> x) -> g (m -> m -> x)
forall a b. (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\m -> x
k m
m1 m
m2 -> m -> x
k (m
m1 m -> m -> m
forall a. Semigroup a => a -> a -> a
<> m
m2)) g (m -> x)
g)

instance FComonad Cofree where
  fextract :: Functor g => Cofree g ~> g
  fextract :: forall (g :: * -> *). Functor g => Cofree g ~> g
fextract = (Cofree g x -> x) -> g (Cofree g x) -> g x
forall a b. (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Cofree g x -> x
forall a. Cofree g a -> a
forall (w :: * -> *) a. Comonad w => w a -> a
extract (g (Cofree g x) -> g x)
-> (Cofree g x -> g (Cofree g x)) -> Cofree g x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cofree g x -> g (Cofree g x)
forall a. Cofree g a -> g (Cofree g a)
forall (f :: * -> *) (w :: * -> *) a.
ComonadCofree f w =>
w a -> f (w a)
Cofree.unwrap

  fextend :: (Functor g, Functor h) => (Cofree g ~> h) -> (Cofree g ~> Cofree h)
  fextend :: forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(Cofree g ~> h) -> Cofree g ~> Cofree h
fextend Cofree g ~> h
tr = (Cofree g ~> h) -> Cofree (Cofree g) x -> Cofree h x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> Cofree g x -> Cofree h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap Cofree g x -> h x
Cofree g ~> h
tr (Cofree (Cofree g) x -> Cofree h x)
-> (Cofree g x -> Cofree (Cofree g) x) -> Cofree g x -> Cofree h x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cofree g x -> Cofree (Cofree g) x
forall (f :: * -> *) a. Comonad f => f a -> Cofree f a
Cofree.section

  {-
  
  fextract $ fduplicate gs
    = fextract $ extract gs :< fmap fduplicate_ (duplicate gs)
    = fmap extract (fmap fduplicate_ (duplicate gs))
    = fmap (extract . fduplicate_) (duplicate gs)
    = fmap extract (duplicate gs)
    = gs
  
  ffmap fextract $ fduplicate gs
    = ffmap fextract $ extract gs :< fmap fduplicate_ (duplicate gs)
    = extract gs :< (fmap (ffmap fextract) . fextract . fmap fduplicate_) (duplicate gs)
    = extract gs :< (fmap (ffmap fextract . fduplicate_) . fextract) (duplicate gs)
      -- gs = (a :< gs')
    = extract (a :< gs') :< fmap (ffmap fextract . fduplicate_) (fextract (duplicate (a :< gs')))
    = a :< fmap (ffmap fextract . fduplicate_) (fextract ((a :< gs') :< fmap duplicate gs'))
    = a :< fmap (ffmap fextract . fduplicate_) (fmap extract (fmap duplicate gs'))
    = a :< fmap (ffmap fextract . fduplicate_) gs'
  ffmap fextract . fduplicate_
    = let go (a :< gs) = a :< fmap go gs
       in go
    = id
  
  -}