{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
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)
class FFunctor ff => FComonad ff where
:: 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