{-# LANGUAGE
    GADTs
  , RankNTypes
  , TypeOperators
  , ConstraintKinds
  , FlexibleContexts
  , FlexibleInstances
  , ScopedTypeVariables
  , UndecidableInstances
  , MultiParamTypeClasses
  , QuantifiedConstraints
  #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Functor.HHCofree
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-- A cofree functor is right adjoint to a forgetful functor.
-- In this package the forgetful functor forgets class constraints.
--
-- Compared to @Data.Functor.HCofree@ we have 2 two parameters.
-----------------------------------------------------------------------------
module Data.Functor.HHCofree where

import Prelude hiding ((.), id)

import Control.Category
import Data.Bifunctor
import Data.Bifunctor.Functor
import Data.Profunctor
import Data.Profunctor.Unsafe
import Data.Profunctor.Monad


-- | Natural transformations.
type f :~~> g = forall c d. f c d -> g c d

-- | The higher order cofree functor for constraint @c@.
data HHCofree c g a b where
  HHCofree :: c f => (f :~~> g) -> f a b -> HHCofree c g a b


counit :: HHCofree c g :~~> g
counit :: HHCofree c g c d -> g c d
counit (HHCofree f :~~> g
k f c d
fa) = f c d -> g c d
f :~~> g
k f c d
fa

leftAdjunct :: c f => (f :~~> g) -> f :~~> HHCofree c g
leftAdjunct :: (f :~~> g) -> f :~~> HHCofree c g
leftAdjunct = (f :~~> g) -> f c d -> HHCofree c g c d
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
       (g :: * -> * -> *) a b.
c f =>
(f :~~> g) -> f a b -> HHCofree c g a b
HHCofree

-- | @unit = leftAdjunct id@
unit :: c g => g :~~> HHCofree c g
unit :: g :~~> HHCofree c g
unit = (g :~~> g) -> g :~~> HHCofree c g
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
       (g :: * -> * -> *).
c f =>
(f :~~> g) -> f :~~> HHCofree c g
leftAdjunct g :~~> g
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

-- | @rightAdjunct f = counit . f@
rightAdjunct :: (f :~~> HHCofree c g) -> f :~~> g
rightAdjunct :: (f :~~> HHCofree c g) -> f :~~> g
rightAdjunct f :~~> HHCofree c g
f = HHCofree c g c d -> g c d
forall (c :: (* -> * -> *) -> Constraint) (g :: * -> * -> *).
HHCofree c g :~~> g
counit (HHCofree c g c d -> g c d)
-> (f c d -> HHCofree c g c d) -> f c d -> g c d
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f c d -> HHCofree c g c d
f :~~> HHCofree c g
f

transform :: (forall r. c r => (r :~~> f) -> r :~~> g) -> HHCofree c f :~~> HHCofree c g
transform :: (forall (r :: * -> * -> *). c r => (r :~~> f) -> r :~~> g)
-> HHCofree c f :~~> HHCofree c g
transform forall (r :: * -> * -> *). c r => (r :~~> f) -> r :~~> g
t (HHCofree f :~~> f
k f c d
a) = (f :~~> g) -> f c d -> HHCofree c g c d
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
       (g :: * -> * -> *) a b.
c f =>
(f :~~> g) -> f a b -> HHCofree c g a b
HHCofree ((f :~~> f) -> f :~~> g
forall (r :: * -> * -> *). c r => (r :~~> f) -> r :~~> g
t f :~~> f
k) f c d
a

hfmap :: (f :~~> g) -> HHCofree c f :~~> HHCofree c g
hfmap :: (f :~~> g) -> HHCofree c f :~~> HHCofree c g
hfmap f :~~> g
f = (forall (r :: * -> * -> *). c r => (r :~~> f) -> r :~~> g)
-> HHCofree c f :~~> HHCofree c g
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
       (g :: * -> * -> *).
(forall (r :: * -> * -> *). c r => (r :~~> f) -> r :~~> g)
-> HHCofree c f :~~> HHCofree c g
transform (f c d -> g c d
f :~~> g
f (f c d -> g c d) -> (r c d -> f c d) -> r c d -> g c d
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.)

hextend :: (HHCofree c f :~~> g) -> HHCofree c f :~~> HHCofree c g
hextend :: (HHCofree c f :~~> g) -> HHCofree c f :~~> HHCofree c g
hextend HHCofree c f :~~> g
f = (forall (r :: * -> * -> *). c r => (r :~~> f) -> r :~~> g)
-> HHCofree c f :~~> HHCofree c g
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
       (g :: * -> * -> *).
(forall (r :: * -> * -> *). c r => (r :~~> f) -> r :~~> g)
-> HHCofree c f :~~> HHCofree c g
transform (\r :~~> f
k -> HHCofree c f c d -> g c d
HHCofree c f :~~> g
f (HHCofree c f c d -> g c d)
-> (r c d -> HHCofree c f c d) -> r c d -> g c d
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (r :~~> f) -> r :~~> HHCofree c f
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
       (g :: * -> * -> *).
c f =>
(f :~~> g) -> f :~~> HHCofree c g
leftAdjunct r :~~> f
k)


instance BifunctorFunctor (HHCofree c) where
  bifmap :: (p :-> q) -> HHCofree c p :-> HHCofree c q
bifmap = (p :-> q) -> HHCofree c p a b -> HHCofree c q a b
forall (f :: * -> * -> *) (g :: * -> * -> *)
       (c :: (* -> * -> *) -> Constraint).
(f :~~> g) -> HHCofree c f :~~> HHCofree c g
hfmap

instance BifunctorComonad (HHCofree c) where
  biextract :: HHCofree c p a b -> p a b
biextract = HHCofree c p a b -> p a b
forall (c :: (* -> * -> *) -> Constraint) (g :: * -> * -> *).
HHCofree c g :~~> g
counit
  biextend :: (HHCofree c p :-> q) -> HHCofree c p :-> HHCofree c q
biextend = (HHCofree c p :-> q) -> HHCofree c p a b -> HHCofree c q a b
forall (c :: (* -> * -> *) -> Constraint) (p :: * -> * -> *)
       (q :: * -> * -> *).
(HHCofree c p :-> q) -> HHCofree c p :-> HHCofree c q
hextend

instance ProfunctorFunctor (HHCofree c) where
  promap :: (p :-> q) -> HHCofree c p :-> HHCofree c q
promap = (p :-> q) -> HHCofree c p a b -> HHCofree c q a b
forall (f :: * -> * -> *) (g :: * -> * -> *)
       (c :: (* -> * -> *) -> Constraint).
(f :~~> g) -> HHCofree c f :~~> HHCofree c g
hfmap

instance ProfunctorComonad (HHCofree c) where
  proextract :: HHCofree c p :-> p
proextract = HHCofree c p a b -> p a b
forall (c :: (* -> * -> *) -> Constraint) (g :: * -> * -> *).
HHCofree c g :~~> g
counit
  produplicate :: HHCofree c p :-> HHCofree c (HHCofree c p)
produplicate = (HHCofree c p :~~> HHCofree c p)
-> HHCofree c p :-> HHCofree c (HHCofree c p)
forall (c :: (* -> * -> *) -> Constraint) (p :: * -> * -> *)
       (q :: * -> * -> *).
(HHCofree c p :-> q) -> HHCofree c p :-> HHCofree c q
hextend HHCofree c p :~~> HHCofree c p
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id


instance (forall x. c x => Bifunctor x) => Bifunctor (HHCofree c g) where
  bimap :: (a -> b) -> (c -> d) -> HHCofree c g a c -> HHCofree c g b d
bimap a -> b
f c -> d
g (HHCofree f :~~> g
k f a c
a) = (f :~~> g) -> f b d -> HHCofree c g b d
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
       (g :: * -> * -> *) a b.
c f =>
(f :~~> g) -> f a b -> HHCofree c g a b
HHCofree f :~~> g
k ((a -> b) -> (c -> d) -> f a c -> f b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
f c -> d
g f a c
a)
  first :: (a -> b) -> HHCofree c g a c -> HHCofree c g b c
first a -> b
f (HHCofree f :~~> g
k f a c
a) = (f :~~> g) -> f b c -> HHCofree c g b c
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
       (g :: * -> * -> *) a b.
c f =>
(f :~~> g) -> f a b -> HHCofree c g a b
HHCofree f :~~> g
k ((a -> b) -> f a c -> f b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first a -> b
f f a c
a)
  second :: (b -> c) -> HHCofree c g a b -> HHCofree c g a c
second b -> c
f (HHCofree f :~~> g
k f a b
a) = (f :~~> g) -> f a c -> HHCofree c g a c
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
       (g :: * -> * -> *) a b.
c f =>
(f :~~> g) -> f a b -> HHCofree c g a b
HHCofree f :~~> g
k ((b -> c) -> f a b -> f a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second b -> c
f f a b
a)

instance (forall x. c x => Profunctor x) => Profunctor (HHCofree c g) where
  dimap :: (a -> b) -> (c -> d) -> HHCofree c g b c -> HHCofree c g a d
dimap a -> b
f c -> d
g (HHCofree f :~~> g
k f b c
a) = (f :~~> g) -> f a d -> HHCofree c g a d
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
       (g :: * -> * -> *) a b.
c f =>
(f :~~> g) -> f a b -> HHCofree c g a b
HHCofree f :~~> g
k ((a -> b) -> (c -> d) -> f b c -> f a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap a -> b
f c -> d
g f b c
a)
  lmap :: (a -> b) -> HHCofree c g b c -> HHCofree c g a c
lmap a -> b
f (HHCofree f :~~> g
k f b c
a) = (f :~~> g) -> f a c -> HHCofree c g a c
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
       (g :: * -> * -> *) a b.
c f =>
(f :~~> g) -> f a b -> HHCofree c g a b
HHCofree f :~~> g
k ((a -> b) -> f b c -> f a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> b
f f b c
a)
  rmap :: (b -> c) -> HHCofree c g a b -> HHCofree c g a c
rmap b -> c
f (HHCofree f :~~> g
k f a b
a) = (f :~~> g) -> f a c -> HHCofree c g a c
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
       (g :: * -> * -> *) a b.
c f =>
(f :~~> g) -> f a b -> HHCofree c g a b
HHCofree f :~~> g
k ((b -> c) -> f a b -> f a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap b -> c
f f a b
a)
  q b c
f #. :: q b c -> HHCofree c g a b -> HHCofree c g a c
#. HHCofree f :~~> g
k f a b
g = (f :~~> g) -> f a c -> HHCofree c g a c
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
       (g :: * -> * -> *) a b.
c f =>
(f :~~> g) -> f a b -> HHCofree c g a b
HHCofree f :~~> g
k (q b c
f q b c -> f a b -> f a c
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a c
#. f a b
g)
  HHCofree f :~~> g
k f b c
g .# :: HHCofree c g b c -> q a b -> HHCofree c g a c
.# q a b
f = (f :~~> g) -> f a c -> HHCofree c g a c
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
       (g :: * -> * -> *) a b.
c f =>
(f :~~> g) -> f a b -> HHCofree c g a b
HHCofree f :~~> g
k (f b c
g f b c -> q a b -> f a c
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
p b c -> q a b -> p a c
.# q a b
f)

instance (forall x. c x => Strong x) => Strong (HHCofree c f) where
  first' :: HHCofree c f a b -> HHCofree c f (a, c) (b, c)
first' (HHCofree f :~~> f
k f a b
a) = (f :~~> f) -> f (a, c) (b, c) -> HHCofree c f (a, c) (b, c)
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
       (g :: * -> * -> *) a b.
