{-# 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 r. g (b %1 -> r) %1 -> h r) -> Curried g h b
forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a %1 -> r) %1 -> h r) -> Curried g h a
Curried (g (a %1 -> r) %1 -> h r
forall r. g (a %1 -> r) %1 -> h r
g (g (a %1 -> r) %1 -> h r)
%1 -> (g (b %1 -> r) %1 -> g (a %1 -> r))
-> g (b %1 -> r)
%1 -> h r
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. ((b %1 -> r) %1 -> a %1 -> r) -> g (b %1 -> r) %1 -> g (a %1 -> r)
forall a b. (a %1 -> b) -> g a %1 -> g b
forall (f :: * -> *) a b. Functor f => (a %1 -> b) -> f a %1 -> f b
Data.fmap ((b %1 -> r) %1 -> (a %1 -> b) -> a %1 -> 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
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 r. g (b %1 -> r) %1 -> h r) -> Curried g h b
forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a %1 -> r) %1 -> h r) -> Curried g h a
Curried (\g (b %1 -> r)
x -> g (a %1 -> r) %1 -> h r
forall r. g (a %1 -> r) %1 -> h r
g (((b %1 -> r) %1 -> a %1 -> r)
%1 -> g (b %1 -> r) %1 -> g (a %1 -> r)
forall a b. (a %1 -> b) %1 -> g a %1 -> g b
forall (f :: * -> *) a b.
Functor f =>
(a %1 -> b) %1 -> f a %1 -> f b
fmap (\b %1 -> r
y -> b %1 -> r
y (b %1 -> r) %1 -> (a %1 -> b) %1 -> a %1 -> 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
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 r. g (a %1 -> r) %1 -> h r) -> Curried g h a
forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a %1 -> r) %1 -> h r) -> Curried g h a
Curried (((a %1 -> r) %1 -> r) -> g (a %1 -> r) %1 -> g r
forall a b. (a %1 -> b) -> g a %1 -> g b
forall (f :: * -> *) a b. Functor f => (a %1 -> b) -> f a %1 -> f b
Data.fmap ((a %1 -> r) %1 -> a %1 -> r
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 r. g (b %1 -> r) %1 -> h r) -> Curried g h b
forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a %1 -> r) %1 -> h r) -> Curried g h a
Curried (g (a %1 -> r) %1 -> h r
forall r. g (a %1 -> r) %1 -> h r
ma (g (a %1 -> r) %1 -> h r)
%1 -> (g (b %1 -> r) %1 -> g (a %1 -> r))
%1 -> g (b %1 -> r)
%1 -> h r
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. g ((a %1 -> b) %1 -> a %1 -> r) %1 -> g (a %1 -> r)
g ((a %1 -> b) %1 -> a %1 -> r) %1 -> h (a %1 -> r)
forall r. g ((a %1 -> b) %1 -> r) %1 -> h r
mf (g ((a %1 -> b) %1 -> a %1 -> r) %1 -> g (a %1 -> r))
%1 -> (g (b %1 -> r) %1 -> g ((a %1 -> b) %1 -> a %1 -> r))
-> g (b %1 -> r)
%1 -> g (a %1 -> r)
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. ((b %1 -> r) %1 -> (a %1 -> b) %1 -> a %1 -> r)
-> g (b %1 -> r) %1 -> g ((a %1 -> b) %1 -> a %1 -> r)
forall a b. (a %1 -> b) -> g a %1 -> g b
forall (f :: * -> *) a b. Functor f => (a %1 -> b) -> f a %1 -> f b
Data.fmap (b %1 -> r) %1 -> (a %1 -> b) %1 -> a %1 -> r
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 r. g (a %1 -> r) %1 -> h r) -> Curried g h a
forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a %1 -> r) %1 -> h r) -> Curried g h a
Curried (((a %1 -> r) %1 -> r) %1 -> g (a %1 -> r) %1 -> g r
forall a b. (a %1 -> b) %1 -> g a %1 -> g b
forall (f :: * -> *) a b.
Functor f =>
(a %1 -> b) %1 -> f a %1 -> f b
fmap ((a %1 -> r) %1 -> a %1 -> r
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 r. g (b %1 -> r) %1 -> h r) -> Curried g h b
forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a %1 -> r) %1 -> h r) -> Curried g h a
Curried (g (a %1 -> r) %1 -> h r
forall r. g (a %1 -> r) %1 -> h r
ma (g (a %1 -> r) %1 -> h r)
%1 -> (g (b %1 -> r) %1 -> g (a %1 -> r))
%1 -> g (b %1 -> r)
%1 -> h r
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. g ((a %1 -> b) %1 -> a %1 -> r) %1 -> g (a %1 -> r)
g ((a %1 -> b) %1 -> a %1 -> r) %1 -> h (a %1 -> r)
forall r. g ((a %1 -> b) %1 -> r) %1 -> h r
mf (g ((a %1 -> b) %1 -> a %1 -> r) %1 -> g (a %1 -> r))
%1 -> (g (b %1 -> r) %1 -> g ((a %1 -> b) %1 -> a %1 -> r))
-> g (b %1 -> r)
%1 -> g (a %1 -> r)
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. ((b %1 -> r) %1 -> (a %1 -> b) %1 -> a %1 -> r)
%1 -> g (b %1 -> r) %1 -> g ((a %1 -> b) %1 -> a %1 -> r)
forall a b. (a %1 -> b) %1 -> g a %1 -> g b
forall (f :: * -> *) a b.
Functor f =>
(a %1 -> b) %1 -> f a %1 -> f b
fmap (b %1 -> r) %1 -> (a %1 -> b) %1 -> a %1 -> r
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) = f (a %1 -> a) %1 -> g a
forall r. f (a %1 -> r) %1 -> g r
f ((a %1 -> a) %1 -> f (a %1 -> a)
forall a. a %1 -> f a
forall (f :: * -> *) a. Applicative f => a %1 -> f a
pure a %1 -> a
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 b. (b %1 -> b) %1 -> f b) -> Yoneda f b
forall (f :: * -> *) a.
(forall b. (a %1 -> b) %1 -> f b) -> Yoneda f a
Yoneda (\b %1 -> b
k -> (a %1 -> b) %1 -> f b
forall b. (a %1 -> b) %1 -> f b
m (b %1 -> b
k (b %1 -> b) %1 -> (a %1 -> b) -> a %1 -> b
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 b. (b %1 -> b) %1 -> f b) -> Yoneda f b
forall (f :: * -> *) a.
(forall b. (a %1 -> b) %1 -> f b) -> Yoneda f a
Yoneda (\b %1 -> b
k -> (a %1 -> b) %1 -> f b
forall b. (a %1 -> b) %1 -> f b
m (b %1 -> b
k (b %1 -> b) %1 -> (a %1 -> b) %1 -> a %1 -> b
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 b. (a %1 -> b) %1 -> f b) -> Yoneda f a
forall (f :: * -> *) a.
(forall b. (a %1 -> b) %1 -> f b) -> Yoneda f a
Yoneda (\a %1 -> b
f -> b %1 -> f b
forall a. a %1 -> f a
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 b. (b %1 -> b) %1 -> f b) -> Yoneda f b
forall (f :: * -> *) a.
(forall b. (a %1 -> b) %1 -> f b) -> Yoneda f a
Yoneda (\b %1 -> b
f -> ((a %1 -> b) %1 -> a %1 -> b) %1 -> f (a %1 -> b)
forall b. ((a %1 -> b) %1 -> b) %1 -> f b
m (\a %1 -> b
g -> b %1 -> b
f (b %1 -> b) %1 -> (a %1 -> b) %1 -> a %1 -> b
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) f (a %1 -> b) %1 -> f a %1 -> f b
forall a b. f (a %1 -> b) %1 -> f a %1 -> f b
forall (f :: * -> *) a b.
Applicative f =>
f (a %1 -> b) %1 -> f a %1 -> f b
<*> (a %1 -> a) %1 -> f a
forall b. (a %1 -> b) %1 -> f b
n a %1 -> a
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 b. (a %1 -> b) %1 -> f b) -> Yoneda f a
forall (f :: * -> *) a.
(forall b. (a %1 -> b) %1 -> f b) -> Yoneda f a
Yoneda (\a %1 -> b
f -> b %1 -> f b
forall a. a %1 -> f a
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 b. (b %1 -> b) %1 -> f b) -> Yoneda f b
forall (f :: * -> *) a.
(forall b. (a %1 -> b) %1 -> f b) -> Yoneda f a
Yoneda (\b %1 -> b
f -> ((a %1 -> b) %1 -> a %1 -> b) %1 -> f (a %1 -> b)
forall b. ((a %1 -> b) %1 -> b) %1 -> f b
m (\a %1 -> b
g -> b %1 -> b
f (b %1 -> b) %1 -> (a %1 -> b) %1 -> a %1 -> b
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) f (a %1 -> b) %1 -> f a %1 -> f b
forall a b. f (a %1 -> b) %1 -> f a %1 -> f b
forall (f :: * -> *) a b.
Applicative f =>
f (a %1 -> b) %1 -> f a %1 -> f b
<*> (a %1 -> a) %1 -> f a
forall b. (a %1 -> b) %1 -> f b
n a %1 -> a
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) = (a %1 -> a) %1 -> f a
forall b. (a %1 -> b) %1 -> f b
m a %1 -> a
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 r. Yoneda f (a %1 -> r) %1 -> Yoneda f r)
-> Curried (Yoneda f) (Yoneda f) a
forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a %1 -> r) %1 -> h r) -> Curried g h a
Curried (Yoneda f (a %1 -> r) %1 -> f a %1 -> Yoneda f r
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 b. (b %1 -> b) %1 -> f b) -> Yoneda f b
forall (f :: * -> *) a.
(forall b. (a %1 -> b) %1 -> f b) -> Yoneda f a
Yoneda (\b %1 -> b
ab_r -> ((a %1 -> b) %1 -> a %1 -> b) %1 -> f (a %1 -> b)
forall b. ((a %1 -> b) %1 -> b) %1 -> f b
k (\a %1 -> b
g -> b %1 -> b
ab_r (b %1 -> b) %1 -> (a %1 -> b) %1 -> a %1 -> b
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) f (a %1 -> b) %1 -> f a %1 -> f b
forall a b. f (a %1 -> b) %1 -> f a %1 -> f b
forall (f :: * -> *) a b.
Applicative f =>
f (a %1 -> b) %1 -> f a %1 -> f b
<*> f a
fa)
{-# INLINE yap #-}