{-# OPTIONS_GHC -fno-warn-unused-matches #-}
{-# LANGUAGE
    RankNTypes
  , TypeOperators
  , ConstraintKinds
  , TemplateHaskell
  , UndecidableInstances
  , QuantifiedConstraints
  #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Functor.HHFree
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-- A free functor is left adjoint to a forgetful functor.
-- In this package the forgetful functor forgets class constraints.
--
-- Compared to @Data.Functor.HFree@ we have 2 two parameters.
-----------------------------------------------------------------------------
module Data.Functor.HHFree where

import Prelude hiding ((.), id)

import Control.Arrow
import Control.Category
import Data.Bifunctor (Bifunctor)
import Data.Bifunctor.Functor
import Data.Biapplicative (Biapplicative)
import Data.Profunctor
import Data.Profunctor.Monad

import Language.Haskell.TH.Syntax (Q, Name, Dec)
import Data.Functor.Free.Internal


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

-- | The higher order free functor over two type parameters for constraint @c@.
newtype HHFree c f a b = HHFree { HHFree c f a b
-> forall (g :: * -> * -> *). c g => (f :~~> g) -> g a b
runHHFree :: forall g. c g => (f :~~> g) -> g a b }


-- | Derive the instance of @`HHFree` c f a b@ for the class @c@,.
--
-- For example:
--
-- @deriveHHFreeInstance ''Category@
deriveHHFreeInstance :: Name -> Q [Dec]
deriveHHFreeInstance :: Name -> Q [Dec]
deriveHHFreeInstance = Name -> Name -> Name -> Name -> Q [Dec]
deriveFreeInstance' ''HHFree 'HHFree 'runHHFree


unit :: f :~~> HHFree c f
unit :: f a b -> HHFree c f a b
unit f a b
fa = (forall (g :: * -> * -> *). c g => (f :~~> g) -> g a b)
-> HHFree c f a b
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *) a b.
(forall (g :: * -> * -> *). c g => (f :~~> g) -> g a b)
-> HHFree c f a b
HHFree ((forall (g :: * -> * -> *). c g => (f :~~> g) -> g a b)
 -> HHFree c f a b)
-> (forall (g :: * -> * -> *). c g => (f :~~> g) -> g a b)
-> HHFree c f a b
forall a b. (a -> b) -> a -> b
$ \f :~~> g
k -> f a b -> g a b
f :~~> g
k f a b
fa

rightAdjunct :: c g => (f :~~> g) -> HHFree c f :~~> g
rightAdjunct :: (f :~~> g) -> HHFree c f :~~> g
rightAdjunct f :~~> g
f HHFree c f a b
h = HHFree c f a b -> (f :~~> g) -> g a b
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *) a b.
HHFree c f a b
-> forall (g :: * -> * -> *). c g => (f :~~> g) -> g a b
runHHFree HHFree c f a b
h f :~~> g
f

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

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

transform :: (forall r. c r => (g :~~> r) -> f :~~> r) -> HHFree c f :~~> HHFree c g
transform :: (forall (r :: * -> * -> *). c r => (g :~~> r) -> f :~~> r)
-> HHFree c f :~~> HHFree c g
transform forall (r :: * -> * -> *). c r => (g :~~> r) -> f :~~> r
t HHFree c f a b
h = (forall (g :: * -> * -> *). c g => (g :~~> g) -> g a b)
-> HHFree c g a b
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *) a b.
(forall (g :: * -> * -> *). c g => (f :~~> g) -> g a b)
-> HHFree c f a b
HHFree ((forall (g :: * -> * -> *). c g => (g :~~> g) -> g a b)
 -> HHFree c g a b)
-> (forall (g :: * -> * -> *). c g => (g :~~> g) -> g a b)
-> HHFree c g a b
forall a b. (a -> b) -> a -> b
$ \g :~~> g
k -> (f :~~> g) -> HHFree c f a b -> g a b
forall (c :: (* -> * -> *) -> Constraint) (g :: * -> * -> *)
       (f :: * -> * -> *).
c g =>
(f :~~> g) -> HHFree c f :~~> g
rightAdjunct ((g :~~> g) -> f :~~> g
forall (r :: * -> * -> *). c r => (g :~~> r) -> f :~~> r
t g :~~> g
k) HHFree c f a b
h
-- transform t = HHFree . (. t) . runHHFree

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

bind :: (f :~~> HHFree c g) -> HHFree c f :~~> HHFree c g
bind :: (f :~~> HHFree c g) -> HHFree c f :~~> HHFree c g
bind f :~~> HHFree c g
f = (forall (r :: * -> * -> *). c r => (g :~~> r) -> f :~~> r)
-> HHFree c f :~~> HHFree c g
forall (c :: (* -> * -> *) -> Constraint) (g :: * -> * -> *)
       (f :: * -> * -> *).
