{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Profunctor.List where

import Proarrow.Category.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Category.Monoidal.Strictified qualified as Str
import Proarrow.Core (CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, type (+->))
import Proarrow.Profunctor.Representable (Representable (..))
import Proarrow.Category.Monoidal.Action (Strong (..), MonoidalAction (..))
import Proarrow.Functor (Functor (..))
import Proarrow.Category.Instance.Prof (Prof(..))

type data LIST k = L [k]
type instance UN L (L as) = as

type List :: (j +-> k) -> LIST j +-> LIST k
data List p as bs where
  Nil :: List p (L '[]) (L '[])
  Cons :: (Str.IsList as, Str.IsList bs) => p a b -> List p (L as) (L bs) -> List p (L (a ': as)) (L (b ': bs))

mkCons :: (Profunctor p) => p a b -> List p (L as) (L bs) -> List p (L (a ': as)) (L (b ': bs))
mkCons :: forall {k} {k} (p :: k +-> k) (a :: k) (b :: k) (as :: [k])
       (bs :: [k]).
Profunctor p =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
mkCons p a b
f List p (L as) (L bs)
fs = p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
forall {k} {k} (as :: [k]) (bs :: [k]) (p :: k +-> k) (a :: k)
       (b :: k).
(IsList as, IsList bs) =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
Cons p a b
f List p (L as) (L bs)
fs ((Ob (L as), Ob (L bs)) => List p (L (a : as)) (L (b : bs)))
-> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: LIST k) (b :: LIST k) r.
((Ob a, Ob b) => r) -> List p a b -> r
\\ List p (L as) (L bs)
fs

instance Functor List where
  map :: forall (a :: j +-> k) (b :: j +-> k). (a ~> b) -> List a ~> List b
