{-# LANGUAGE
    GADTs
  , RankNTypes
  , TypeOperators
  , ConstraintKinds
  , TemplateHaskell
  , 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.Functor.Identity

import Language.Haskell.TH.Syntax
import Data.Functor.Cofree.Internal


-- | 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


-- | Derive the instance of @`HCofree` c a@ for the class @c@.
--
-- For example:
--
-- @deriveHCofreeInstance ''Traversable@
deriveHCofreeInstance :: Name -> Q [Dec]
deriveHCofreeInstance :: Name -> Q [Dec]
deriveHCofreeInstance = Name -> Name -> Name -> Q [Dec]
deriveCofreeInstance' ''HCofree 'HCofree


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

deriveCofreeInstance' ''HCofree 'HCofree ''Functor
deriveCofreeInstance' ''HCofree 'HCofree ''Foldable
deriveCofreeInstance' ''HCofree 'HCofree ''Traversable

-- | The cofree comonad of a functor.
instance (c ~=> Comonad) => 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