(forall (r :: * -> * -> *). c r => (g :~~> r) -> f :~~> r)
-> HHFree c f :~~> HHFree c g
transform (\g :~~> r
k -> (g :~~> r) -> HHFree c g :~~> r
forall (c :: (* -> * -> *) -> Constraint) (g :: * -> * -> *)
       (f :: * -> * -> *).
c g =>
(f :~~> g) -> HHFree c f :~~> g
rightAdjunct g :~~> r
k (HHFree c g a b -> r a b)
-> (f a b -> HHFree c g a b) -> f a b -> r a b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f a b -> HHFree c g a b
f :~~> HHFree c g
f)

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

instance BifunctorMonad (HHFree c) where
  bireturn :: p a b -> HHFree c p a b
bireturn = p a b -> HHFree c p a b
forall (f :: * -> * -> *) (c :: (* -> * -> *) -> Constraint).
f :~~> HHFree c f
unit
  bibind :: (p :-> HHFree c q) -> HHFree c p :-> HHFree c q
bibind = (p :-> HHFree c q) -> HHFree c p a b -> HHFree c q a b
forall (f :: * -> * -> *) (c :: (* -> * -> *) -> Constraint)
       (g :: * -> * -> *).
(f :~~> HHFree c g) -> HHFree c f :~~> HHFree c g
bind

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

instance ProfunctorMonad (HHFree c) where
  proreturn :: p :-> HHFree c p
proreturn = p a b -> HHFree c p a b
forall (f :: * -> * -> *) (c :: (* -> * -> *) -> Constraint).
f :~~> HHFree c f
unit
  projoin :: HHFree c (HHFree c p) :-> HHFree c p
projoin = (HHFree c p :~~> HHFree c p)
-> HHFree c (HHFree c p) :-> HHFree c p
forall (f :: * -> * -> *) (c :: (* -> * -> *) -> Constraint)
       (g :: * -> * -> *).
(f :~~> HHFree c g) -> HHFree c f :~~> HHFree c g
bind HHFree c p :~~> HHFree c p
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id


deriveFreeInstance' ''HHFree 'HHFree 'runHHFree ''Category
deriveFreeInstance' ''HHFree 'HHFree 'runHHFree ''Arrow
deriveFreeInstance' ''HHFree 'HHFree 'runHHFree ''ArrowZero
deriveFreeInstance' ''HHFree 'HHFree 'runHHFree ''ArrowPlus
deriveFreeInstance' ''HHFree 'HHFree 'runHHFree ''ArrowChoice
deriveFreeInstance' ''HHFree 'HHFree 'runHHFree ''ArrowLoop

instance (forall x. c x => ArrowApply x) => ArrowApply (HHFree c f) where
  app :: HHFree c f (HHFree c f b c, b) c
app = (forall (g :: * -> * -> *).
 c g =>
 (f :~~> g) -> g (HHFree c f b c, b) c)
-> HHFree c f (HHFree c f b c, b) c
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *) a b.
(forall (g :: * -> * -> *). c g => (f :~~> g) -> g a b)
-> HHFree c f a b
HHFree ((forall (g :: * -> * -> *).
  c g =>
  (f :~~> g) -> g (HHFree c f b c, b) c)
 -> HHFree c f (HHFree c f b c, b) c)
-> (forall (g :: * -> * -> *).
    c g =>
    (f :~~> g) -> g (HHFree c f b c, b) c)
-> HHFree c f (HHFree c f b c, b) c
forall a b. (a -> b) -> a -> b
$ \f :~~> g
k -> g (g b c, b) c
forall (a :: * -> * -> *) b c. ArrowApply a => a (a b c, b) c
app g (g b c, b) c
-> g (HHFree c f b c, b) (g b c, b) -> g (HHFree c f b c, b) c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((HHFree c f b c, b) -> (g b c, b))
-> g (HHFree c f b c, b) (g b c, b)
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr ((HHFree c f b c -> g b c) -> (HHFree c f b c, b) -> (g b c, b)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((f :~~> g) -> HHFree c f :~~> g
forall (c :: (* -> * -> *) -> Constraint) (g :: * -> * -> *)
       (f :: * -> * -> *).
c g =>
(f :~~> g) -> HHFree c f :~~> g
rightAdjunct f :~~> g
k))

deriveFreeInstance' ''HHFree 'HHFree 'runHHFree ''Bifunctor
deriveFreeInstance' ''HHFree 'HHFree 'runHHFree ''Biapplicative
deriveFreeInstance' ''HHFree 'HHFree 'runHHFree ''Profunctor
deriveFreeInstance' ''HHFree 'HHFree 'runHHFree ''Strong
deriveFreeInstance' ''HHFree 'HHFree 'runHHFree ''Choice
deriveFreeInstance' ''HHFree 'HHFree 'runHHFree ''Closed