{-# LANGUAGE GADTs #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# OPTIONS_HADDOCK hide #-}

-- | A few things lifted from kan-extensions and lens for generic deriving of
-- 'Data.Functor.Linear.Traversable' instances (see
-- "Data.Functor.Linear.Internal.Traversable").
module Control.Functor.Linear.Internal.Kan where

import Control.Functor.Linear
import qualified Data.Functor.Linear.Internal.Applicative as Data
import qualified Data.Functor.Linear.Internal.Functor as Data
import Prelude.Linear.Internal

-- | A linear version of @Data.Functor.Day.Curried.Curried@ in the
-- @kan-extensions@ package. We use this for generic traversals. How
-- does it help? Consider a type like
--
-- @data Foo a = Foo a a a a@
--
-- The generic representation may look roughly like
--
-- @D1 _ (C1 _ ((S1 _ Rec1 :*: S1 _ Rec1) :*: (S1 _ Rec1 :*: S1 _ Rec1)))@
--
-- Traversing this naively requires a bunch of @fmap@ applications.
-- Most of them could be removed using 'Yoneda', but one aspect
-- can't be. Let's simplify down to the hard bit:
--
-- @m :*: (n :*: o)@
--
-- Traversing this looks like
--
-- @((:*:) <$> m) <*> ((:*:) <$> n <*> o)@
--
-- We want to reassociate the applications so the whole reconstruction
-- of the generic representation happens in one place, allowing inlining
-- to (hopefully) erase them altogether. It will end up looking roughly like
--
-- @(\x y z -> x :*: (y :*: z)) <$> m <*> n <*> o@
--
-- In our context, we always have the two functor
-- arguments the same, so something like @Curried f f@.
-- @Curried f f a@ is a lot like @f a@, as demonstrated directly by
-- 'lowerCurriedC' and, in @kan-extensions@, @liftCurried@.
-- It's a sort of "continuation passing style" version. If we have
-- something like
--
-- @
-- Con <$> m <*> n <*> o
--
-- -- parenthesized
--
-- ((Con <$> m) <*> n) <*> o
-- @
--
-- we can look at what happens next to each field. So the next thing
-- after performing @m@ is to map @Con@ over it. The next thing after
-- performing @n@ is to apply @Con <$> m@ to it within the functor.
newtype Curried g h a = Curried
  {forall (g :: * -> *) (h :: * -> *) a.
Curried g h a -> forall r. g (a %1 -> r) %1 -> h r
runCurried :: forall r. g (a %1 -> r) %1 -> h r}

instance Data.Functor g => Data.Functor (Curried g h) where
  fmap :: forall a b. (a %1 -> b) -> Curried g h a %1 -> Curried g h b
fmap a %1 -> b
f (Curried forall r. g (a %1 -> r) %1 -> h r
g) = forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a %1 -> r) %1 -> h r) -> Curried g h a
Curried (forall r. g (a %1 -> r) %1 -> h r
g forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. forall (f :: * -> *) a b. Functor f => (a %1 -> b) -> f a %1 -> f b
Data.fmap (forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. a %1 -> b
f))
  {-# INLINE fmap #-}

instance Functor g => Functor (Curried g h) where
  fmap :: forall a b. (a %1 -> b) %1 -> Curried g h a %1 -> Curried g h b
fmap a %1 -> b
f (Curried forall r. g (a %1 -> r) %1 -> h r
g) = forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a %1 -> r) %1 -> h r) -> Curried g h a
Curried (\g (b %1 -> r)
x -> forall r. g (a %1 -> r) %1 -> h r
g (forall (f :: * -> *) a b.
Functor f =>
(a %1 -> b) %1 -> f a %1 -> f b
fmap (\b %1 -> r
y -> b %1 -> r
y forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. a %1 -> b
f) g (b %1 -> r)
x))
  {-# INLINE fmap #-}

instance (Data.Functor g, g ~ h) => Data.Applicative (Curried g h) where
  pure :: forall a. a -> Curried g h a
pure a
a = forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a %1 -> r) %1 -> h r) -> Curried g h a
Curried (forall (f :: * -> *) a b. Functor f => (a %1 -> b) -> f a %1 -> f b
Data.fmap (forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ a
a))
  {-# INLINE pure #-}
  Curried forall r. g ((a %1 -> b) %1 -> r) %1 -> h r
mf <*> :: forall a b.
Curried g h (a %1 -> b) %1 -> Curried g h a %1 -> Curried g h b
<*> Curried forall r. g (a %1 -> r) %1 -> h r
ma = forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a %1 -> r) %1 -> h r) -> Curried g h a
Curried (forall r. g (a %1 -> r) %1 -> h r
ma forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. forall r. g ((a %1 -> b) %1 -> r) %1 -> h r
mf forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. forall (f :: * -> *) a b. Functor f => (a %1 -> b) -> f a %1 -> f b
Data.fmap forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
(.))
  {-# INLINE (<*>) #-}

instance (Functor g, g ~ h) => Applicative (Curried g h) where
  pure :: forall a. a %1 -> Curried g h a
pure a
a = forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a %1 -> r) %1 -> h r) -> Curried g h a
Curried (forall (f :: * -> *) a b.
Functor f =>
(a %1 -> b) %1 -> f a %1 -> f b
fmap (forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ a
a))
  {-# INLINE pure #-}
  Curried forall r. g ((a %1 -> b) %1 -> r) %1 -> h r
mf <*> :: forall a b.
Curried g h (a %1 -> b) %1 -> Curried g h a %1 -> Curried g h b
<*> Curried forall r. g (a %1 -> r) %1 -> h r
ma = forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a %1 -> r) %1 -> h r) -> Curried g h a
Curried (forall r. g (a %1 -> r) %1 -> h r
ma forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. forall r. g ((a %1 -> b) %1 -> r) %1 -> h r
mf forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. forall (f :: * -> *) a b.
Functor f =>
(a %1 -> b) %1 -> f a %1 -> f b
fmap forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
(.))
  {-# INLINE (<*>) #-}

lowerCurriedC :: Applicative f => Curried f g a %1 -> g a
lowerCurriedC :: forall (f :: * -> *) (g :: * -> *) a.
Applicative f =>
Curried f g a %1 -> g a
lowerCurriedC (Curried forall r. f (a %1 -> r) %1 -> g r
f) = forall r. f (a %1 -> r) %1 -> g r
f (forall (f :: * -> *) a. Applicative f => a %1 -> f a
pure forall a (q :: Multiplicity). a %q -> a
id)
{-# INLINE lowerCurriedC #-}

newtype Yoneda f a = Yoneda {forall (f :: * -> *) a.
Yoneda f a -> forall b. (a %1 -> b) %1 -> f b
runYoneda :: forall b. (a %1 -> b) %1 -> f b}

instance Data.Functor (Yoneda f) where
  fmap :: forall a b. (a %1 -> b) -> Yoneda f a %1 -> Yoneda f b
fmap a %1 -> b
f (Yoneda forall b. (a %1 -> b) %1 -> f b
m) = forall (f :: * -> *) a.
(forall b. (a %1 -> b) %1 -> f b) -> Yoneda f a
Yoneda (\b %1 -> b
k -> forall b. (a %1 -> b) %1 -> f b
m (b %1 -> b
k forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. a %1 -> b
f))
  {-# INLINE fmap #-}

instance Functor (Yoneda f) where
  fmap :: forall a b. (a %1 -> b) %1 -> Yoneda f a %1 -> Yoneda f b
fmap a %1 -> b
f (Yoneda forall b. (a %1 -> b) %1 -> f b
m) = forall (f :: * -> *) a.
(forall b. (a %1 -> b) %1 -> f b) -> Yoneda f a
Yoneda (\b %1 -> b
k -> forall b. (a %1 -> b) %1 -> f b
m (b %1 -> b
k forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. a %1 -> b
f))
  {-# INLINE fmap #-}

instance Applicative f => Data.Applicative (Yoneda f) where
  pure :: forall a. a -> Yoneda f a
pure a
a = forall (f :: * -> *) a.
(forall b. (a %1 -> b) %1 -> f b) -> Yoneda f a
Yoneda (\a %1 -> b
f -> forall (f :: * -> *) a. Applicative f => a %1 -> f a
pure (a %1 -> b
f a
a))
  {-# INLINE pure #-}
  Yoneda forall b. ((a %1 -> b) %1 -> b) %1 -> f b
m <*> :: forall a b. Yoneda f (a %1 -> b) %1 -> Yoneda f a %1 -> Yoneda f b
<*> Yoneda forall b. (a %1 -> b) %1 -> f b
n = forall (f :: * -> *) a.
(forall b. (a %1 -> b) %1 -> f b) -> Yoneda f a
Yoneda (\b %1 -> b
f -> forall b. ((a %1 -> b) %1 -> b) %1 -> f b
m (\a %1 -> b
g -> b %1 -> b
f forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. a %1 -> b
g) forall (f :: * -> *) a b.
Applicative f =>
f (a %1 -> b) %1 -> f a %1 -> f b
<*> forall b. (a %1 -> b) %1 -> f b
n forall a (q :: Multiplicity). a %q -> a
id)
  {-# INLINE (<*>) #-}

instance Applicative f => Applicative (Yoneda f) where
  pure :: forall a. a %1 -> Yoneda f a
pure a
a = forall (f :: * -> *) a.
(forall b. (a %1 -> b) %1 -> f b) -> Yoneda f a
Yoneda (\a %1 -> b
f -> forall (f :: * -> *) a. Applicative f => a %1 -> f a
pure (a %1 -> b
f a
a))
  {-# INLINE pure #-}
  Yoneda forall b. ((a %1 -> b) %1 -> b) %1 -> f b
m <*> :: forall a b. Yoneda f (a %1 -> b) %1 -> Yoneda f a %1 -> Yoneda f b
<*> Yoneda forall b. (a %1 -> b) %1 -> f b
n = forall (f :: * -> *) a.
(forall b. (a %1 -> b) %1 -> f b) -> Yoneda f a
Yoneda (\b %1 -> b
f -> forall b. ((a %1 -> b) %1 -> b) %1 -> f b
m (\a %1 -> b
g -> b %1 -> b
f forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. a %1 -> b
g) forall (f :: * -> *) a b.
Applicative f =>
f (a %1 -> b) %1 -> f a %1 -> f b
<*> forall b. (a %1 -> b) %1 -> f b
n forall a (q :: Multiplicity). a %q -> a
id)
  {-# INLINE (<*>) #-}

lowerYoneda :: Yoneda f a %1 -> f a
lowerYoneda :: forall (f :: * -> *) a. Yoneda f a %1 -> f a
lowerYoneda (Yoneda forall b. (a %1 -> b) %1 -> f b
m) = forall b. (a %1 -> b) %1 -> f b
m forall a (q :: Multiplicity). a %q -> a
id
{-# INLINE lowerYoneda #-}

-- This bit comes from lens.
liftCurriedYonedaC :: Applicative f => f a %1 -> Curried (Yoneda f) (Yoneda f) a
liftCurriedYonedaC :: forall (f :: * -> *) a.
Applicative f =>
f a %1 -> Curried (Yoneda f) (Yoneda f) a
liftCurriedYonedaC f a
fa = forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a %1 -> r) %1 -> h r) -> Curried g h a
Curried (forall (f :: * -> *) a b.
Applicative f =>
Yoneda f (a %1 -> b) %1 -> f a %1 -> Yoneda f b
`yap` f a
fa)
{-# INLINE liftCurriedYonedaC #-}

yap :: Applicative f => Yoneda f (a %1 -> b) %1 -> f a %1 -> Yoneda f b
yap :: forall (f :: * -> *) a b.
Applicative f =>
Yoneda f (a %1 -> b) %1 -> f a %1 -> Yoneda f b
yap (Yoneda forall b. ((a %1 -> b) %1 -> b) %1 -> f b
k) f a
fa = forall (f :: * -> *) a.
(forall b. (a %1 -> b) %1 -> f b) -> Yoneda f a
Yoneda (\b %1 -> b
ab_r -> forall b. ((a %1 -> b) %1 -> b) %1 -> f b
k (\a %1 -> b
g -> b %1 -> b
ab_r forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. a %1 -> b
g) forall (f :: * -> *) a b.
Applicative f =>
f (a %1 -> b) %1 -> f a %1 -> f b
<*> f a
fa)
{-# INLINE yap #-}