{-# LANGUAGE
    GADTs
  , RankNTypes
  , TypeOperators
  , ConstraintKinds
  , UndecidableInstances
  , QuantifiedConstraints
  #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Functor.HCofree
-- 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.Cofree@ we're going up a level.
-- These free functors go between categories of functors and the natural
-- transformations between them.
-----------------------------------------------------------------------------
module Data.Functor.HCofree where

import Control.Comonad
import Control.Comonad.Trans.Class
import Data.Foldable
import Data.Functor.Identity

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

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


counit :: HCofree c g :~> g
counit :: HCofree c g b -> g b
counit (HCofree f :~> g
k f b
fa) = f b -> g b
f :~> g
k f b
fa

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

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

-- | @rightAdjunct f = counit . f@
rightAdjunct :: (f :~> HCofree c g) -> f :~> g
rightAdjunct :: (f :~> HCofree c g) -> f :~> g
rightAdjunct f :~> HCofree c g
f = HCofree c g b -> g b
forall (c :: (* -> *) -> Constraint) (g :: * -> *).
HCofree c g :~> g
counit (HCofree c g b -> g b) -> (f b -> HCofree c g b) -> f b -> g b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f b -> HCofree c g b
f :~> HCofree c g
f

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

hfmap :: (f :~> g) -> HCofree c f :~> HCofree c g
hfmap :: (f :~> g) -> HCofree c f :~> HCofree c g
hfmap f :~> g
f = (forall (r :: * -> *). c r => (r :~> f) -> r :~> g)
-> HCofree c f :~> HCofree c g
forall (c :: (* -> *) -> Constraint) (f :: * -> *) (g :: * -> *).
(forall (r :: * -> *). c r => (r :~> f) -> r :~> g)
-> HCofree c f :~> HCofree c g
transform (f b -> g b
f :~> g
f (f b -> g b) -> (r b -> f b) -> r b -> g b
forall b c a. (b -> c) -> (a -> b) -> a -> c
.)

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

liftCofree :: c f => f a -> HCofree c f a
liftCofree :: f a -> HCofree c f a
liftCofree = (f :~> f) -> f :~> HCofree c f
forall (c :: (* -> *) -> Constraint) (f :: * -> *) (g :: * -> *).
c f =>
(f :~> g) -> f :~> HCofree c g
leftAdjunct forall a. a -> a
f :~> f
id

lowerCofree :: HCofree c f a -> f a
lowerCofree :: HCofree c f a -> f a
lowerCofree = HCofree c f a -> f a
forall (c :: (* -> *) -> Constraint) (g :: * -> *).
HCofree c g :~> g
counit

convert :: (c (t f), Comonad f, ComonadTrans t) => t f a -> HCofree c f a
convert :: t f a -> HCofree c f a
convert = (t f :~> f) -> t f :~> HCofree c f
forall (c :: (* -> *) -> Constraint) (f :: * -> *) (g :: * -> *).
c f =>
(f :~> g) -> f :~> HCofree c g
leftAdjunct t f :~> f
forall (t :: (* -> *) -> * -> *) (w :: * -> *) a.
(ComonadTrans t, Comonad w) =>
t w a -> w a
lower

coiter :: c Identity => (forall b. b -> f b) -> a -> HCofree c f a
coiter :: (forall b. b -> f b) -> a -> HCofree c f a
coiter forall b. b -> f b
f = (Identity :~> f) -> Identity :~> HCofree c f
forall (c :: (* -> *) -> Constraint) (f :: * -> *) (g :: * -> *).
c f =>
(f :~> g) -> f :~> HCofree c g
leftAdjunct (b -> f b
forall b. b -> f b
f (b -> f b) -> (Identity b -> b) -> Identity b -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity b -> b
forall a. Identity a -> a
runIdentity) (Identity a -> HCofree c f a)
-> (a -> Identity a) -> a -> HCofree c f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Identity a
forall a. a -> Identity a
Identity

unwrap :: HCofree Comonad g a -> g (HCofree Comonad g a)
unwrap :: HCofree Comonad g a -> g (HCofree Comonad g a)
unwrap = HCofree Comonad g (HCofree Comonad g a) -> g (HCofree Comonad g a)
forall (c :: (* -> *) -> Constraint) (g :: * -> *).
HCofree c g :~> g
counit (HCofree Comonad g (HCofree Comonad g a)
 -> g (HCofree Comonad g a))
-> (HCofree Comonad g a -> HCofree Comonad g (HCofree Comonad g a))
-> HCofree Comonad g a
-> g (HCofree Comonad g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HCofree Comonad g a -> HCofree Comonad g (HCofree Comonad g a)
forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate

instance (forall x. c x => Functor x) => Functor (HCofree c g) where
  fmap :: (a -> b) -> HCofree c g a -> HCofree c g b
fmap a -> b
f (HCofree f :~> g
k f a
a) = (f :~> g) -> f b -> HCofree c g b
forall (c :: (* -> *) -> Constraint) (f :: * -> *) (g :: * -> *) a.
c f =>
(f :~> g) -> f a -> HCofree c g a
HCofree f :~> g
k ((a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f f a
a)
  a
a <$ :: a -> HCofree c g b -> HCofree c g a
<$ HCofree f :~> g
k f b
b = (f :~> g) -> f a -> HCofree c g a
forall (c :: (* -> *) -> Constraint) (f :: * -> *) (g :: * -> *) a.
c f =>
(f :~> g) -> f a -> HCofree c g a
HCofree f :~> g
k (a
a a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f b
b)

instance (forall x. c x => Foldable x) => Foldable (HCofree c g) where
  foldMap :: (a -> m) -> HCofree c g a -> m
foldMap a -> m
f (HCofree f :~> g
_ f a
a) = (a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f f a
a
  foldMap' :: (a -> m) -> HCofree c g a -> m
foldMap' a -> m
f (HCofree f :~> g
_ f a
a) = (a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap' a -> m
f f a
a
  fold :: HCofree c g m -> m
fold (HCofree f :~> g
_ f m
a) = f m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold f m
a
  foldr :: (a -> b -> b) -> b -> HCofree c g a -> b
foldr a -> b -> b
f b
z (HCofree f :~> g
_ f a
a) = (a -> b -> b) -> b -> f a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
f b
z f a
a
  foldl :: (b -> a -> b) -> b -> HCofree c g a -> b
foldl b -> a -> b
f b
z (HCofree f :~> g
_ f a
a) = (b -> a -> b) -> b -> f a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl b -> a -> b
f b
z f a
a
  foldl' :: (b -> a -> b) -> b -> HCofree c g a -> b
foldl' b -> a -> b
f b
z (HCofree f :~> g
_ f a
a) = (b -> a -> b) -> b -> f a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' b -> a -> b
f b
z f a
a
  foldr1 :: (a -> a -> a) -> HCofree c g a -> a
foldr1 a -> a -> a
f (HCofree f :~> g
_ f a
a) = (a -> a -> a) -> f a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 a -> a -> a
f f a
a
  foldr' :: (a -> b -> b) -> b -> HCofree c g a -> b
foldr' a -> b -> b
f b
z (HCofree f :~> g
_ f a
a) = (a -> b -> b) -> b -> f a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr' a -> b -> b
f b
z f a
a
  foldl1 :: (a -> a -> a) -> HCofree c g a -> a
foldl1 a -> a -> a
f (HCofree f :~> g
_ f a
a) = (a -> a -> a) -> f a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 a -> a -> a
f f a
a
  toList :: HCofree c g a -> [a]
toList (HCofree f :~> g
_ f a
a) = f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList f a
a
  null :: HCofree c g a -> Bool
null (HCofree f :~> g
_ f a
a) = f a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null f a
a
  length :: HCofree c g a -> Int
length (HCofree f :~> g
_ f a
a) = f a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length f a
a
  elem :: a -> HCofree c g a -> Bool
elem a
e (HCofree f :~> g
_ f a
a) = a -> f a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
e f a
a
  maximum :: HCofree c g a -> a
maximum (HCofree f :~> g
_ f a
a) = f a -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum f a
a
  minimum :: HCofree c g a -> a
minimum (HCofree f :~> g
_ f a
a) = f a -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum f a
a
  sum :: HCofree c g a -> a
sum (HCofree f :~> g
_ f a
a) = f a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum f a
a
  product :: HCofree c g a -> a
product (HCofree f :~> g
_ f a
a) = f a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product f a
a

instance (forall x. c x => Traversable x) => Traversable (HCofree c g) where
  traverse :: (a -> f b) -> HCofree c g a -> f (HCofree c g b)
traverse a -> f b
f (HCofree f :~> g
k f a
a) = (f :~> g) -> f b -> HCofree c g b
forall (c :: (* -> *) -> Constraint) (f :: * -> *) (g :: * -> *) a.
c f =>
(f :~> g) -> f a -> HCofree c g a
HCofree f :~> g
k (f b -> HCofree c g b) -> f (f b) -> f (HCofree c g b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> f a -> f (f b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f f a
a
  sequenceA :: HCofree c g (f a) -> f (HCofree c g a)
sequenceA (HCofree f :~> g
k f (f a)
a) = (f :~> g) -> f a -> HCofree c g a
forall (c :: (* -> *) -> Constraint) (f :: * -> *) (g :: * -> *) a.
c f =>
(f :~> g) -> f a -> HCofree c g a
HCofree f :~> g
k (f a -> HCofree c g a) -> f (f a) -> f (HCofree c g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f a) -> f (f a)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA f (f a)
a
  mapM :: (a -> m b) -> HCofree c g a -> m (HCofree c g b)
mapM a -> m b
f (HCofree f :~> g
k f a
a) = (f :~> g) -> f b -> HCofree c g b
forall (c :: (* -> *) -> Constraint) (f :: * -> *) (g :: * -> *) a.
c f =>
(f :~> g) -> f a -> HCofree c g a
HCofree f :~> g
k (f b -> HCofree c g b) -> m (f b) -> m (HCofree c g b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> m b) -> f a -> m (f b)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> m b
f f a
a
  sequence :: HCofree c g (m a) -> m (HCofree c g a)
sequence (HCofree f :~> g
k f (m a)
a) = (f :~> g) -> f a -> HCofree c g a
forall (c :: (* -> *) -> Constraint) (f :: * -> *) (g :: * -> *) a.
c f =>
(f :~> g) -> f a -> HCofree c g a
HCofree f :~> g
k (f a -> HCofree c g a) -> m (f a) -> m (HCofree c g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (m a) -> m (f a)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence f (m a)
a

-- | The cofree comonad of a functor.
instance (forall x. c x => Comonad x) => Comonad (HCofree c g) where
  extract :: HCofree c g a -> a
extract (HCofree f :~> g
_ f a
a) = f a -> a
forall (w :: * -> *) a. Comonad w => w a -> a
extract f a
a
  extend :: (HCofree c g a -> b) -> HCofree c g a -> HCofree c g b
extend HCofree c g a -> b
f (HCofree f :~> g
k f a
a) = (f :~> g) -> f b -> HCofree c g b
forall (c :: (* -> *) -> Constraint) (f :: * -> *) (g :: * -> *) a.
c f =>
(f :~> g) -> f a -> HCofree c g a
HCofree f :~> g
k (f b -> HCofree c g b) -> f b -> HCofree c g b
forall a b. (a -> b) -> a -> b
$ (f a -> b) -> f a -> f b
forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend (HCofree c g a -> b
f (HCofree c g a -> b) -> (f a -> HCofree c g a) -> f a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f :~> g) -> f a -> HCofree c g a
forall (c :: (* -> *) -> Constraint) (f :: * -> *) (g :: * -> *) a.
c f =>
(f :~> g) -> f a -> HCofree c g a
HCofree f :~> g
k) f a
a
  duplicate :: HCofree c g a -> HCofree c g (HCofree c g a)
duplicate (HCofree f :~> g
k f a
a) = (f :~> g) -> f (HCofree c g a) -> HCofree c g (HCofree c g a)
forall (c :: (* -> *) -> Constraint) (f :: * -> *) (g :: * -> *) a.
c f =>
(f :~> g) -> f a -> HCofree c g a
HCofree f :~> g
k (f (HCofree c g a) -> HCofree c g (HCofree c g a))
-> f (HCofree c g a) -> HCofree c g (HCofree c g a)
forall a b. (a -> b) -> a -> b
$ (f a -> HCofree c g a) -> f a -> f (HCofree c g a)
forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend ((f :~> g) -> f a -> HCofree c g a
forall (c :: (* -> *) -> Constraint) (f :: * -> *) (g :: * -> *) a.
c f =>
(f :~> g) -> f a -> HCofree c g a
HCofree f :~> g
k) f a
a