{-# LANGUAGE TypeOperators #-}

module ZkFold.Base.Control.HApplicative where

import           Data.Function             (const, ($), (.))
import           GHC.Generics              (U1 (..), (:*:) (..))

import           ZkFold.Base.Data.HFunctor

-- | A higher-order functor with application, providing operations to apply a
-- function of type @(forall a. f a -> g a -> ...)@ of arbitrary arity to
-- arguments of corresponding types @f a@, @g a@, ...
class HFunctor c => HApplicative c where
  {-# MINIMAL (hpure | hunit), (hap | hliftA2 | hpair) #-}

  -- | Lift a proxy functor into the structure. If 'hunit' is specified instead,
  -- a default definition is available. The following is expected to hold:
  --
  -- [Definition] @'hpure' x == 'hmap' ('const' x) 'hunit'@
  hpure :: (forall a. f a) -> c f
  hpure forall (a :: k). f a
f = (forall (a :: k). U1 a -> f a) -> c U1 -> c f
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HFunctor c =>
(forall (a :: k). f a -> g a) -> c f -> c g
forall (f :: k -> Type) (g :: k -> Type).
(forall (a :: k). f a -> g a) -> c f -> c g
hmap (f a -> U1 a -> f a
forall a b. a -> b -> a
const f a
forall (a :: k). f a
f) c U1
forall {k} (c :: (k -> Type) -> Type). HApplicative c => c U1
hunit

  -- | Lift a concrete proxy functor @'U1'@ into the structure.
  -- Note that it is almost always better to define @'hpure'@ instead and rely
  -- on the default implementation of @'hunit'@.
  -- The following is expected to hold:
  --
  -- [Definition] @'hunit' == 'hpure' 'U1'@
  hunit :: c U1
  hunit = (forall (a :: k). U1 a) -> c U1
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type).
HApplicative c =>
(forall (a :: k). f a) -> c f
forall (f :: k -> Type). (forall (a :: k). f a) -> c f
hpure U1 a
forall (a :: k). U1 a
forall k (p :: k). U1 p
U1

  -- | Sequential application. It is hard to find the legitimate usecase for
  -- this function; this is only provided for comparison with classic
  -- @'Applicative'@ class.
  --
  -- The default definition is via @'hpair'@. The following is expected to hold:
  --
  -- [Definition] @'hap' t f == 'hmap' (\\('Transform' g ':*:' x) -> g x) ('hpair' t x)@
  hap :: c (Transform f g) -> c f -> c g
  hap c (Transform f g)
t = (forall (a :: k). (:*:) (Transform f g) f a -> g a)
-> c (Transform f g :*: f) -> c g
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HFunctor c =>
(forall (a :: k). f a -> g a) -> c f -> c g
forall (f :: k -> Type) (g :: k -> Type).
(forall (a :: k). f a -> g a) -> c f -> c g
hmap (\(Transform f a -> g a
g :*: f a
x) -> f a -> g a
g f a
x) (c (Transform f g :*: f) -> c g)
-> (c f -> c (Transform f g :*: f)) -> c f -> c g
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c (Transform f g) -> c f -> c (Transform f g :*: f)
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HApplicative c =>
c f -> c g -> c (f :*: g)
forall (f :: k -> Type) (g :: k -> Type). c f -> c g -> c (f :*: g)
hpair c (Transform f g)
t

  -- | Applies a binary function of type @(forall a. f a -> g a -> h a)@ to a
  -- pair of arguments of types @c f@ and @c g@,
  -- yielding the result of type @c h@.
  --
  -- If @'hap'@ is specified instead, a default definition is available.
  -- The following is expected to hold:
  --
  -- [Definition] @'hliftA2' f x y == 'hap' ('hmap' ('Transform' '.' f) x) y@
  -- [Compatibility] @'hmap' f x == 'hliftA2' ('const' f) 'hunit' x@
  hliftA2 :: (forall a. f a -> g a -> h a) -> c f -> c g -> c h
  hliftA2 forall (a :: k). f a -> g a -> h a
f = c (Transform g h) -> c g -> c h
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HApplicative c =>
c (Transform f g) -> c f -> c g
forall (f :: k -> Type) (g :: k -> Type).
c (Transform f g) -> c f -> c g
hap (c (Transform g h) -> c g -> c h)
-> (c f -> c (Transform g h)) -> c f -> c g -> c h
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). f a -> Transform g h a)
-> c f -> c (Transform g h)
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HFunctor c =>
(forall (a :: k). f a -> g a) -> c f -> c g
forall (f :: k -> Type) (g :: k -> Type).
(forall (a :: k). f a -> g a) -> c f -> c g
hmap ((g a -> h a) -> Transform g h a
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
(f a -> g a) -> Transform f g a
Transform ((g a -> h a) -> Transform g h a)
-> (f a -> g a -> h a) -> f a -> Transform g h a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> g a -> h a
forall (a :: k). f a -> g a -> h a
f)

  -- | Joins two structures, preserving the outputs. Note that it is almost
  -- always better to define @'hliftA2'@ instead and rely on the default
  -- implementation of @'hpair'@. The following is expected to hold:
  --
  -- [Definition] @'hpair' x y == 'hliftA2' (':*:') x y@
  -- [Associativity] @'hliftA2' (\\(a ':*:' b) c -> a ':*:' (b ':*:' c)) ('hpair' x y) z == 'hpair' x ('hpair' y z)@
  -- [Left identity] @'hliftA2' 'const' x 'hunit' == x@
  -- [Right identity] @'hliftA2' ('const' 'id') 'hunit' y == y@
  hpair :: c f -> c g -> c (f :*: g)
  hpair = (forall (a :: k). f a -> g a -> (:*:) f g a)