map (Prof a :~> b
n) = (List a :~> List b) -> Prof (List a) (List b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \case
    List a a b
Nil -> List b a b
List b (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
    Cons a a b
p List a (L as) (L bs)
ps -> b a b -> List b (L as) (L bs) -> List b (L (a : as)) (L (b : bs))
forall {k} {k} (as :: [k]) (bs :: [k]) (p :: k +-> k) (a :: k)
       (b :: k).
(IsList as, IsList bs) =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
Cons (a a b -> b a b
a :~> b
n a a b
p) (Prof (List a) (List b) -> List a :~> List b
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
Prof p q -> p :~> q
unProf ((a ~> b) -> List a ~> List b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: j +-> k) (b :: j +-> k). (a ~> b) -> List a ~> List b
map ((a :~> b) -> Prof a b
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof a a b -> b a b
a :~> b
n)) List a (L as) (L bs)
ps)

-- | The category of lists of arrows.
instance (CategoryOf k) => CategoryOf (LIST k) where
  type (~>) = List (~>)
  type Ob as = (Is L as, Str.IsList (UN L as))

instance (Promonad p) => Promonad (List p) where
  id :: forall (a :: LIST j). Ob a => List p a a
id @(L bs) = case forall (as :: [j]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
Str.sList @bs of
    SList (UN L a)
Str.SNil -> List p a a
List p (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
    SList (UN L a)
Str.SSing -> p a1 a1 -> List p (L '[]) (L '[]) -> List p (L '[a1]) (L '[a1])
forall {k} {k} (as :: [k]) (bs :: [k]) (p :: k +-> k) (a :: k)
       (b :: k).
(IsList as, IsList bs) =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
Cons p a1 a1
forall (a :: j). Ob a => p a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id List p (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
    SList (UN L a)
Str.SCons -> p a1 a1
-> List p (L (b : bs)) (L (b : bs))
-> List p (L (a1 : b : bs)) (L (a1 : b : bs))
forall {k} {k} (as :: [k]) (bs :: [k]) (p :: k +-> k) (a :: k)
       (b :: k).
(IsList as, IsList bs) =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
Cons p a1 a1
forall (a :: j). Ob a => p a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id List p (L (b : bs)) (L (b : bs))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: LIST j). Ob a => List p a a
id
  List p b c
Nil . :: forall (b :: LIST j) (c :: LIST j) (a :: LIST j).
List p b c -> List p a b -> List p a c
. List p a b
Nil = List p a c
List p (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
  Cons p a b
f List p (L as) (L bs)
fs . Cons p a b
g List p (L as) (L bs)
gs = p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
forall {k} {k} (as :: [k]) (bs :: [k]) (p :: k +-> k) (a :: k)
       (b :: k).
(IsList as, IsList bs) =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
Cons (p a b
f p a b -> p a a -> p a b
forall (b :: j) (c :: j) (a :: j). p b c -> p a b -> p a c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a a
p a b
g) (List p (L as) (L bs)
fs List p (L as) (L bs)
-> List p (L as) (L as) -> List p (L as) (L bs)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: LIST j) (c :: LIST j) (a :: LIST j).
List p b c -> List p a b -> List p a c
. List p (L as) (L as)
List p (L as) (L bs)
gs)

instance (Profunctor p) => Profunctor (List p) where
  dimap :: forall (c :: LIST k) (a :: LIST k) (b :: LIST j) (d :: LIST j).
(c ~> a) -> (b ~> d) -> List p a b -> List p c d
dimap c ~> a
List (~>) c a
Nil b ~> d
List (~>) b d
Nil List p a b
Nil = List p c d
List p (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
  dimap (Cons a ~> b
l List (~>) (L as) (L bs)
ls) (Cons a ~> b
r List (~>) (L as) (L bs)
rs) (Cons p a b
f List p (L as) (L bs)
fs) =
    p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
forall {k} {k} (as :: [k]) (bs :: [k]) (p :: k +-> k) (a :: k)
       (b :: k).
(IsList as, IsList bs) =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
Cons ((a ~> a) -> (b ~> b) -> p a b -> p a b
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a ~> b
a ~> a
l a ~> b
b ~> b
r p a b
f) ((L as ~> L as)
-> (L bs ~> L bs) -> List p (L as) (L bs) -> List p (L as) (L bs)
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall (c :: LIST k) (a :: LIST k) (b :: LIST j) (d :: LIST j).
(c ~> a) -> (b ~> d) -> List p a b -> List p c d
dimap L as ~> L as
List (~>) (L as) (L bs)
ls L bs ~> L bs
List (~>) (L as) (L bs)
rs List p (L as) (L bs)
fs)
  dimap c ~> a
List (~>) c a
Nil Cons{} List p a b
fs = case List p a b
fs of {}
  dimap Cons{} b ~> d
List (~>) b d
Nil List p a b
fs = case List p a b
fs of {}
  (Ob a, Ob b) => r
r \\ :: forall (a :: LIST k) (b :: LIST j) r.
((Ob a, Ob b) => r) -> List p a b -> r
\\ List p a b
Nil = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ Cons p a b
f List p (L as) (L bs)
Nil = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
f
  (Ob a, Ob b) => r
r \\ Cons p a b
f fs :: List p (L as) (L bs)
fs@Cons{} = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
f ((Ob (L as), Ob (L bs)) => r) -> List p (L as) (L bs) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: LIST k) (b :: LIST j) r.
((Ob a, Ob b) => r) -> List p a b -> r
\\ List p (L as) (L bs)
fs

-- | The free monoidal profunctor on a profunctor.
instance (Profunctor p) => MonoidalProfunctor (List p) where
  par0 :: List p Unit Unit
par0 = List p Unit Unit
List p (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
  List p x1 x2
Nil par :: forall (x1 :: LIST k) (x2 :: LIST j) (y1 :: LIST k) (y2 :: LIST j).
List p x1 x2 -> List p y1 y2 -> List p (x1 ** y1) (x2 ** y2)
`par` List p y1 y2
Nil = List p (x1 ** y1) (x2 ** y2)
List p (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
  List p x1 x2
Nil `par` gs :: List p y1 y2
gs@Cons{} = List p y1 y2
List p (x1 ** y1) (x2 ** y2)
gs
  Cons p a b
f List p (L as) (L bs)
fs `par` List p y1 y2
Nil = p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
forall {k} {k} (p :: k +-> k) (a :: k) (b :: k) (as :: [k])
       (bs :: [k]).
Profunctor p =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
mkCons p a b
f (List p (L as) (L bs)
fs List p (L as) (L bs)
-> List p (L '[]) (L '[]) -> List p (L as ** L '[]) (L bs ** L '[])
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: LIST k) (x2 :: LIST j) (y1 :: LIST k) (y2 :: LIST j).
List p x1 x2 -> List p y1 y2 -> List p (x1 ** y1) (x2 ** y2)
`par` List p (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil)
  Cons p a b
f List p (L as) (L bs)
fs `par` Cons p a b
g List p (L as) (L bs)
gs = p a b
-> List p (L (as ++ (a : as))) (L (bs ++ (b : bs)))
-> List p (L (a : (as ++ (a : as)))) (L (b : (bs ++ (b : bs))))
forall {k} {k} (p :: k +-> k) (a :: k) (b :: k) (as :: [k])
       (bs :: [k]).
Profunctor p =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
mkCons p a b
f (List p (L as) (L bs)
fs List p (L as) (L bs)
-> List p (L (a : as)) (L (b : bs))
-> List p (L as ** L (a : as)) (L bs ** L (b : bs))
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: LIST k) (x2 :: LIST j) (y1 :: LIST k) (y2 :: LIST j).
List p x1 x2 -> List p y1 y2 -> List p (x1 ** y1) (x2 ** y2)
`par` p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
forall {k} {k} (as :: [k]) (bs :: [k]) (p :: k +-> k) (a :: k)
       (b :: k).
(IsList as, IsList bs) =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
Cons p a b
g List p (L as) (L bs)
gs)

-- | The free monoidal category on a category.
instance (CategoryOf k) => Monoidal (LIST k) where
  type Unit = L '[]
  type p ** q = L (UN L p Str.++ UN L q)
  withOb2 :: forall (a :: LIST k) (b :: LIST k) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @(L as) @(L bs) = forall (as :: [k]) (bs :: [k]) r.
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
forall {k} (as :: [k]) (bs :: [k]) r.
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
Str.withIsList2 @as @bs
  leftUnitor :: forall (a :: LIST k). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
List (~>) (L (UN L a)) (L (UN L a))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: LIST k). Ob a => List (~>) a a
id
  leftUnitorInv :: forall (a :: LIST k). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
List (~>) (L (UN L a)) (L (UN L a))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: LIST k). Ob a => List (~>) a a
id
  rightUnitor :: forall (a :: LIST k). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
List (~>) (L (UN L a)) (L (UN L a))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: LIST k). Ob a => List (~>) a a
id
  rightUnitorInv :: forall (a :: LIST k). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
List (~>) (L (UN L a)) (L (UN L a))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: LIST k). Ob a => List (~>) a a
id
  associator :: forall (a :: LIST k) (b :: LIST k) (c :: LIST k).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @as @bs @cs = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @as @bs (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(as ** bs) @cs (forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (p :: LIST k +-> LIST k) (a :: LIST k).
(Promonad p, Ob a) =>
p a a
id @(List (~>))))
  associatorInv :: forall (a :: LIST k) (b :: LIST k) (c :: LIST k).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @as @bs @cs = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @bs @cs (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @as @(bs ** cs) (forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (p :: LIST k +-> LIST k) (a :: LIST k).
(Promonad p, Ob a) =>
p a a
id @(List (~>))))

