{-# LANGUAGE CPP #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

#if __GLASGOW_HASKELL__ >= 806

{-# LANGUAGE QuantifiedConstraints #-}

#endif

{-# OPTIONS_GHC -Wno-orphans #-}
module Barbies.Internal.ApplicativeT
  ( ApplicativeT(tpure, tprod)
  , tzip, tunzip, tzipWith, tzipWith3, tzipWith4

  , CanDeriveApplicativeT
  , gtprodDefault, gtpureDefault
  )

where

import Barbies.Generics.Applicative(GApplicative(..))
import Barbies.Internal.FunctorT (FunctorT (..))

import Control.Applicative (Alternative(..))
import Data.Functor.Compose (Compose (..))
import Data.Functor.Product (Product (..))
import Data.Functor.Reverse (Reverse (..))
import Data.Functor.Sum (Sum (..))
import Data.Kind (Type)
import Data.Proxy (Proxy (..))

import Data.Generics.GenericN

-- | A 'FunctorT' with application, providing operations to:
--
--     * embed an "empty" value ('tpure')
--
--     * align and combine values ('tprod')
--
--  It should satisfy the following laws:
--
--  [Naturality of 'tprod']
--
-- @
-- 'tmap' (\('Pair' a b) -> 'Pair' (f a) (g b)) (u `'tprod'` v) = 'tmap' f u `'tprod'` 'tmap' g v
-- @
--
--  [Left and right identity]
--
-- @
-- 'tmap' (\('Pair' _ b) -> b) ('tpure' e `'tprod'` v) = v
-- 'tmap' (\('Pair' a _) -> a) (u `'tprod'` 'tpure' e) = u
-- @
--
-- [Associativity]
--
-- @
-- 'tmap' (\('Pair' a ('Pair' b c)) -> 'Pair' ('Pair' a b) c) (u `'tprod'` (v `'tprod'` w)) = (u `'tprod'` v) `'tprod'` w
-- @
--
--  It is to 'FunctorT' in the same way is 'Applicative'
--  relates to 'Functor'. For a presentation of 'Applicative' as
--  a monoidal functor, see Section 7 of
--  <http://www.soi.city.ac.uk/~ross/papers/Applicative.html Applicative Programming with Effects>.
--
-- There is a default implementation of 'tprod' and 'tpure' based on 'Generic'.
-- Intuitively, it works on types where the value of `tpure` is uniquely defined.
-- This corresponds rougly to record types (in the presence of sums, there would
-- be several candidates for `tpure`), where every field is either a 'Monoid' or
-- covered by the argument @f@.
class FunctorT t => ApplicativeT (t :: (k -> Type) -> (k' -> Type)) where
  tpure
    :: (forall a . f a)
    -> t f x

  tprod
    :: t f x
    -> t g x
    -> t (f `Product` g) x

  default tpure
    :: CanDeriveApplicativeT t f f x
    => (forall a . f a)
    -> t f x
  tpure = forall {k} {k} (t :: (k -> *) -> k -> *) (f :: k -> *) (x :: k).
CanDeriveApplicativeT t f f x =>
(forall (a :: k). f a) -> t f x
gtpureDefault

  default tprod
    :: CanDeriveApplicativeT t f g x
    => t f x
    -> t g x
    -> t (f `Product` g) x
  tprod = forall {k} {k} (t :: (k -> *) -> k -> *) (f :: k -> *)
       (g :: k -> *) (x :: k).
CanDeriveApplicativeT t f g x =>
t f x -> t g x -> t (Product f g) x
gtprodDefault


-- | An alias of 'tprod'.
tzip
  :: ApplicativeT t
  => t f x
  -> t g x
  -> t (f `Product` g) x
tzip :: forall {k} {k'} (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
       (g :: k -> *).
ApplicativeT t =>
t f x -> t g x -> t (Product f g) x
tzip = forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
       (g :: k -> *).
ApplicativeT t =>
t f x -> t g x -> t (Product f g) x
tprod

-- | An equivalent of 'unzip'.
tunzip
  :: ApplicativeT t
  => t (f `Product` g) x
  -> (t f x, t g x)
tunzip :: forall {k} {k'} (t :: (k -> *) -> k' -> *) (f :: k -> *)
       (g :: k -> *) (x :: k').
ApplicativeT t =>
t (Product f g) x -> (t f x, t g x)
tunzip t (Product f g) x
tfg
  = (forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (g :: k -> *)
       (x :: k').
FunctorT t =>
(forall (a :: k). f a -> g a) -> t f x -> t g x
tmap (\(Pair f a
a g a
_) -> f a
a) t (Product f g) x
tfg, forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (g :: k -> *)
       (x :: k').
FunctorT t =>
(forall (a :: k). f a -> g a) -> t f x -> t g x
tmap (\(Pair f a
_ g a
b) -> g a
b) t (Product f g) x
tfg)

-- | An equivalent of 'Data.List.zipWith'.
tzipWith
  :: ApplicativeT t
  => (forall a. f a -> g a -> h a)
  -> t f x
  -> t g x
  -> t h x
tzipWith :: forall {k} {k'} (t :: (k -> *) -> k' -> *) (f :: k -> *)
       (g :: k -> *) (h :: k -> *) (x :: k').
ApplicativeT t =>
(forall (a :: k). f a -> g a -> h a) -> t f x -> t g x -> t h x
tzipWith forall (a :: k). f a -> g a -> h a
f t f x
tf t g x
tg
  = forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (g :: k -> *)
       (x :: k').
FunctorT t =>
(forall (a :: k). f a -> g a) -> t f x -> t g x
tmap (\(Pair f a
fa g a
ga) -> forall (a :: k). f a -> g a -> h a
f f a
fa g a
ga) (t f x
tf forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
       (g :: k -> *).
ApplicativeT t =>
t f x -> t g x -> t (Product f g) x
`tprod` t g x
tg)

-- | An equivalent of 'Data.List.zipWith3'.
tzipWith3
  :: ApplicativeT t
  => (forall a. f a -> g a -> h a -> i a)
  -> t f x
  -> t g x
  -> t h x
  -> t i x
tzipWith3 :: forall {k} {k'} (t :: (k -> *) -> k' -> *) (f :: k -> *)
       (g :: k -> *) (h :: k -> *) (i :: k -> *) (x :: k').
ApplicativeT t =>
(forall (a :: k). f a -> g a -> h a -> i a)
-> t f x -> t g x -> t h x -> t i x
tzipWith3 forall (a :: k). f a -> g a -> h a -> i a
f t f x
tf t g x
tg t h x
th
  = forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (g :: k -> *)
       (x :: k').
FunctorT t =>
(forall (a :: k). f a -> g a) -> t f x -> t g x
tmap (\(Pair (Pair f a
fa g a
ga) h a
ha) -> forall (a :: k). f a -> g a -> h a -> i a
f f a
fa g a
ga h a
ha)
         (t f x
tf forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
       (g :: k -> *).
ApplicativeT t =>
t f x -> t g x -> t (Product f g) x
`tprod` t g x
tg forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
       (g :: k -> *).
ApplicativeT t =>
t f x -> t g x -> t (Product f g) x
`tprod` t h x
th)


-- | An equivalent of 'Data.List.zipWith4'.
tzipWith4
  :: ApplicativeT t
  => (forall a. f a -> g a -> h a -> i a -> j a)
  -> t f x
  -> t g x
  -> t h x
  -> t i x
  -> t j x
tzipWith4 :: forall {k} {k'} (t :: (k -> *) -> k' -> *) (f :: k -> *)
       (g :: k -> *) (h :: k -> *) (i :: k -> *) (j :: k -> *) (x :: k').
ApplicativeT t =>
(forall (a :: k). f a -> g a -> h a -> i a -> j a)
-> t f x -> t g x -> t h x -> t i x -> t j x
tzipWith4 forall (a :: k). f a -> g a -> h a -> i a -> j a
f t f x
tf t g x
tg t h x
th t i x
ti
  = forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (g :: k -> *)
       (x :: k').
FunctorT t =>
(forall (a :: k). f a -> g a) -> t f x -> t g x
tmap (\(Pair (Pair (Pair f a
fa g a
ga) h a
ha) i a
ia) -> forall (a :: k). f a -> g a -> h a -> i a -> j a
f f a
fa g a
ga h a
ha i a
ia)
         (t f x
tf forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
       (g :: k -> *).
ApplicativeT t =>
t f x -> t g x -> t (Product f g) x
`tprod` t g x
tg forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
       (g :: k -> *).
ApplicativeT t =>
t f x -> t g x -> t (Product f g) x
`tprod` t h x
th forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
       (g :: k -> *).
ApplicativeT t =>
t f x -> t g x -> t (Product f g) x
`tprod` t i x
ti)


-- | @'CanDeriveApplicativeT' T f g x@ is in practice a predicate about @T@ only.
--   Intuitively, it says that the following holds, for any arbitrary @f@:
--
--     * There is an instance of @'Generic' (T f)@.
--
--     * @T@ has only one constructor (that is, it is not a sum-type).
--
--     * Every field of @T f x@ is either a monoid, or of the form @f a@, for
--       some type @a@.
type CanDeriveApplicativeT t f g x
  = ( GenericP 1 (t f x)
    , GenericP 1 (t g x)
    , GenericP 1 (t (f `Product` g) x)
    , GApplicative 1 f g (RepP 1 (t f x)) (RepP 1 (t g x)) (RepP 1 (t (f `Product` g) x))
    )


-- ======================================
-- Generic derivation of instances
-- ======================================

-- | Default implementation of 'tprod' based on 'Generic'.
gtprodDefault
  :: forall t f g x
  .  CanDeriveApplicativeT t f g x
  => t f x
  -> t g x
  -> t (f `Product` g) x
gtprodDefault :: forall {k} {k} (t :: (k -> *) -> k -> *) (f :: k -> *)
       (g :: k -> *) (x :: k).
CanDeriveApplicativeT t f g x =>
t f x -> t g x -> t (Product f g) x
gtprodDefault t f x
l t g x
r
  = forall (n :: Natural) a x.
GenericP n a =>
Proxy n -> RepP n a x -> a
toP Proxy 1
p1 forall a b. (a -> b) -> a -> b
$ forall {k} {k} k (n :: k) (f :: k -> *) (g :: k -> *)
       (repbf :: k -> *) (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
GApplicative n f g repbf repbg repbfg =>
Proxy n -> Proxy f -> Proxy g -> repbf x -> repbg x -> repbfg x
gprod Proxy 1
p1 (forall {k} (t :: k). Proxy t
Proxy @f) (forall {k} (t :: k). Proxy t
Proxy @g) (forall (n :: Natural) a x.
GenericP n a =>
Proxy n -> a -> RepP n a x
fromP Proxy 1
p1 t f x
l) (forall (n :: Natural) a x.
GenericP n a =>
Proxy n -> a -> RepP n a x
fromP Proxy 1
p1 t g x
r)
  where
      p1 :: Proxy 1
p1 = forall {k} (t :: k). Proxy t
Proxy @1
{-# INLINE gtprodDefault #-}

gtpureDefault
  :: forall t f x
  .  CanDeriveApplicativeT t f f x
  => (forall a . f a)
  -> t f x
gtpureDefault :: forall {k} {k} (t :: (k -> *) -> k -> *) (f :: k -> *) (x :: k).
CanDeriveApplicativeT t f f x =>
(forall (a :: k). f a) -> t f x
gtpureDefault forall (a :: k). f a
fa
  = forall (n :: Natural) a x.
GenericP n a =>
Proxy n -> RepP n a x -> a
toP (forall {k} (t :: k). Proxy t
Proxy @1) forall a b. (a -> b) -> a -> b
$ forall {k} {k} k (n :: k) (f :: k -> *) (g :: k -> *)
       (repbf :: k -> *) (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
(GApplicative n f g repbf repbg repbfg, f ~ g, repbf ~ repbg) =>
Proxy n
-> Proxy f
-> Proxy repbf
-> Proxy repbfg
-> (forall (a :: k). f a)
-> repbf x
gpure
      (forall {k} (t :: k). Proxy t
Proxy @1)
      (forall {k} (t :: k). Proxy t
Proxy @f)
      (forall {k} (t :: k). Proxy t
Proxy @(RepP 1 (t f x)))
      (forall {k} (t :: k). Proxy t
Proxy @(RepP 1 (t (f `Product` f) x)))
      forall (a :: k). f a
fa
{-# INLINE gtpureDefault #-}


-- ------------------------------------------------------------
-- Generic derivation: Special cases for ApplicativeT
-- -------------------------------------------------------------

type P = Param

instance
  (  ApplicativeT t
  ) => GApplicative 1 f g (Rec (t (P 1 f) x) (t f x))
                          (Rec (t (P 1 g) x) (t g x))
                          (Rec (t (P 1 (f `Product` g)) x) (t (f `Product` g) x))
  where
  gpure :: forall (x :: k).
(f ~ g, Rec (t (P 1 f) x) (t f x) ~ Rec (t (P 1 g) x) (t g x)) =>
Proxy 1
-> Proxy f
-> Proxy (Rec (t (P 1 f) x) (t f x))
-> Proxy (Rec (t (P 1 (Product f g)) x) (t (Product f g) x))
-> (forall (a :: k). f a)
-> Rec (t (P 1 f) x) (t f x) x
gpure Proxy 1
_ Proxy f
_ Proxy (Rec (t (P 1 f) x) (t f x))
_ Proxy (Rec (t (P 1 (Product f g)) x) (t (Product f g) x))
_ forall (a :: k). f a
fa
    = forall {k} p a (x :: k). K1 R a x -> Rec p a x
Rec (forall k i c (p :: k). c -> K1 i c p
K1 (forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k').
ApplicativeT t =>
(forall (a :: k). f a) -> t f x
tpure forall (a :: k). f a
fa))
  {-# INLINE gpure #-}

  gprod :: forall (x :: k).
Proxy 1
-> Proxy f
-> Proxy g
-> Rec (t (P 1 f) x) (t f x) x
-> Rec (t (P 1 g) x) (t g x) x
-> Rec (t (P 1 (Product f g)) x) (t (Product f g) x) x
gprod Proxy 1
_ Proxy f
_ Proxy g
_ (Rec (K1 t f x
tf)) (Rec (K1 t g x
tg))
    = forall {k} p a (x :: k). K1 R a x -> Rec p a x
Rec (forall k i c (p :: k). c -> K1 i c p
K1 (t f x
tf forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
       (g :: k -> *).
ApplicativeT t =>
t f x -> t g x -> t (Product f g) x
`tprod` t g x
tg))
  {-# INLINE gprod #-}



instance
  ( Applicative h
  , ApplicativeT t
  ) => GApplicative 1 f g (Rec (h (t (P 1 f) x)) (h (t f x)))
                          (Rec (h (t (P 1 g) x)) (h (t g x)))
                          (Rec (h (t (P 1 (f `Product` g)) x)) (h (t (f `Product` g) x)))
  where
  gpure :: forall (x :: k).
(f ~ g,
 Rec (h (t (P 1 f) x)) (h (t f x))
 ~ Rec (h (t (P 1 g) x)) (h (t g x))) =>
Proxy 1
-> Proxy f
-> Proxy (Rec (h (t (P 1 f) x)) (h (t f x)))
-> Proxy
     (Rec (h (t (P 1 (Product f g)) x)) (h (t (Product f g) x)))
-> (forall (a :: k). f a)
-> Rec (h (t (P 1 f) x)) (h (t f x)) x
gpure Proxy 1
_ Proxy f
_ Proxy (Rec (h (t (P 1 f) x)) (h (t f x)))
_ Proxy (Rec (h (t (P 1 (Product f g)) x)) (h (t (Product f g) x)))
_ forall (a :: k). f a
fa
    = forall {k} p a (x :: k). K1 R a x -> Rec p a x
Rec (forall k i c (p :: k). c -> K1 i c p
K1 (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k').
ApplicativeT t =>
(forall (a :: k). f a) -> t f x
tpure forall (a :: k). f a
fa))
  {-# INLINE gpure #-}

  gprod :: forall (x :: k).
Proxy 1
-> Proxy f
-> Proxy g
-> Rec (h (t (P 1 f) x)) (h (t f x)) x
-> Rec (h (t (P 1 g) x)) (h (t g x)) x
-> Rec (h (t (P 1 (Product f g)) x)) (h (t (Product f g) x)) x
gprod Proxy 1
_ Proxy f
_ Proxy g
_ (Rec (K1 h (t f x)
htf)) (Rec (K1 h (t g x)
htg))
    = forall {k} p a (x :: k). K1 R a x -> Rec p a x
Rec (forall k i c (p :: k). c -> K1 i c p
K1 (forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
       (g :: k -> *).
ApplicativeT t =>
t f x -> t g x -> t (Product f g) x
tprod forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> h (t f x)
htf forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> h (t g x)
htg))
  {-# INLINE gprod #-}


-- This is the same as the previous instance, but for nested Applicatives.
instance
  ( Applicative h
  , Applicative m
  , ApplicativeT t
  ) => GApplicative 1 f g (Rec (m (h (t (P 1 f) x))) (m (h (t f x))))
                          (Rec (m (h (t (P 1 g) x))) (m (h (t g x))))
                          (Rec (m (h (t (P 1 (f `Product` g)) x))) (m (h (t (f `Product` g) x))))
  where
  gpure :: forall (x :: k).
(f ~ g,
 Rec (m (h (t (P 1 f) x))) (m (h (t f x)))
 ~ Rec (m (h (t (P 1 g) x))) (m (h (t g x)))) =>
Proxy 1
-> Proxy f
-> Proxy (Rec (m (h (t (P 1 f) x))) (m (h (t f x))))
-> Proxy
     (Rec (m (h (t (P 1 (Product f g)) x))) (m (h (t (Product f g) x))))
-> (forall (a :: k). f a)
-> Rec (m (h (t (P 1 f) x))) (m (h (t f x))) x
gpure Proxy 1
_ Proxy f
_ Proxy (Rec (m (h (t (P 1 f) x))) (m (h (t f x))))
_ Proxy
  (Rec (m (h (t (P 1 (Product f g)) x))) (m (h (t (Product f g) x))))
_ forall (a :: k). f a
x
    = forall {k} p a (x :: k). K1 R a x -> Rec p a x
Rec (forall k i c (p :: k). c -> K1 i c p
K1 (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k').
ApplicativeT t =>
(forall (a :: k). f a) -> t f x
tpure forall (a :: k). f a
x))
  {-# INLINE gpure #-}

  gprod :: forall (x :: k).
Proxy 1
-> Proxy f
-> Proxy g
-> Rec (m (h (t (P 1 f) x))) (m (h (t f x))) x
-> Rec (m (h (t (P 1 g) x))) (m (h (t g x))) x
-> Rec
     (m (h (t (P 1 (Product f g)) x))) (m (h (t (Product f g) x))) x
gprod Proxy 1
_ Proxy f
_ Proxy g
_ (Rec (K1 m (h (t f x))
htfx)) (Rec (K1 m (h (t g x))
htgx))
    = forall {k} p a (x :: k). K1 R a x -> Rec p a x
Rec (forall k i c (p :: k). c -> K1 i c p
K1 (forall {k} {k'} {f :: * -> *} {t :: (k -> *) -> k' -> *}
       {f :: k -> *} {x :: k'} {g :: k -> *}.
(Applicative f, ApplicativeT t) =>
f (t f x) -> f (t g x) -> f (t (Product f g) x)
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (h (t f x))
htfx forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (h (t g x))
htgx))
    where
      go :: f (t f x) -> f (t g x) -> f (t (Product f g) x)
go f (t f x)
a f (t g x)
b = forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
       (g :: k -> *).
ApplicativeT t =>
t f x -> t g x -> t (Product f g) x
tprod forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (t f x)
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (t g x)
b
  {-# INLINE gprod #-}


-- --------------------------------
-- Instances for base types
-- --------------------------------

instance Applicative f => ApplicativeT (Compose f) where
  tpure :: forall (f :: k' -> *) (x :: k').
(forall (a :: k'). f a) -> Compose f f x
tpure forall (a :: k'). f a
fa
    = forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (a :: k'). f a
fa)
  {-# INLINE tpure #-}

  tprod :: forall (f :: k' -> *) (x :: k') (g :: k' -> *).
Compose f f x -> Compose f g x -> Compose f (Product f g) x
tprod (Compose f (f x)
fga) (Compose f (g x)
fha)
    = forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f x)
fga forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (g x)
fha)
  {-# INLINE tprod #-}

instance ApplicativeT Reverse where
  tpure :: forall (f :: k' -> *) (x :: k').
(forall (a :: k'). f a) -> Reverse f x
tpure forall (a :: k'). f a
fa
    = forall {k} (f :: k -> *) (a :: k). f a -> Reverse f a
Reverse forall (a :: k'). f a
fa
  {-# INLINE tpure #-}

  tprod :: forall (f :: k' -> *) (x :: k') (g :: k' -> *).
Reverse f x -> Reverse g x -> Reverse (Product f g) x
tprod (Reverse f x
fa) (Reverse g x
ga)
    = forall {k} (f :: k -> *) (a :: k). f a -> Reverse f a
Reverse (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair f x
fa g x
ga)
  {-# INLINE tprod #-}


instance Alternative f => ApplicativeT (Product f) where
  tpure :: forall (f :: * -> *) x. (forall a. f a) -> Product f f x
tpure forall a. f a
fa
    = forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair forall (f :: * -> *) a. Alternative f => f a
empty forall a. f a
fa
  {-# INLINE tpure #-}

  tprod :: forall (f :: * -> *) x (g :: * -> *).
Product f f x -> Product f g x -> Product f (Product f g) x
tprod (Pair f x
fl f x
gl) (Pair f x
fr g x
gr)
    = forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair (f x
fl forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> f x
fr) (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair f x
gl g x
gr)
  {-# INLINE tprod #-}

instance Alternative f => ApplicativeT (Sum f) where
  tpure :: forall (f :: * -> *) x. (forall a. f a) -> Sum f f x
tpure forall a. f a
fa
    = forall {k} (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR forall a. f a
fa
  {-# INLINE tpure #-}

  tprod :: forall (f :: * -> *) x (g :: * -> *).
Sum f f x -> Sum f g x -> Sum f (Product f g) x
tprod Sum f f x
l Sum f g x
r
    = case (Sum f f x
l, Sum f g x
r) of
        (InR f x
gl, InR g x
gr) -> forall {k} (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair f x
gl g x
gr)
        (InR f x
_,  InL f x
fr) -> forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL f x
fr
        (InL f x
fl, InR g x
_)  -> forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL f x
fl
        (InL f x
fl, InL f x
fr) -> forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL (f x
fl forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> f x
fr)
  {-# INLINE tprod #-}