{- | Exponentiation of a @Functor@ by a @Functor@.

For reference:

Powers of polynomial monads by David Spivak <https://topos.site/blog/2023/09/powers-of-polynomial-monads/>

-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE LambdaCase #-}
module Data.Functor.Exp where

import FFunctor
import GHC.Generics ((:*:)(..))
import Control.Monad (ap)
import Control.Comonad
import Control.Applicative
import FMonad
import FStrong
import Data.Functor.Day (Day(..))

newtype Exp1 f g a = Exp1 { forall (f :: * -> *) (g :: * -> *) a.
Exp1 f g a -> forall r. f r -> (a -> r) -> g r
unExp1 :: forall r. f r -> (a -> r) -> g r }
    deriving (forall a b. (a -> b) -> Exp1 f g a -> Exp1 f g b)
-> (forall a b. a -> Exp1 f g b -> Exp1 f g a)
-> Functor (Exp1 f g)
forall a b. a -> Exp1 f g b -> Exp1 f g a
forall a b. (a -> b) -> Exp1 f g a -> Exp1 f g b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (f :: * -> *) (g :: * -> *) a b.
a -> Exp1 f g b -> Exp1 f g a
forall (f :: * -> *) (g :: * -> *) a b.
(a -> b) -> Exp1 f g a -> Exp1 f g b
$cfmap :: forall (f :: * -> *) (g :: * -> *) a b.
(a -> b) -> Exp1 f g a -> Exp1 f g b
fmap :: forall a b. (a -> b) -> Exp1 f g a -> Exp1 f g b
$c<$ :: forall (f :: * -> *) (g :: * -> *) a b.
a -> Exp1 f g b -> Exp1 f g a
<$ :: forall a b. a -> Exp1 f g b -> Exp1 f g a
Functor

type (:^:) f g = Exp1 g f

toExp1 :: forall f g h. Functor g => ((f :*: g) ~> h) -> (g ~> Exp1 f h)
toExp1 :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Functor g =>
((f :*: g) ~> h) -> g ~> Exp1 f h
toExp1 (f :*: g) ~> h
fg2h g x
gx = (forall r. f r -> (x -> r) -> h r) -> Exp1 f h x
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> (a -> r) -> g r) -> Exp1 f g a
Exp1 (\f r
fr x -> r
xr -> (:*:) f g r -> h r
(f :*: g) ~> h
fg2h (f r
fr f r -> g r -> (:*:) f g r
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (x -> r) -> g x -> g r
forall a b. (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap x -> r
xr g x
gx))

fromExp1 :: forall f g h. (g ~> Exp1 f h) -> ((f :*: g) ~> h)
fromExp1 :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
(g ~> Exp1 f h) -> (f :*: g) ~> h
fromExp1 g ~> Exp1 f h
g2fh (f x
fx :*: g x
gx) = Exp1 f h x -> forall r. f r -> (x -> r) -> h r
forall (f :: * -> *) (g :: * -> *) a.
Exp1 f g a -> forall r. f r -> (a -> r) -> g r
unExp1 (g x -> Exp1 f h x
g ~> Exp1 f h
g2fh g x
gx) f x
fx x -> x
forall a. a -> a
id

evalExp1 :: (f :*: Exp1 f g) ~> g
evalExp1 :: forall (f :: * -> *) (g :: * -> *) x. (:*:) f (Exp1 f g) x -> g x
evalExp1 = (Exp1 f g ~> Exp1 f g) -> (f :*: Exp1 f g) ~> g
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
(g ~> Exp1 f h) -> (f :*: g) ~> h
fromExp1 Exp1 f g x -> Exp1 f g x
forall a. a -> a
Exp1 f g ~> Exp1 f g
id

coevalExp1 :: Functor g => g ~> Exp1 f (f :*: g)
coevalExp1 :: forall (g :: * -> *) (f :: * -> *).
Functor g =>
g ~> Exp1 f (f :*: g)
coevalExp1 = ((f :*: g) ~> (f :*: g)) -> g ~> Exp1 f (f :*: g)
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Functor g =>
((f :*: g) ~> h) -> g ~> Exp1 f h
toExp1 (:*:) f g x -> (:*:) f g x
forall a. a -> a
(f :*: g) ~> (f :*: g)
id

fromExp1' :: Functor f => Exp1 f g b -> f a -> g (Either a b)
fromExp1' :: forall (f :: * -> *) (g :: * -> *) b a.
Functor f =>
Exp1 f g b -> f a -> g (Either a b)
fromExp1' Exp1 f g b
e f a
fa = Exp1 f g b -> forall r. f r -> (b -> r) -> g r
forall (f :: * -> *) (g :: * -> *) a.
Exp1 f g a -> forall r. f r -> (a -> r) -> g r
unExp1 Exp1 f g b
e (a -> Either a b
forall a b. a -> Either a b
Left (a -> Either a b) -> f a -> f (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
fa) b -> Either a b
forall a b. b -> Either a b
Right

toExp1' :: Functor g => (forall a. f a -> g (Either a b)) -> Exp1 f g b
toExp1' :: forall (g :: * -> *) (f :: * -> *) b.
Functor g =>
(forall a. f a -> g (Either a b)) -> Exp1 f g b
toExp1' forall a. f a -> g (Either a b)
fg = (forall r. f r -> (b -> r) -> g r) -> Exp1 f g b
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> (a -> r) -> g r) -> Exp1 f g a
Exp1 ((forall r. f r -> (b -> r) -> g r) -> Exp1 f g b)
-> (forall r. f r -> (b -> r) -> g r) -> Exp1 f g b
forall a b. (a -> b) -> a -> b
$ \f r
fr b -> r
br -> (r -> r) -> (b -> r) -> Either r b -> r
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either r -> r
forall a. a -> a
id b -> r
br (Either r b -> r) -> g (Either r b) -> g r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f r -> g (Either r b)
forall a. f a -> g (Either a b)
fg f r
fr

instance (Functor f, Monad g) => Applicative (Exp1 f g) where
  pure :: forall a. a -> Exp1 f g a
pure a
a = (forall r. f r -> (a -> r) -> g r) -> Exp1 f g a
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> (a -> r) -> g r) -> Exp1 f g a
Exp1 ((forall r. f r -> (a -> r) -> g r) -> Exp1 f g a)
-> (forall r. f r -> (a -> r) -> g r) -> Exp1 f g a
forall a b. (a -> b) -> a -> b
$ \f r
_ a -> r
ar -> r -> g r
forall a. a -> g a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> r
ar a
a)
  <*> :: forall a b. Exp1 f g (a -> b) -> Exp1 f g a -> Exp1 f g b