instance (Representable p) => Representable (List p) where
  type List p % L '[] = L '[]
  type List p % L (a ': as) = L ((p % a) ': UN L (List p % L as))
  index :: forall (a :: LIST k) (b :: LIST j). List p a b -> a ~> (List p % b)
index List p a b
Nil = a ~> (List p % b)
List (~>) (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
  index (Cons p a b
p List p (L as) (L bs)
Nil) = (a ~> (p % b))
-> List (~>) (L '[]) (L '[]) -> List (~>) (L '[a]) (L '[p % b])
forall {k} {k} (as :: [k]) (bs :: [k]) (p :: k +-> k) (a :: k)
       (b :: k).
(IsList as, IsList bs) =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
Cons (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index @p p a b
p) List (~>) (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
  index (Cons p a b
p ps :: List p (L as) (L bs)
ps@Cons{}) = (a ~> (p % b))
-> List (~>) (L (a : as)) (L ((p % b) : UN L (List p % L bs)))
-> List
     (~>)
     (L (a : a : as))
     (L ((p % b) : (p % b) : UN L (List p % L bs)))
forall {k} {k} (p :: k +-> k) (a :: k) (b :: k) (as :: [k])
       (bs :: [k]).
Profunctor p =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
mkCons (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index @p p a b
p) (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: LIST j +-> LIST k) (a :: LIST k) (b :: LIST j).
Representable p =>
p a b -> a ~> (p % b)
index @(List p) List p (L as) (L bs)
ps)
  tabulate :: forall (b :: LIST j) (a :: LIST k).
Ob b =>
(a ~> (List p % b)) -> List p a b
tabulate @(L b) a ~> (List p % b)
List (~>) a (List p % L (UN L b))
Nil = case forall (as :: [j]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
Str.sList @b of SList (UN L b)
Str.SNil -> List p a b
List p (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
  tabulate @(L b) (Cons a ~> b
f List (~>) (L as) (L bs)
Nil) = case forall (as :: [j]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
Str.sList @b of SList (UN L b)
Str.SSing -> p a a1 -> List p (L '[]) (L '[]) -> List p (L '[a]) (L '[a1])
forall {k} {k} (as :: [k]) (bs :: [k]) (p :: k +-> k) (a :: k)
       (b :: k).
(IsList as, IsList bs) =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
Cons (forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @p a ~> b
a ~> (p % a1)
f) List p (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
  tabulate @(L b) (Cons a ~> b
f fs :: List (~>) (L as) (L bs)
fs@Cons{}) = case forall (as :: [j]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
Str.sList @b of SList (UN L b)
Str.SCons -> p a a1
-> List p (L (a : as)) (L (b : bs))
-> List p (L (a : a : as)) (L (a1 : b : bs))
forall {k} {k} (as :: [k]) (bs :: [k]) (p :: k +-> k) (a :: k)
       (b :: k).
(IsList as, IsList bs) =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
Cons (forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @p a ~> b
a ~> (p % a1)
f) (forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: LIST j +-> LIST k) (b :: LIST j) (a :: LIST k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @(List p) L (a : as) ~> (List p % L (b : bs))
List (~>) (L as) (L bs)
fs)
  repMap :: forall (a :: LIST j) (b :: LIST j).
(a ~> b) -> (List p % a) ~> (List p % b)
repMap a ~> b
List (~>) a b
Nil = (List p % a) ~> (List p % b)
List (~>) (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
  repMap (Cons a ~> b
f List (~>) (L as) (L bs)
Nil) = ((p % a) ~> (p % b))
-> List (~>) (L '[]) (L '[]) -> List (~>) (L '[p % a]) (L '[p % b])
forall {k} {k} (as :: [k]) (bs :: [k]) (p :: k +-> k) (a :: k)
       (b :: k).
(IsList as, IsList bs) =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
Cons (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p a ~> b
f) List (~>) (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
  repMap (Cons a ~> b
f fs :: List (~>) (L as) (L bs)
fs@Cons{}) = ((p % a) ~> (p % b))
-> List
     (~>)
     (L ((p % a) : UN L (List p % L as)))
     (L ((p % b) : UN L (List p % L bs)))
-> List
     (~>)
     (L ((p % a) : (p % a) : UN L (List p % L as)))
     (L ((p % b) : (p % b) : UN L (List p % L bs)))
forall {k} {k} (p :: k +-> k) (a :: k) (b :: k) (as :: [k])
       (bs :: [k]).
Profunctor p =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
mkCons (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p a ~> b
f) (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: LIST j +-> LIST k) (a :: LIST j) (b :: LIST j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @(List p) L (a : as) ~> L (b : bs)
List (~>) (L as) (L bs)
fs)

instance (DaggerProfunctor p) => DaggerProfunctor (List p) where
  dagger :: forall (a :: LIST j) (b :: LIST j). List p a b -> List p b a
dagger List p a b
Nil = List p b a
List p (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
  dagger (Cons p a b
f List p (L as) (L bs)
fs) = p b a -> List p (L bs) (L as) -> List p (L (b : bs)) (L (a : as))
forall {k} {k} (as :: [k]) (bs :: [k]) (p :: k +-> k) (a :: k)
       (b :: k).
(IsList as, IsList bs) =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
Cons (p a b -> p b a
forall (a :: j) (b :: j). p a b -> p b a
forall {k} (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
dagger p a b
f) (List p (L as) (L bs) -> List p (L bs) (L as)
forall {k} (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
forall (a :: LIST j) (b :: LIST j). List p a b -> List p b a
dagger List p (L as) (L bs)
fs)

instance MonoidalAction m k => MonoidalAction m (LIST k) where
  type Act (a :: m) (L '[] :: LIST k) = L '[]
  type Act (a :: m) (L (b ': bs) :: LIST k) = L (Act a b ': UN L (Act a (L bs)))
  withObAct :: forall (a :: m) (x :: LIST k) r.
(Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @a @(L xs) Ob (Act a x) => r
r = case forall (as :: [k]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
Str.sList @xs of
    SList (UN L x)
Str.SNil -> r
Ob (Act a x) => r
r
    Str.SSing @x -> forall m k (a :: m) (x :: k) r.
(MonoidalAction m k, Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @m @k @a @x r
Ob (Act a a1) => r
Ob (Act a x) => r
r
    Str.SCons @x @(y ': ys) -> forall m k (a :: m) (x :: k) r.
(MonoidalAction m k, Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @m @(LIST k) @a @(L ys) (forall m k (a :: m) (x :: k) r.
(MonoidalAction m k, Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @m @(LIST k) @a @(L (y ': ys)) (forall m k (a :: m) (x :: k) r.
(MonoidalAction m k, Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @m @k @a @x r
Ob (Act a a1) => r
Ob (Act a x) => r
r))
  unitor :: forall (x :: LIST k). Ob x => Act Unit x ~> x
unitor @(L xs) = case forall (as :: [k]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
Str.sList @xs of
    SList (UN L x)
Str.SNil -> Act Unit x ~> x
List (~>) (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
    Str.SSing @x -> (Act Unit a1 ~> a1)
-> List (~>) (L '[]) (L '[])
-> List (~>) (L '[Act Unit a1]) (L '[a1])
forall {k} {k} (as :: [k]) (bs :: [k]) (p :: k +-> k) (a :: k)
       (b :: k).
(IsList as, IsList bs) =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
Cons (forall m k (x :: k). (MonoidalAction m k, Ob x) => Act Unit x ~> x
unitor @m @k @x) List (~>) (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
    Str.SCons @x @xs' -> (Act Unit a1 ~> a1)
-> List (~>) (L (Act Unit b : UN L (Act Unit (L bs)))) (L (b : bs))
-> List
     (~>)
     (L (Act Unit a1 : Act Unit b : UN L (Act Unit (L bs))))
     (L (a1 : b : bs))
forall {k} {k} (p :: k +-> k) (a :: k) (b :: k) (as :: [k])
       (bs :: [k]).
Profunctor p =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
mkCons (forall m k (x :: k). (MonoidalAction m k, Ob x) => Act Unit x ~> x
unitor @m @k @x) (forall m k (x :: k). (MonoidalAction m k, Ob x) => Act Unit x ~> x
unitor @m @(LIST k) @(L xs'))
  unitorInv :: forall (x :: LIST k). Ob x => x ~> Act Unit x
unitorInv @(L xs) = case forall (as :: [k]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
Str.sList @xs of
    SList (UN L x)
Str.SNil -> x ~> Act Unit x
List (~>) (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
    Str.SSing @x -> (a1 ~> Act Unit a1)
-> List (~>) (L '[]) (L '[])
-> List (~>) (L '[a1]) (L '[Act Unit a1])
forall {k} {k} (as :: [k]) (bs :: [k]) (p :: k +-> k) (a :: k)
       (b :: k).
(IsList as, IsList bs) =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
Cons (forall m k (x :: k). (MonoidalAction m k, Ob x) => x ~> Act Unit x
unitorInv @m @k @x) List (~>) (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
    Str.SCons @x @xs' -> (a1 ~> Act Unit a1)
-> List (~>) (L (b : bs)) (L (Act Unit b : UN L (Act Unit (L bs))))
-> List
     (~>)
     (L (a1 : b : bs))
     (L (Act Unit a1 : Act Unit b : UN L (Act Unit (L bs))))
forall {k} {k} (p :: k +-> k) (a :: k) (b :: k) (as :: [k])
       (bs :: [k]).
Profunctor p =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
mkCons (forall m k (x :: k). (MonoidalAction m k, Ob x) => x ~> Act Unit x
unitorInv @m @k @x) (forall m k (x :: k). (MonoidalAction m k, Ob x) => x ~> Act Unit x
unitorInv @m @(LIST k) @(L xs'))
  multiplicator :: forall (a :: m) (b :: m) (x :: LIST k).
(Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator @a @b @(L xs) = case forall (as :: [k]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
Str.sList @xs of
    SList (UN L x)
Str.SNil -> Act a (Act b x) ~> Act (a ** b) x
List (~>) (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
    Str.SSing @x -> (Act a (Act b a1) ~> Act (a ** b) a1)
-> List (~>) (L '[]) (L '[])
-> List (~>) (L '[Act a (Act b a1)]) (L '[Act (a ** b) a1])
forall {k} {k} (as :: [k]) (bs :: [k]) (p :: k +-> k) (a :: k)
       (b :: k).
(IsList as, IsList bs) =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
Cons (forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator @m @k @a @b @x) List (~>) (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
    Str.SCons @x @xs' -> (Act a (Act b a1) ~> Act (a ** b) a1)
-> List
     (~>)
     (L (Act a (Act b b) : UN L (Act a (L (UN L (Act b (L bs)))))))
     (L (Act (a ** b) b : UN L (Act (a ** b) (L bs))))
-> List
     (~>)
     (L (Act a (Act b a1)
           : Act a (Act b b) : UN L (Act a (L (UN L (Act b (L bs)))))))
     (L (Act (a ** b) a1 : Act (a ** b) b : UN L (Act (a ** b) (L bs))))
forall {k} {k} (p :: k +-> k) (a :: k) (b :: k) (as :: [k])
       (bs :: [k]).
Profunctor p =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
mkCons (forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator @m @k @a @b @x) (forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator @m @(LIST k) @a @b @(L xs'))
  multiplicatorInv :: forall (a :: m) (b :: m) (x :: LIST k).
(Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv @a @b @(L xs) = case forall (as :: [k]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
Str.sList @xs of
    SList (UN L x)
Str.SNil -> Act (a ** b) x ~> Act a (Act b x)
List (~>) (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
    Str.SSing @x -> (Act (a ** b) a1 ~> Act a (Act b a1))
-> List (~>) (L '[]) (L '[])
-> List (~>) (L '[Act (a ** b) a1]) (L '[Act a (Act b a1)])
forall {k} {k} (as :: [k]) (bs :: [k]) (p :: k +-> k) (a :: k)
       (b :: k).
(IsList as, IsList bs) =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
Cons (forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv @m @k @a @b @x) List (~>) (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
    Str.SCons @x @xs' -> (Act (a ** b) a1 ~> Act a (Act b a1))
-> List
     (~>)
     (L (Act (a ** b) b : UN L (Act (a ** b) (L bs))))
     (L (Act a (Act b b) : UN L (Act a (L (UN L (Act b (L bs)))))))
-> List
     (~>)
     (L (Act (a ** b) a1 : Act (a ** b) b : UN L (Act (a ** b) (L bs))))
     (L (Act a (Act b a1)
           : Act a (Act b b) : UN L (Act a (L (UN L (Act b (L bs)))))))
forall {k} {k} (p :: k +-> k) (a :: k) (b :: k) (as :: [k])
       (bs :: [k]).
Profunctor p =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
mkCons (forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv @m @k @a @b @x) (forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv @m @(LIST k) @a @b @(L xs'))

instance (Strong m p) => Strong m (List p) where
  act :: forall (a :: m) (b :: m) (x :: LIST k) (y :: LIST j).
(a ~> b) -> List p x y -> List p (Act a x) (Act b y)
act a ~> b
_ List p x y
Nil = List p (Act a x) (Act b y)
List p (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
  act a ~> b
f (Cons p a b
g List p (L as) (L bs)
Nil) = p (Act a a) (Act b b)
-> List p (L '[]) (L '[]) -> List p (L '[Act a a]) (L '[Act b b])
forall {k} {k} (as :: [k]) (bs :: [k]) (p :: k +-> k) (a :: k)
       (b :: k).
(IsList as, IsList bs) =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
Cons ((a ~> b) -> p a b -> p (Act a a) (Act b b)
forall (a :: m) (b :: m) (x :: k) (y :: j).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act a ~> b
f p a b
g) List p (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
  act a ~> b
f (Cons p a b
g gs :: List p (L as) (L bs)
gs@Cons{}) = p (Act a a) (Act b b)
-> List
     p
     (L (Act a a : UN L (Act a (L as))))
     (L (Act b b : UN L (Act b (L bs))))
-> List
     p
     (L (Act a a : Act a a : UN L (Act a (L as))))
     (L (Act b b : Act b b : UN L (Act b (L bs))))
forall {k} {k} (p :: k +-> k) (a :: k) (b :: k) (as :: [k])
       (bs :: [k]).
Profunctor p =>
p a b -> List p (L as) (L bs) -> List p (L (a : as)) (L (b : bs))
mkCons ((a ~> b) -> p a b -> p (Act a a) (Act b b)
forall (a :: m) (b :: m) (x :: k) (y :: j).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act a ~> b
f p a b
g) ((a ~> b)
-> List p (L as) (L bs) -> List p (Act a (L as)) (Act b (L bs))
forall (a :: m) (b :: m) (x :: LIST k) (y :: LIST j).
(a ~> b) -> List p x y -> List p (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act a ~> b
f List p (L as) (L bs)
gs)