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

import Control.Applicative
import Control.Monad (join)
import Control.Monad.Trans.Class
import Data.Functor.Identity
import Data.Functor.Contravariant
import Data.Functor.Contravariant.Divisible

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

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

-- | The higher order free functor for constraint @c@.
newtype HFree c f a = HFree { forall (c :: (* -> *) -> Constraint) (f :: * -> *) a.
HFree c f a -> forall (g :: * -> *). c g => (f :~> g) -> g a
runHFree :: forall g. c g => (f :~> g) -> g a }

-- | The free monad of a functor.
instance (c ~=> Monad, c (HFree c f)) => Monad (HFree c f) where
  return :: forall a. a -> HFree c f a
return = a -> HFree c f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  HFree forall (g :: * -> *). c g => (f :~> g) -> g a
f >>= :: forall a b. HFree c f a -> (a -> HFree c f b) -> HFree c f b
>>= a -> HFree c f b
g = (forall (g :: * -> *). c g => (f :~> g) -> g b) -> HFree c f b
forall (c :: (* -> *) -> Constraint) (f :: * -> *) a.
(forall (g :: * -> *). c g => (f :~> g) -> g a) -> HFree c f a
HFree ((forall (g :: * -> *). c g => (f :~> g) -> g b) -> HFree c f b)
-> (forall (g :: * -> *). c g => (f :~> g) -> g b) -> HFree c f b
forall a b. (a -> b) -> a -> b
$ \f :~> g
k -> (f :~> g) -> g a
forall (g :: * -> *). c g => (f :~> g) -> g a
f f :~> g
k g a -> (a -> g b) -> g b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (f :~> g) -> HFree c f :~> g
forall (c :: (* -> *) -> Constraint) (g :: * -> *) (f :: * -> *).
c g =>
(f :~> g) -> HFree c f :~> g
rightAdjunct f :~> g
k (HFree c f b -> g b) -> (a -> HFree c f b) -> a -> g b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> HFree c f b
g
  HFree forall (g :: * -> *). c g => (f :~> g) -> g a
f >> :: forall a b. HFree c f a -> HFree c f b -> HFree c f b
>> HFree forall (g :: * -> *). c g => (f :~> g) -> g b
g = (forall (g :: * -> *). c g => (f :~> g) -> g b) -> HFree c f b
forall (c :: (* -> *) -> Constraint) (f :: * -> *) a.
(forall (g :: * -> *). c g => (f :~> g) -> g a) -> HFree c f a
HFree ((forall (g :: * -> *). c g => (f :~> g) -> g b) -> HFree c f b)
-> (forall (g :: * -> *). c g => (f :~> g) -> g b) -> HFree c f b
forall a b. (a -> b) -> a -> b
$ \f :~> g
k -> (f :~> g) -> g a
forall (g :: * -> *). c g => (f :~> g) -> g a
f f :~> g
k g a -> g b -> g b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (f :~> g) -> g b
forall (g :: * -> *). c g => (f :~> g) -> g b
g f :~> g
k


-- | Derive the instance of @`HFree` c f a@ for the class @c@,.
--
-- For example:
--
-- @deriveHFreeInstance ''Functor@
deriveHFreeInstance :: Name -> Q [Dec]
deriveHFreeInstance :: Name -> Q [Dec]
deriveHFreeInstance = Name -> Name -> Name -> Name -> Q [Dec]
deriveFreeInstance' ''HFree 'HFree 'runHFree

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

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

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

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

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

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

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

liftFree :: f a -> HFree c f a
liftFree :: forall (f :: * -> *) a (c :: (* -> *) -> Constraint).
f a -> HFree c f a
liftFree = f a -> HFree c f a
forall (f :: * -> *) (c :: (* -> *) -> Constraint). f :~> HFree c f
unit

lowerFree :: c f => HFree c f a -> f a
lowerFree :: forall (c :: (* -> *) -> Constraint) (f :: * -> *) a.
c f =>
HFree c f a -> f a
lowerFree = HFree c f a -> f a
forall (c :: (* -> *) -> Constraint) (f :: * -> *).
c f =>
HFree c f :~> f
counit

convert :: (c (t f), Monad f, MonadTrans t) => HFree c f a -> t f a
convert :: forall (c :: (* -> *) -> Constraint) (t :: (* -> *) -> * -> *)
       (f :: * -> *) a.
(c (t f), Monad f, MonadTrans t) =>
HFree c f a -> t f a
convert = (f :~> t f) -> HFree c f :~> t f
forall (c :: (* -> *) -> Constraint) (g :: * -> *) (f :: * -> *).
c g =>
(f :~> g) -> HFree c f :~> g
rightAdjunct f :~> t f
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

iter :: c Identity => (forall b. f b -> b) -> HFree c f a -> a
iter :: forall (c :: (* -> *) -> Constraint) (f :: * -> *) a.
c Identity =>
(forall b. f b -> b) -> HFree c f a -> a
iter forall b. f b -> b
f = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a)
-> (HFree c f a -> Identity a) -> HFree c f a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f :~> Identity) -> HFree c f :~> Identity
forall (c :: (* -> *) -> Constraint) (g :: * -> *) (f :: * -> *).
c g =>
(f :~> g) -> HFree c f :~> g
rightAdjunct (b -> Identity b
forall a. a -> Identity a
Identity (b -> Identity b) -> (f b -> b) -> f b -> Identity b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f b -> b
forall b. f b -> b
f)

wrap :: f (HFree Monad f a) -> HFree Monad f a
wrap :: forall (f :: * -> *) a. f (HFree Monad f a) -> HFree Monad f a
wrap f (HFree Monad f a)
as = HFree Monad f (HFree Monad f a) -> HFree Monad f a
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (f (HFree Monad f a) -> HFree Monad f (HFree Monad f a)
forall (f :: * -> *) (c :: (* -> *) -> Constraint). f :~> HFree c f
unit f (HFree Monad f a)
as)


deriveFreeInstance' ''HFree 'HFree 'runHFree ''Functor
deriveFreeInstance' ''HFree 'HFree 'runHFree ''Applicative
deriveFreeInstance' ''HFree 'HFree 'runHFree ''Alternative

-- HFree Monad is only a monad transformer if rightAdjunct is called with monad morphisms.
-- F.e. lift . return == return fails if the results are inspected with rightAdjunct (const Nothing).

deriveFreeInstance' ''HFree 'HFree 'runHFree ''Contravariant
deriveFreeInstance' ''HFree 'HFree 'runHFree ''Divisible
deriveFreeInstance' ''HFree 'HFree 'runHFree ''Decidable