(<*>) = Exp1 f g (a -> b) -> Exp1 f g a -> Exp1 f g b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance (Functor f, Monad g) => Monad (Exp1 f g) where
  Exp1 f g a
ma >>= :: forall a b. Exp1 f g a -> (a -> Exp1 f g b) -> Exp1 f g b
>>= a -> Exp1 f g b
k = (forall r. f r -> (b -> r) -> g r) -> Exp1 f g b
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> (a -> r) -> g r) -> Exp1 f g a
Exp1 ((forall r. f r -> (b -> r) -> g r) -> Exp1 f g b)
-> (forall r. f r -> (b -> r) -> g r) -> Exp1 f g b
forall a b. (a -> b) -> a -> b
$ \f r
fr b -> r
br ->
    Exp1 f g a -> f r -> g (Either r a)
forall (f :: * -> *) (g :: * -> *) b a.
Functor f =>
Exp1 f g b -> f a -> g (Either a b)
fromExp1' Exp1 f g a
ma f r
fr g (Either r a) -> (Either r a -> g r) -> g r
forall a b. g a -> (a -> g b) -> g b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Left r
r -> r -> g r
forall a. a -> g a
forall (f :: * -> *) a. Applicative f => a -> f a
pure r
r
      Right a
a -> Exp1 f g b -> forall r. f r -> (b -> r) -> g r
forall (f :: * -> *) (g :: * -> *) a.
Exp1 f g a -> forall r. f r -> (a -> r) -> g r
unExp1 (a -> Exp1 f g b
k a
a) f r
fr b -> r
br

-- | Equivalent to @'Data.Monoid.Alt' (Exp1 f g) a@
instance (Comonad f, Monad g) => Semigroup (Exp1 f g a) where
  <> :: Exp1 f g a -> Exp1 f g a -> Exp1 f g a
(<>) = Exp1 f g a -> Exp1 f g a -> Exp1 f g a
forall a. Exp1 f g a -> Exp1 f g a -> Exp1 f g a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>)

-- | Equivalent to @'Data.Monoid.Alt' (Exp1 f g) a@
instance (Comonad f, Monad g) => Monoid (Exp1 f g a) where
  mempty :: Exp1 f g a
mempty = Exp1 f g a
forall a. Exp1 f g a
forall (f :: * -> *) a. Alternative f => f a
empty

instance (Comonad f, Monad g) => Alternative (Exp1 f g) where
  empty :: forall a. Exp1 f g a
empty = (forall r. f r -> (a -> r) -> g r) -> Exp1 f g a
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> (a -> r) -> g r) -> Exp1 f g a
Exp1 ((forall r. f r -> (a -> r) -> g r) -> Exp1 f g a)
-> (forall r. f r -> (a -> r) -> g r) -> Exp1 f g a
forall a b. (a -> b) -> a -> b
$ \f r
fr a -> r
_ -> r -> g r
forall a. a -> g a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (f r -> r
forall a. f a -> a
forall (w :: * -> *) a. Comonad w => w a -> a
extract f r
fr)
  Exp1 f g a
m1 <|> :: forall a. Exp1 f g a -> Exp1 f g a -> Exp1 f g a
<|> Exp1 f g a
m2 = (forall r. f r -> (a -> r) -> g r) -> Exp1 f g a
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> (a -> r) -> g r) -> Exp1 f g a
Exp1 ((forall r. f r -> (a -> r) -> g r) -> Exp1 f g a)
-> (forall r. f r -> (a -> r) -> g r) -> Exp1 f g a
forall a b. (a -> b) -> a -> b
$ \f r
fr a -> r
ar ->
    Exp1 f g a -> f (f r) -> g (Either (f r) a)