c f =>
(f :~~> g) -> f a b -> HHCofree c g a b
HHCofree f :~~> f
k (f a b -> f (a, c) (b, c)
forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (a, c) (b, c)
first' f a b
a)
  second' :: HHCofree c f a b -> HHCofree c f (c, a) (c, b)
second' (HHCofree f :~~> f
k f a b
a) = (f :~~> f) -> f (c, a) (c, b) -> HHCofree c f (c, a) (c, b)
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
       (g :: * -> * -> *) a b.
c f =>
(f :~~> g) -> f a b -> HHCofree c g a b
HHCofree f :~~> f
k (f a b -> f (c, a) (c, b)
forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (c, a) (c, b)
second' f a b
a)

instance (forall x. c x => Choice x) => Choice (HHCofree c f) where
  left' :: HHCofree c f a b -> HHCofree c f (Either a c) (Either b c)
left' (HHCofree f :~~> f
k f a b
a) = (f :~~> f)
-> f (Either a c) (Either b c)
-> HHCofree c f (Either a c) (Either b c)
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
       (g :: * -> * -> *) a b.
c f =>
(f :~~> g) -> f a b -> HHCofree c g a b
HHCofree f :~~> f
k (f a b -> f (Either a c) (Either b c)
forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either a c) (Either b c)
left' f a b
a)
  right' :: HHCofree c f a b -> HHCofree c f (Either c a) (Either c b)
right' (HHCofree f :~~> f
k f a b
a) = (f :~~> f)
-> f (Either c a) (Either c b)
-> HHCofree c f (Either c a) (Either c b)
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
       (g :: * -> * -> *) a b.
c f =>
(f :~~> g) -> f a b -> HHCofree c g a b
HHCofree f :~~> f
k (f a b -> f (Either c a) (Either c b)
forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either c a) (Either c b)
right' f a b
a)

instance (forall x. c x => Closed x) => Closed (HHCofree c f) where
  closed :: HHCofree c f a b -> HHCofree c f (x -> a) (x -> b)
closed (HHCofree f :~~> f
k f a b
a) = (f :~~> f) -> f (x -> a) (x -> b) -> HHCofree c f (x -> a) (x -> b)
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
       (g :: * -> * -> *) a b.
c f =>
(f :~~> g) -> f a b -> HHCofree c g a b
HHCofree f :~~> f
k (f a b -> f (x -> a) (x -> b)
forall (p :: * -> * -> *) a b x.
Closed p =>
p a b -> p (x -> a) (x -> b)
closed f a b
a)