-> c f -> c g -> c (f :*: g)
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type) (h :: k -> Type).
HApplicative c =>
(forall (a :: k). f a -> g a -> h a) -> c f -> c g -> c h
forall (f :: k -> Type) (g :: k -> Type) (h :: k -> Type).
(forall (a :: k). f a -> g a -> h a) -> c f -> c g -> c h
hliftA2 f a -> g a -> (:*:) f g a
forall (a :: k). f a -> g a -> (:*:) f g a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
(:*:)

-- | A newtype wrapper for natural transformations used in @'hap'@ definition.
newtype Transform f g a = Transform { forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
Transform f g a -> f a -> g a
runTransform :: f a -> g a }

-- | If @'hap'@ and @'hpure'@ do not rely on @'hmap'@ (i.e. at least are not
-- implemented by default), this function can be used to implement @'hmap'@.
hmapA :: HApplicative c => (forall a. f a -> g a) -> c f -> c g
hmapA :: forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HApplicative c =>
(forall (a :: k). f a -> g a) -> c f -> c g
hmapA forall (a :: k). f a -> g a
g = c (Transform f g) -> c f -> c g
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HApplicative c =>
c (Transform f g) -> c f -> c g
forall (f :: k -> Type) (g :: k -> Type).
c (Transform f g) -> c f -> c g
hap (c (Transform f g) -> c f -> c g)
-> c (Transform f g) -> c f -> c g
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Transform f g a) -> c (Transform f g)
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type).
HApplicative c =>
(forall (a :: k). f a) -> c f
forall (f :: k -> Type). (forall (a :: k). f a) -> c f
hpure ((f a -> g a) -> Transform f g a
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
(f a -> g a) -> Transform f g a
Transform f a -> g a
forall (a :: k). f a -> g a
g)

-- | If @'hliftA2'@ and @'hunit'@ do not rely on @'hmap'@ (at least, @'hliftA2'@
-- is not implemented by default), this function can be used to implement @'hmap'@.
hliftA1 :: HApplicative c => (forall a. f a -> g a) -> c f -> c g
hliftA1 :: forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HApplicative c =>
(forall (a :: k). f a -> g a) -> c f -> c g
hliftA1 forall (a :: k). f a -> g a
g = (forall (a :: k). U1 a -> f a -> g a) -> c U1 -> c f -> c g
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type) (h :: k -> Type).
HApplicative c =>
(forall (a :: k). f a -> g a -> h a) -> c f -> c g -> c h
forall (f :: k -> Type) (g :: k -> Type) (h :: k -> Type).
(forall (a :: k). f a -> g a -> h a) -> c f -> c g -> c h
hliftA2 ((f a -> g a) -> U1 a -> f a -> g a
forall a b. a -> b -> a
const f a -> g a
forall (a :: k). f a -> g a
g) c U1
forall {k} (c :: (k -> Type) -> Type). HApplicative c => c U1
hunit

-- | Applies a ternary natural transformation
-- to a triple of arguments behind an @'HApplicative'@.
hliftA3 :: HApplicative c => (forall a. f a -> g a -> h a -> i a) -> c f -> c g -> c h -> c i
hliftA3 :: forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type) (h :: k -> Type) (i :: k -> Type).
HApplicative c =>
(forall (a :: k). f a -> g a -> h a -> i a)
-> c f -> c g -> c h -> c i
hliftA3 forall (a :: k). f a -> g a -> h a -> i a
i c f
f c g
g = (forall (a :: k). (:*:) f g a -> h a -> i a)
-> c (f :*: g) -> c h -> c i
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type) (h :: k -> Type).
HApplicative c =>
(forall (a :: k). f a -> g a -> h a) -> c f -> c g -> c h
forall (f :: k -> Type) (g :: k -> Type) (h :: k -> Type).
(forall (a :: k). f a -> g a -> h a) -> c f -> c g -> c h
hliftA2 (\(f a
x :*: g a
y) -> f a -> g a -> h a -> i a
forall (a :: k). f a -> g a -> h a -> i a
i f a
x g a
y) (c f -> c g -> c (f :*: g)
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HApplicative c =>
c f -> c g -> c (f :*: g)
forall (f :: k -> Type) (g :: k -> Type). c f -> c g -> c (f :*: g)
hpair c f
f c g
g)