{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE NoImplicitPrelude #-}

module Data.Functor.Linear.Internal.Applicative
  (
    Applicative(..)
  ) where

import Data.Functor.Linear.Internal.Functor
import Prelude.Linear.Internal
import qualified Control.Monad.Trans.Reader as NonLinear
import Data.Monoid.Linear hiding (Sum)
import Data.Functor.Compose
import Data.Functor.Const
import Data.Functor.Identity

-- # Applicative definition
-------------------------------------------------------------------------------

-- | Data 'Applicative'-s can be seen as containers which can be zipped
-- together. A prime example of data 'Applicative' are vectors of known length
-- ('ZipList's would be, if it were not for the fact that zipping them together
-- drops values, which we are not allowed to do in a linear container).
--
-- In fact, an applicative functor is precisely a functor equipped with (pure
-- and) @liftA2 :: (a %1-> b %1-> c) -> f a %1-> f b %1-> f c@. In the case where
-- @f = []@, the signature of 'liftA2' would specialise to that of 'zipWith'.
--
-- Intuitively, the type of 'liftA2' means that 'Applicative's can be seen as
-- containers whose "number" of elements is known at compile-time. This
-- includes vectors of known length but excludes 'Maybe', since this may
-- contain either zero or one value.  Similarly, @((->) r)@ forms a Data
-- 'Applicative', since this is a (possibly infinitary) container indexed by
-- @r@, while lists do not, since they may contain any number of elements.
--
-- == Remarks for the mathematically inclined
--
-- An 'Applicative' is, as in the restricted case, a lax monoidal endofunctor of
-- the category of linear types. That is, it is equipped with
--
-- * a (linear) function @() %1-> f ()@
-- * a (linear) natural transformation @(f a, f b) %1-> f (a, b)@
--
-- It is a simple exercise to verify that these are equivalent to the definition
-- of 'Applicative'. Hence that the choice of linearity of the various arrow is
-- indeed natural.
class Functor f => Applicative f where
  {-# MINIMAL pure, (liftA2 | (<*>)) #-}
  pure :: a -> f a
  (<*>) :: f (a %1-> b) %1-> f a %1-> f b
  f (a %1 -> b)
f <*> f a
x = ((a %1 -> b) %1 -> a %1 -> b) -> f (a %1 -> b) %1 -> f a %1 -> f b
forall (f :: * -> *) a b c.
Applicative f =>
(a %1 -> b %1 -> c) -> f a %1 -> f b %1 -> f c
liftA2 (a %1 -> b) %1 -> a %1 -> b
forall a b. (a %1 -> b) %1 -> a %1 -> b
($) f (a %1 -> b)
f f a
x
  liftA2 :: (a %1-> b %1-> c) -> f a %1-> f b %1-> f c
  liftA2 a %1 -> b %1 -> c
f f a
x f b
y = a %1 -> b %1 -> c
f (a %1 -> b %1 -> c) -> f a %1 -> f (b %1 -> c)
forall (f :: * -> *) a b. Functor f => (a %1 -> b) -> f a %1 -> f b
<$> f a
x f (b %1 -> c) %1 -> f b %1 -> f c
forall (f :: * -> *) a b.
Applicative f =>
f (a %1 -> b) %1 -> f a %1 -> f b
<*> f b
y

-- # Instances
-------------------------------------------------------------------------------

instance Monoid x => Applicative (Const x) where
  pure :: forall a. a -> Const x a
pure a
_ = x -> Const x a
forall {k} a (b :: k). a -> Const a b
Const x
forall a. Monoid a => a
mempty
  Const x
x <*> :: forall a b. Const x (a %1 -> b) %1 -> Const x a %1 -> Const x b
<*> Const x
y = x %1 -> Const x b
forall {k} a (b :: k). a -> Const a b
Const (x
x x %1 -> x %1 -> x
forall a. Semigroup a => a %1 -> a %1 -> a
<> x
y)

instance Monoid a => Applicative ((,) a) where
  pure :: forall a. a -> (a, a)
pure a
x = (a
forall a. Monoid a => a
mempty, a
x)
  (a
u,a %1 -> b
f) <*> :: forall a b. (a, a %1 -> b) %1 -> (a, a) %1 -> (a, b)
<*> (a
v,a
x) = (a
u a %1 -> a %1 -> a
forall a. Semigroup a => a %1 -> a %1 -> a
<> a
v, a %1 -> b
f a
x)

instance Applicative Identity where
  pure :: forall a. a -> Identity a
pure = a -> Identity a
forall a. a -> Identity a
Identity
  Identity a %1 -> b
f <*> :: forall a b. Identity (a %1 -> b) %1 -> Identity a %1 -> Identity b
<*> Identity a
x = b %1 -> Identity b
forall a. a -> Identity a
Identity (a %1 -> b
f a
x)

instance (Applicative f, Applicative g) => Applicative (Compose f g) where
   pure :: forall a. a -> Compose f g a
pure a
x = f (g a) -> Compose f g a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (g a -> f (g a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> g a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x))
   (Compose f (g (a %1 -> b))
f) <*> :: forall a b.
Compose f g (a %1 -> b) %1 -> Compose f g a %1 -> Compose f g b
<*> (Compose f (g a)
x) = f (g b) %1 -> Compose f g b
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose ((g (a %1 -> b) %1 -> g a %1 -> g b)
-> f (g (a %1 -> b)) %1 -> f (g a) %1 -> f (g b)
forall (f :: * -> *) a b c.
Applicative f =>
(a %1 -> b %1 -> c) -> f a %1 -> f b %1 -> f c
liftA2 g (a %1 -> b) %1 -> g a %1 -> g b
forall (f :: * -> *) a b.
Applicative f =>
f (a %1 -> b) %1 -> f a %1 -> f b
(<*>) f (g (a %1 -> b))
f f (g a)
x)
   liftA2 :: forall a b c.
(a %1 -> b %1 -> c)
-> Compose f g a %1 -> Compose f g b %1 -> Compose f g c
liftA2 a %1 -> b %1 -> c
f (Compose f (g a)
x) (Compose f (g b)
y) = f (g c) %1 -> Compose f g c
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose ((g a %1 -> g b %1 -> g c) -> f (g a) %1 -> f (g b) %1 -> f (g c)
forall (f :: * -> *) a b c.
Applicative f =>
(a %1 -> b %1 -> c) -> f a %1 -> f b %1 -> f c
liftA2 ((a %1 -> b %1 -> c) -> g a %1 -> g b %1 -> g c
forall (f :: * -> *) a b c.
Applicative f =>
(a %1 -> b %1 -> c) -> f a %1 -> f b %1 -> f c
liftA2 a %1 -> b %1 -> c
f) f (g a)
x f (g b)
y)

instance Applicative m => Applicative (NonLinear.ReaderT r m) where
  pure :: forall a. a -> ReaderT r m a
pure a
x = (r -> m a) -> ReaderT r m a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
NonLinear.ReaderT (\r
_ -> a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x)
  NonLinear.ReaderT r -> m (a %1 -> b)
f <*> :: forall a b.
ReaderT r m (a %1 -> b) %1 -> ReaderT r m a %1 -> ReaderT r m b
<*> NonLinear.ReaderT r -> m a
x = (r -> m b) %1 -> ReaderT r m b
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
NonLinear.ReaderT (\r
r -> r -> m (a %1 -> b)
f r
r m (a %1 -> b) %1 -> m a %1 -> m b
forall (f :: * -> *) a b.
Applicative f =>
f (a %1 -> b) %1 -> f a %1 -> f b
<*> r -> m a
x r
r)