forall (f :: * -> *) (g :: * -> *) b a.
Functor f =>
Exp1 f g b -> f a -> g (Either a b)
fromExp1' Exp1 f g a
m1 (f r -> f (f r)
forall a. f a -> f (f a)
forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate f r
fr) g (Either (f r) a) -> (Either (f r) a -> g r) -> g r
forall a b. g a -> (a -> g b) -> g b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Left f r
fr' -> Exp1 f g a -> forall r. f r -> (a -> r) -> g r
forall (f :: * -> *) (g :: * -> *) a.
Exp1 f g a -> forall r. f r -> (a -> r) -> g r
unExp1 Exp1 f g a
m2 f r
fr' a -> r
ar
      Right a
a  -> r -> g r
forall a. a -> g a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> r
ar a
a)


instance FFunctor (Exp1 f) where
  ffmap :: forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> Exp1 f g x -> Exp1 f h x
ffmap g ~> h
gh (Exp1 forall r. f r -> (x -> r) -> g r
e) = (forall r. f r -> (x -> r) -> h r) -> Exp1 f h x
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> (a -> r) -> g r) -> Exp1 f g a
Exp1 ((forall r. f r -> (x -> r) -> h r) -> Exp1 f h x)
-> (forall r. f r -> (x -> r) -> h r) -> Exp1 f h x
forall a b. (a -> b) -> a -> b
$ \f r
fr x -> r
ar -> g r -> h r
g ~> h
gh (f r -> (x -> r) -> g r
forall r. f r -> (x -> r) -> g r
e f r
fr x -> r
ar) 

-- | @g ~ Exp1 Proxy g@; @Exp1 f (Exp1 f g) ~ Exp1 (f :*: f) g@
instance Functor f => FMonad (Exp1 f) where
  fpure :: forall (g :: * -> *). Functor g => g ~> Exp1 f g
fpure g x
gx = (forall r. f r -> (x -> r) -> g r) -> Exp1 f g x
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> (a -> r) -> g r) -> Exp1 f g a
Exp1 ((forall r. f r -> (x -> r) -> g r) -> Exp1 f g x)
-> (forall r. f r -> (x -> r) -> g r) -> Exp1 f g x
forall a b. (a -> b) -> a -> b
$ \f r
_ x -> r
br -> x -> r
br (x -> r) -> g x -> g r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g x
gx
  fbind :: forall (g :: * -> *) (h :: * -> *) a.
(Functor g, Functor h) =>
(g ~> Exp1 f h) -> Exp1 f g a -> Exp1 f h a
fbind g ~> Exp1 f h
k Exp1 f g a
fgx = (forall r. f r -> (a -> r) -> h r) -> Exp1 f h a
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> (a -> r) -> g r) -> Exp1 f g a
Exp1 ((forall r. f r -> (a -> r) -> h r) -> Exp1 f h a)
-> (forall r. f r -> (a -> r) -> h r) -> Exp1 f h a
forall a b. (a -> b) -> a -> b
$ \f r
fr a -> r
yr ->
    Exp1 f h (Either r a) -> forall r. f r -> (Either r a -> r) -> h r
forall (f :: * -> *) (g :: * -> *) a.
Exp1 f g a -> forall r. f r -> (a -> r) -> g r
unExp1 (g (Either r a) -> Exp1 f h (Either r a)
g ~> Exp1 f h
k (Exp1 f g a -> f r -> g (Either r a)
forall (f :: * -> *) (g :: * -> *) b a.
Functor f =>
Exp1 f g b -> f a -> g (Either a b)
fromExp1' Exp1 f g a
fgx f r
fr)) f r
fr ((r -> r) -> (a -> r) -> Either r a -> r
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either r -> r
forall a. a -> a
id a -> r
yr)

instance Functor f => FStrong (Exp1 f) where
  fstrength :: forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (Exp1 f g) h ~> Exp1 f (Day g h)
fstrength (Day Exp1 f g b
mb h c
hc b -> c -> x
op) =
    (forall r. f r -> (x -> r) -> Day g h r) -> Exp1 f (Day g h) x
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> (a -> r) -> g r) -> Exp1 f g a
Exp1 ((forall r. f r -> (x -> r) -> Day g h r) -> Exp1 f (Day g h) x)
-> (forall r. f r -> (x -> r) -> Day g h r) -> Exp1 f (Day g h) x
forall a b. (a -> b) -> a -> b
$ \f r
fr x -> r
ar ->
      let op' :: Either r b -> c -> r
op' (Left r
r) c
_ = r
r
          op' (Right b
b) c
c = x -> r
ar (b -> c -> x
op b
b c
c)
      in g (Either r b) -> h c -> (Either r b -> c -> r) -> Day g h r
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day (Exp1 f g b -> f r -> g (Either r b)
forall (f :: * -> *) (g :: * -> *) b a.
Functor f =>
Exp1 f g b -> f a -> g (Either a b)
fromExp1' Exp1 f g b
mb f r
fr) h c
hc Either r b -> c -> r
op'