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

module Proarrow.Category.Promonoidal where

import Data.Kind (Constraint)
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Category.Monoidal.Strictified qualified as Str
import Proarrow.Core
  ( CategoryOf (..)
  , Obj
  , Profunctor (..)
  , Promonad (..)
  , UN
  , lmap
  , obj
  , tgt
  , (//)
  , (:~>)
  , type (+->)
  )
import Proarrow.Functor (Functor (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.List (LIST (..), List (..), foldList)
import Proarrow.Profunctor.Representable (Representable (..), dimapRep)

type PROTENSOR k = LIST k +-> k
type Protensor :: forall {k}. PROTENSOR k -> Constraint
class (Profunctor p) => Protensor p where
  compose :: (p :.: List p) a bss -> p a (Tensor % bss)
  decompose :: (Ob bss) => p a (Tensor % bss) -> (p :.: List p) a bss

class (Protensor p) => Promonoid p m where
  mempty :: p m (L '[])
  mappend :: p m (L '[m, m])

class (Protensor t, Profunctor p) => PromonoidalProfunctor t p where
  parN :: t :.: List p :~> p :.: t

type Tensor :: PROTENSOR k
data Tensor a bs where
  Tensor :: (Ob bs) => {forall {k} (bs :: LIST k) (a :: k). Tensor a bs -> '[a] ~> UN L bs
unTensor :: '[a] ~> UN L bs} -> Tensor a bs
instance (Monoidal k) => Profunctor (Tensor :: PROTENSOR k) where
  dimap :: forall (c :: k) (a :: k) (b :: LIST k) (d :: LIST k).
(c ~> a) -> (b ~> d) -> Tensor a b -> Tensor c d
dimap = (c ~> a) -> (b ~> d) -> Tensor a b -> Tensor c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: LIST k) r.
((Ob a, Ob b) => r) -> Tensor a b -> r
\\ Tensor (Str.Str Fold '[a] ~> Fold (UN L b)
f) = r
(Ob a, Ob (Fold (UN L b))) => r
(Ob a, Ob b) => r
r ((Ob a, Ob (Fold (UN L b))) => r) -> (a ~> Fold (UN L b)) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ a ~> Fold (UN L b)
Fold '[a] ~> Fold (UN L b)
f
instance (Monoidal k) => Representable (Tensor :: PROTENSOR k) where
  type Tensor % as = Str.Fold (UN L as)
  index :: forall (a :: k) (b :: LIST k). Tensor a b -> a ~> (Tensor % b)
index (Tensor (Str.Str Fold '[a] ~> Fold (UN L b)
f)) = a ~> (Tensor % b)
Fold '[a] ~> Fold (UN L b)
f
  tabulate :: forall (b :: LIST k) (a :: k).
Ob b =>
(a ~> (Tensor % b)) -> Tensor a b
tabulate a ~> (Tensor % b)
f = ('[a] ~> UN L b) -> Tensor a b
forall {k} (bs :: LIST k) (a :: k).
Ob bs =>
('[a] ~> UN L bs) -> Tensor a bs
Tensor ((Fold '[a] ~> Fold (UN L b)) -> Strictified '[a] (UN L b)
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str.Str a ~> (Tensor % b)
Fold '[a] ~> Fold (UN L b)
f) ((Ob a, Ob (Fold (UN L b))) => Tensor a b)
-> (a ~> Fold (UN L b)) -> Tensor a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ a ~> Fold (UN L b)
a ~> (Tensor % b)
f
  repMap :: forall (a :: LIST k) (b :: LIST k).
(a ~> b) -> (Tensor % a) ~> (Tensor % b)
repMap = (a ~> b) -> (Tensor % a) ~> (Tensor % b)
List (~>) a b -> Fold (UN L a) ~> Fold (UN L b)
forall {k1} {k2} (p :: k1 +-> k2) (as :: LIST k2) (bs :: LIST k1).
MonoidalProfunctor p =>
List p as bs -> p (Fold (UN L as)) (Fold (UN L bs))
foldList
instance (Monoidal k) => MonoidalProfunctor (Tensor :: PROTENSOR k) where
  par0 :: Tensor Unit Unit
par0 = ('[Unit] ~> UN L (L '[])) -> Tensor Unit (L '[])
forall {k} (bs :: LIST k) (a :: k).
Ob bs =>
('[a] ~> UN L bs) -> Tensor a bs
Tensor ((Fold '[Unit] ~> Fold '[]) -> Strictified '[Unit] '[]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str.Str Unit ~> Unit
Fold '[Unit] ~> Fold '[]
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)
  Tensor '[x1] ~> UN L x2
f par :: forall (x1 :: k) (x2 :: LIST k) (y1 :: k) (y2 :: LIST k).
Tensor x1 x2 -> Tensor y1 y2 -> Tensor (x1 ** y1) (x2 ** y2)
`par` Tensor '[y1] ~> UN L y2
g = let fg :: Strictified ('[x1] ** '[y1]) (UN L x2 ** UN L y2)
fg = '[x1] ~> UN L x2
Strictified '[x1] (UN L x2)
f Strictified '[x1] (UN L x2)
-> Strictified '[y1] (UN L y2)
-> Strictified ('[x1] ** '[y1]) (UN L x2 ** UN L y2)
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
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)
`par` '[y1] ~> UN L y2
Strictified '[y1] (UN L y2)
g in Strictified '[x1, y1] (UN L x2 ++ UN L y2)
Strictified ('[x1] ** '[y1]) (UN L x2 ** UN L y2)
fg Strictified '[x1, y1] (UN L x2 ++ UN L y2)
-> ((Ob '[x1, y1], Ob (UN L x2 ++ UN L y2)) =>
    Tensor (x1 ** y1) (L (UN L x2 ++ UN L y2)))
-> Tensor (x1 ** y1) (L (UN L x2 ++ UN L y2))
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// Strictified '[x1, y1] (UN L x2 ++ UN L y2)
-> Fold '[x1, y1] ~> Fold (UN L x2 ++ UN L y2)
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
Str.unStr Strictified '[x1, y1] (UN L x2 ++ UN L y2)
Strictified ('[x1] ** '[y1]) (UN L x2 ** UN L y2)
fg (Fold '[x1, y1] ~> Fold (UN L x2 ++ UN L y2))
-> ((Ob (Fold '[x1, y1]), Ob (Fold (UN L x2 ++ UN L y2))) =>
    Tensor (x1 ** y1) (L (UN L x2 ++ UN L y2)))
-> Tensor (x1 ** y1) (L (UN L x2 ++ UN L y2))
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// ('[x1 ** y1] ~> UN L (L (UN L x2 ++ UN L y2)))
-> Tensor (x1 ** y1) (L (UN L x2 ++ UN L y2))
forall {k} (bs :: LIST k) (a :: k).
Ob bs =>
('[a] ~> UN L bs) -> Tensor a bs
Tensor ((Fold '[x1 ** y1] ~> Fold (UN L x2 ++ UN L y2))
-> Strictified '[x1 ** y1] (UN L x2 ++ UN L y2)
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str.Str (Strictified '[x1, y1] (UN L x2 ++ UN L y2)
-> Fold '[x1, y1] ~> Fold (UN L x2 ++ UN L y2)
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
Str.unStr Strictified '[x1, y1] (UN L x2 ++ UN L y2)
Strictified ('[x1] ** '[y1]) (UN L x2 ** UN L y2)
fg))
instance (Monoidal k) => Protensor (Tensor :: PROTENSOR k) where
  compose :: forall (a :: k) (bss :: LIST (LIST k)).
(:.:) Tensor (List Tensor) a bss -> Tensor a (Tensor % bss)
compose (Tensor (Str.Str Fold '[a] ~> Fold (UN L b)
f) :.: List Tensor b bss
l) = (a ~> Fold (UN L b))
-> Tensor (Fold (UN L b)) (Fold (UN L bss))
-> Tensor a (Fold (UN L bss))
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> Fold (UN L b)
Fold '[a] ~> Fold (UN L b)
f (List Tensor b bss -> Tensor (Fold (UN L b)) (Fold (UN L bss))
forall {k1} {k2} (p :: k1 +-> k2) (as :: LIST k2) (bs :: LIST k1).
MonoidalProfunctor p =>
List p as bs -> p (Fold (UN L as)) (Fold (UN L bs))
foldList List Tensor b bss
l)
  decompose :: forall (bss :: LIST (LIST k)) (a :: k).
Ob bss =>
Tensor a (Tensor % bss) -> (:.:) Tensor (List Tensor) a bss
decompose @bss (Tensor (Str.Str Fold '[a] ~> Fold (UN L (Fold (UN L bss)))
f)) = (a ~> Fold (UN L (Fold (UN L bss))))
-> (:.:) Tensor (List Tensor) (Fold (UN L (Fold (UN L bss)))) bss
-> (:.:) Tensor (List Tensor) a bss
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> Fold (UN L (Fold (UN L bss)))
Fold '[a] ~> Fold (UN L (Fold (UN L bss)))
f (Obj bss -> (:.:) Tensor (List Tensor) (Tensor % (Tensor % bss)) bss
forall (ass :: LIST (LIST k)).
Monoidal k =>
Obj ass -> (:.:) Tensor (List Tensor) (Tensor % (Tensor % ass)) ass
go (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: LIST (LIST k)).
(CategoryOf (LIST (LIST k)), Ob a) =>
Obj a
obj @bss))
    where
      -- 🤮
      go :: (Monoidal k) => Obj (ass :: LIST (LIST k)) -> (Tensor :.: List Tensor) (Tensor % (Tensor % ass)) ass
      go :: forall (ass :: LIST (LIST k)).
Monoidal k =>
Obj ass -> (:.:) Tensor (List Tensor) (Tensor % (Tensor % ass)) ass
go Obj ass
List (List (~>)) ass ass
Nil = ('[Unit] ~> UN L (L '[])) -> Tensor Unit (L '[])
forall {k} (bs :: LIST k) (a :: k).
Ob bs =>
('[a] ~> UN L bs) -> Tensor a bs
Tensor ((Fold '[Unit] ~> Fold '[]) -> Strictified '[Unit] '[]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str.Str Unit ~> Unit
Fold '[Unit] ~> Fold '[]
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id) Tensor Unit (L '[])
-> List Tensor (L '[]) ass -> (:.:) Tensor (List Tensor) Unit ass
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: List Tensor (L '[]) ass
List Tensor (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
      go (Cons List (~>) a b
as List (List (~>)) (L as1) (L bs1)
Nil) = let fas :: Fold (UN L b) ~> Fold (UN L b)
fas = List (~>) b b -> Fold (UN L b) ~> Fold (UN L b)
forall {k1} {k2} (p :: k1 +-> k2) (as :: LIST k2) (bs :: LIST k1).
MonoidalProfunctor p =>
List p as bs -> p (Fold (UN L as)) (Fold (UN L bs))
foldList List (~>) a b
List (~>) b b
as in List (~>) a b
as List (~>) a b
-> ((Ob a, Ob b) =>
    (:.:) Tensor (List Tensor) (Fold (UN L b)) (L '[b]))
-> (:.:) Tensor (List Tensor) (Fold (UN L b)) (L '[b])
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// Fold (UN L b) ~> Fold (UN L b)
fas (Fold (UN L b) ~> Fold (UN L b))
-> ((Ob (Fold (UN L b)), Ob (Fold (UN L b))) =>
    (:.:) Tensor (List Tensor) (Fold (UN L b)) (L '[b]))
-> (:.:) Tensor (List Tensor) (Fold (UN L b)) (L '[b])
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// ('[Fold (UN L b)] ~> UN L (L '[Fold (UN L b)]))
-> Tensor (Fold (UN L b)) (L '[Fold (UN L b)])
forall {k} (bs :: LIST k) (a :: k).
Ob bs =>
('[a] ~> UN L bs) -> Tensor a bs
Tensor ((Fold '[Fold (UN L b)] ~> Fold '[Fold (UN L b)])
-> Strictified '[Fold (UN L b)] '[Fold (UN L b)]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str.Str Fold '[Fold (UN L b)] ~> Fold '[Fold (UN L b)]
Fold (UN L b) ~> Fold (UN L b)
fas) Tensor (Fold (UN L b)) (L '[Fold (UN L b)])
-> List Tensor (L '[Fold (UN L b)]) (L '[b])
-> (:.:) Tensor (List Tensor) (Fold (UN L b)) (L '[b])
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: Tensor (Fold (UN L b)) b
-> List Tensor (L '[]) (L '[])
-> List Tensor (L '[Fold (UN L b)]) (L '[b])
forall {k} {j} (as1 :: [k]) (bs1 :: [j]) (p :: j +-> k) (a :: k)
       (b :: j).
(IsList as1, IsList bs1) =>
p a b
-> List p (L as1) (L bs1) -> List p (L (a : as1)) (L (b : bs1))
Cons (('[Fold (UN L b)] ~> UN L b) -> Tensor (Fold (UN L b)) b
forall {k} (bs :: LIST k) (a :: k).
Ob bs =>
('[a] ~> UN L bs) -> Tensor a bs
Tensor ((Fold '[Fold (UN L b)] ~> Fold (UN L b))
-> Strictified '[Fold (UN L b)] (UN L b)
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str.Str Fold '[Fold (UN L b)] ~> Fold (UN L b)
Fold (UN L b) ~> Fold (UN L b)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)) List Tensor (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
      go (Cons @ass' @_ @_ @as List (~>) a b
as ass :: List (List (~>)) (L as1) (L bs1)
ass@Cons{}) = case Obj (L (b : bs1))
-> (:.:)
     Tensor
     (List Tensor)
     (Tensor % (Tensor % L (b : bs1)))
     (L (b : bs1))
forall (ass :: LIST (LIST k)).
Monoidal k =>
Obj ass -> (:.:) Tensor (List Tensor) (Tensor % (Tensor % ass)) ass
go Obj (L (b : bs1))
List (List (~>)) (L as1) (L bs1)
ass of
        Tensor @bs '[Tensor % (Tensor % L (b : bs1))] ~> UN L b
g :.: List Tensor b (L (b : bs1))
l ->
          List (~>) a b
as List (~>) a b
-> ((Ob a, Ob b) =>
    (:.:)
      Tensor
      (List Tensor)
      (Fold (UN L b ++ UN L (Fold (b : bs1))))
      (L (b : b : bs1)))
-> (:.:)
     Tensor
     (List Tensor)
     (Fold (UN L b ++ UN L (Fold (b : bs1))))
     (L (b : b : bs1))
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
            let fas :: Fold (UN L (L (UN L b))) ~> Fold (UN L (L (UN L b)))
fas = List (~>) (L (UN L b)) (L (UN L b))
-> Fold (UN L (L (UN L b))) ~> Fold (UN L (L (UN L b)))
forall {k1} {k2} (p :: k1 +-> k2) (as :: LIST k2) (bs :: LIST k1).
MonoidalProfunctor p =>
List p as bs -> p (Fold (UN L as)) (Fold (UN L bs))
foldList List (~>) a b
List (~>) (L (UN L b)) (L (UN L b))
as; fass :: List (~>) (Fold (UN L (L as1))) (Fold (UN L (L bs1)))
fass = List (List (~>)) (L as1) (L bs1)
-> List (~>) (Fold (UN L (L as1))) (Fold (UN L (L bs1)))
forall {k1} {k2} (p :: k1 +-> k2) (as :: LIST k2) (bs :: LIST k1).
MonoidalProfunctor p =>
List p as bs -> p (Fold (UN L as)) (Fold (UN L bs))
foldList List (List (~>)) (L as1) (L bs1)
ass
            in Fold (UN L b) ~> Fold (UN L b)
Fold (UN L (L (UN L b))) ~> Fold (UN L (L (UN L b)))
fas (Fold (UN L b) ~> Fold (UN L b))
-> ((Ob (Fold (UN L b)), Ob (Fold (UN L b))) =>
    (:.:)
      Tensor
      (List Tensor)
      (Fold (UN L b ++ UN L (Fold (b : bs1))))
      (L (b : b : bs1)))
-> (:.:)
     Tensor
     (List Tensor)
     (Fold (UN L b ++ UN L (Fold (b : bs1))))
     (L (b : b : bs1))
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
                 List (~>) (Fold (b : bs1)) (Fold (b : bs1))
List (~>) (Fold (UN L (L as1))) (Fold (UN L (L bs1)))
fass List (~>) (Fold (b : bs1)) (Fold (b : bs1))
-> ((Ob (Fold (b : bs1)), Ob (Fold (b : bs1))) =>
    (:.:)
      Tensor
      (List Tensor)
      (Fold (UN L b ++ UN L (Fold (b : bs1))))
      (L (b : b : bs1)))
-> (:.:)
     Tensor
     (List Tensor)
     (Fold (UN L b ++ UN L (Fold (b : bs1))))
     (L (b : b : bs1))
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
                   let fasg :: Strictified
  (UN L b ** UN L (Fold (b : bs1))) ('[Fold (UN L b)] ** UN L b)
fasg = forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str.Str @(UN L as) @'[Str.Fold (UN L as)] Fold (UN L a) ~> Fold '[Fold (UN L a)]
Fold (UN L (L (UN L b))) ~> Fold (UN L (L (UN L b)))
fas Strictified (UN L b) '[Fold (UN L b)]
-> Strictified (UN L (Fold (b : bs1))) (UN L b)
-> Strictified
     (UN L b ** UN L (Fold (b : bs1))) ('[Fold (UN L b)] ** UN L b)
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
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)
`par` forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str.Str @(UN L (Str.Fold ass')) @(UN L bs) (Strictified '[Fold (UN L (Fold (b : bs1)))] (UN L b)
-> Fold '[Fold (UN L (Fold (b : bs1)))] ~> Fold (UN L b)
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
Str.unStr '[Tensor % (Tensor % L (b : bs1))] ~> UN L b
Strictified '[Fold (UN L (Fold (b : bs1)))] (UN L b)
g)
                   in List
  (~>)
  (L (UN L b ++ UN L (L (UN L (Fold (b : bs1))))))
  (L (UN L (L (UN L b)) ++ UN L (L (UN L (Fold (b : bs1))))))
-> Fold (UN L (L (UN L b ++ UN L (L (UN L (Fold (b : bs1)))))))
   ~> Fold
        (UN L (L (UN L (L (UN L b)) ++ UN L (L (UN L (Fold (b : bs1)))))))
forall {k1} {k2} (p :: k1 +-> k2) (as :: LIST k2) (bs :: LIST k1).
MonoidalProfunctor p =>
List p as bs -> p (Fold (UN L as)) (Fold (UN L bs))
foldList (List (~>) a b
List (~>) a (L (UN L b))
as List (~>) a (L (UN L b))
-> List
     (~>) (L (UN L (Fold (b : bs1)))) (L (UN L (Fold (b : bs1))))
-> List
     (~>)
     (a ** L (UN L (Fold (b : bs1))))
     (L (UN L b) ** L (UN L (Fold (b : bs1))))
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 k) (y1 :: LIST k) (y2 :: LIST k).
List (~>) x1 x2
-> List (~>) y1 y2 -> List (~>) (x1 ** y1) (x2 ** y2)
`par` List (~>) (Fold (UN L (L as1))) (Fold (UN L (L bs1)))
List (~>) (L (UN L (Fold (b : bs1)))) (L (UN L (Fold (b : bs1))))
fass) (Fold (UN L (L (UN L b ++ UN L (L (UN L (Fold (b : bs1)))))))
 ~> Fold
      (UN L (L (UN L (L (UN L b)) ++ UN L (L (UN L (Fold (b : bs1))))))))
-> ((Ob
       (Fold (UN L (L (UN L b ++ UN L (L (UN L (Fold (b : bs1)))))))),
     Ob
       (Fold
          (UN
             L (L (UN L (L (UN L b)) ++ UN L (L (UN L (Fold (b : bs1))))))))) =>
    (:.:)
      Tensor
      (List Tensor)
      (Fold (UN L b ++ UN L (Fold (b : bs1))))
      (L (b : b : bs1)))
-> (:.:)
     Tensor
     (List Tensor)
     (Fold (UN L b ++ UN L (Fold (b : bs1))))
     (L (b : b : bs1))
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// Strictified
  (UN L b ** UN L (Fold (b : bs1))) ('[Fold (UN L b)] ** UN L b)
Strictified
  (UN L b ++ UN L (Fold (b : bs1))) (Fold (UN L b) : UN L b)
fasg Strictified
  (UN L b ++ UN L (Fold (b : bs1))) (Fold (UN L b) : UN L b)
-> ((Ob (UN L b ++ UN L (Fold (b : bs1))),
     Ob (Fold (UN L b) : UN L b)) =>
    (:.:)
      Tensor
      (List Tensor)
      (Fold (UN L b ++ UN L (Fold (b : bs1))))
      (L (b : b : bs1)))
-> (:.:)
     Tensor
     (List Tensor)
     (Fold (UN L b ++ UN L (Fold (b : bs1))))
     (L (b : b : bs1))
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (('[Fold (UN L b ++ UN L (Fold (b : bs1)))]
 ~> UN L (L (Fold (UN L b) : UN L b)))
-> Tensor
     (Fold (UN L b ++ UN L (Fold (b : bs1))))
     (L (Fold (UN L b) : UN L b))
forall {k} (bs :: LIST k) (a :: k).
Ob bs =>
('[a] ~> UN L bs) -> Tensor a bs
Tensor ((Fold '[Fold (UN L b ++ UN L (Fold (b : bs1)))]
 ~> Fold (Fold (UN L b) : UN L b))
-> Strictified
     '[Fold (UN L b ++ UN L (Fold (b : bs1)))] (Fold (UN L b) : UN L b)
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str.Str (Strictified
  (UN L b ++ UN L (Fold (b : bs1))) (Fold (UN L b) : UN L b)
-> Fold (UN L b ++ UN L (Fold (b : bs1)))
   ~> Fold (Fold (UN L b) : UN L b)
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
Str.unStr Strictified
  (UN L b ** UN L (Fold (b : bs1))) ('[Fold (UN L b)] ** UN L b)
Strictified
  (UN L b ++ UN L (Fold (b : bs1))) (Fold (UN L b) : UN L b)
fasg))) Tensor
  (Fold (UN L b ++ UN L (Fold (b : bs1))))
  (L (Fold (UN L b) : UN L b))
-> List Tensor (L (Fold (UN L b) : UN L b)) (L (b : b : bs1))
-> (:.:)
     Tensor
     (List Tensor)
     (Fold (UN L b ++ UN L (Fold (b : bs1))))
     (L (b : b : bs1))
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: Tensor (Fold (UN L b)) b
-> List Tensor (L (UN L b)) (L (b : bs1))
-> List Tensor (L (Fold (UN L b) : UN L b)) (L (b : b : bs1))
forall {k} {j} (as1 :: [k]) (bs1 :: [j]) (p :: j +-> k) (a :: k)
       (b :: j).
(IsList as1, IsList bs1) =>
p a b
-> List p (L as1) (L bs1) -> List p (L (a : as1)) (L (b : bs1))
Cons (('[Fold (UN L b)] ~> UN L b) -> Tensor (Fold (UN L b)) b
forall {k} (bs :: LIST k) (a :: k).
Ob bs =>
('[a] ~> UN L bs) -> Tensor a bs
Tensor ((Fold '[Fold (UN L b)] ~> Fold (UN L b))
-> Strictified '[Fold (UN L b)] (UN L b)
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str.Str Fold '[Fold (UN L b)] ~> Fold (UN L b)
Fold (UN L b) ~> Fold (UN L b)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)) List Tensor b (L (b : bs1))
List Tensor (L (UN L b)) (L (b : bs1))
l

instance (MonoidalProfunctor p) => PromonoidalProfunctor Tensor p where
  parN :: (Tensor :.: List p) :~> (p :.: Tensor)
parN (Tensor (Str.Str Fold '[a] ~> Fold (UN L b)
f) :.: List p b b
l) = let fl :: p (Fold (UN L b)) (Fold (UN L b))
fl = List p b b -> p (Fold (UN L b)) (Fold (UN L b))
forall {k1} {k2} (p :: k1 +-> k2) (as :: LIST k2) (bs :: LIST k1).
MonoidalProfunctor p =>
List p as bs -> p (Fold (UN L as)) (Fold (UN L bs))
foldList List p b b
l in (a ~> Fold (UN L b))
-> p (Fold (UN L b)) (Fold (UN L b)) -> p a (Fold (UN L b))
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> Fold (UN L b)
Fold '[a] ~> Fold (UN L b)
f p (Fold (UN L b)) (Fold (UN L b))
fl p a (Fold (UN L b))
-> Tensor (Fold (UN L b)) b -> (:.:) p Tensor a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: ('[Fold (UN L b)] ~> UN L b) -> Tensor (Fold (UN L b)) b
forall {k} (bs :: LIST k) (a :: k).
Ob bs =>
('[a] ~> UN L bs) -> Tensor a bs
Tensor ((Fold '[Fold (UN L b)] ~> Fold (UN L b))
-> Strictified '[Fold (UN L b)] (UN L b)
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str.Str (p (Fold (UN L b)) (Fold (UN L b)) -> Obj (Fold (UN L b))
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt p (Fold (UN L b)) (Fold (UN L b))
fl)) ((Ob (Fold (UN L b)), Ob (Fold (UN L b))) => (:.:) p Tensor a b)
-> p (Fold (UN L b)) (Fold (UN L b)) -> (:.:) p Tensor a b
forall (a :: j) (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 (Fold (UN L b)) (Fold (UN L b))
fl ((Ob b, Ob b) => (:.:) p Tensor a b)
-> List p b b -> (:.:) p Tensor a b
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 j) (b :: LIST j) r.
((Ob a, Ob b) => r) -> List p a b -> r
\\ List p b b
l

type PList :: LIST (j +-> k) -> LIST j +-> LIST k
data PList ps as bs where
  PNil :: PList (L '[]) (L '[]) (L '[])
  PCons
    :: (Ob as, Ob bs, Ob p, Ob ps) => p a b -> PList (L ps) (L as) (L bs) -> PList (L (p ': ps)) (L (a ': as)) (L (b ': bs))
instance (CategoryOf j, CategoryOf k, Ob ps) => Profunctor (PList ps :: LIST j +-> LIST k) where
  dimap :: forall (c :: LIST k) (a :: LIST k) (b :: LIST j) (d :: LIST j).
(c ~> a) -> (b ~> d) -> PList ps a b -> PList ps c d
dimap c ~> a
List (~>) c a
Nil b ~> d
List (~>) b d
Nil PList ps a b
PNil = PList ps c d
PList (L '[]) (L '[]) (L '[])
forall {j} {k}. PList (L '[]) (L '[]) (L '[])
PNil
  dimap (Cons a ~> b
l List (~>) (L as1) (L bs1)
ls) (Cons a ~> b
r List (~>) (L as1) (L bs1)
rs) (PCons p a b
f PList (L ps) (L as) (L bs)
fs) =
    List (~>) (L as1) (L bs1)
ls List (~>) (L as1) (L bs1)
-> ((Ob (L as1), Ob (L bs1)) => PList ps c d) -> PList ps c d
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
      List (~>) (L as1) (L bs1)
rs List (~>) (L as1) (L bs1)
-> ((Ob (L as1), Ob (L bs1)) => PList ps c d) -> PList ps c d
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
        p a b
-> PList (L ps) (L as1) (L bs1)
-> PList (L (p : ps)) (L (a : as1)) (L (b : bs1))
forall {k} {k} (bs :: [k]) (as :: [k]) (p :: k +-> k)
       (ps :: [k +-> k]) (a :: k) (b :: k).
(Ob bs, Ob as, Ob p, Ob ps) =>
p a b
-> PList (L ps) (L bs) (L as)
-> PList (L (p : ps)) (L (a : bs)) (L (b : as))
PCons ((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 as1 ~> L as)
-> (L bs ~> L bs1)
-> PList (L ps) (L as) (L bs)
-> PList (L ps) (L as1) (L bs1)
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) -> PList (L ps) a b -> PList (L ps) c d
dimap L as1 ~> L as
List (~>) (L as1) (L bs1)
ls L bs ~> L bs1
List (~>) (L as1) (L bs1)
rs PList (L ps) (L as) (L bs)
fs)
  dimap c ~> a
List (~>) c a
Nil Cons{} PList ps a b
ps = case PList ps a b
ps of {}
  dimap Cons{} b ~> d
List (~>) b d
Nil PList ps a b
ps = case PList ps a b
ps of {}
  (Ob a, Ob b) => r
r \\ :: forall (a :: LIST k) (b :: LIST j) r.
((Ob a, Ob b) => r) -> PList ps a b -> r
\\ PList ps a b
PNil = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ PCons p a b
f PList (L ps) (L as) (L bs)
PNil = 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 \\ PCons p a b
f fs :: PList (L ps) (L as) (L bs)
fs@PCons{} = 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) -> PList (L ps) (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) -> PList (L ps) a b -> r
\\ PList (L ps) (L as) (L bs)
fs
instance (CategoryOf j, CategoryOf k) => Functor (PList :: LIST (j +-> k) -> LIST j +-> LIST k) where
  map :: forall (a :: LIST (j +-> k)) (b :: LIST (j +-> k)).
(a ~> b) -> PList a ~> PList b
map a ~> b
List Prof a b
Nil = (PList (L '[]) :~> PList (L '[]))
-> Prof (PList (L '[])) (PList (L '[]))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \PList (L '[]) a b
PNil -> PList (L '[]) a b
PList (L '[]) (L '[]) (L '[])
forall {j} {k}. PList (L '[]) (L '[]) (L '[])
PNil
  map f :: a ~> b
f@(Cons (Prof a :~> b
n) List Prof (L as1) (L bs1)
fs) = a ~> b
List Prof (L (a : as1)) (L (b : bs1))
f List Prof (L (a : as1)) (L (b : bs1))
-> ((Ob (L (a : as1)), Ob (L (b : bs1))) =>
    Prof (PList (L (a : as1))) (PList (L (b : bs1))))
-> Prof (PList (L (a : as1))) (PList (L (b : bs1)))
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (PList (L (a : as1)) :~> PList (L (b : bs1)))
-> Prof (PList (L (a : as1))) (PList (L (b : bs1)))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof (\(PCons p a b
p PList (L ps) (L as) (L bs)
ps) -> b a b
-> PList (L bs1) (L as) (L bs)
-> PList (L (b : bs1)) (L (a : as)) (L (b : bs))
forall {k} {k} (bs :: [k]) (as :: [k]) (p :: k +-> k)
       (ps :: [k +-> k]) (a :: k) (b :: k).
(Ob bs, Ob as, Ob p, Ob ps) =>
p a b
-> PList (L ps) (L bs) (L as)
-> PList (L (p : ps)) (L (a : bs)) (L (b : as))
PCons (a a b -> b a b
a :~> b
n a a b
p a b
p) (Prof (PList (L as1)) (PList (L bs1))
-> PList (L as1) :~> PList (L bs1)
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
Prof p q -> p :~> q
unProf ((L as1 ~> L bs1) -> PList (L as1) ~> PList (L bs1)
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: LIST (j +-> k)) (b :: LIST (j +-> k)).
(a ~> b) -> PList a ~> PList b
map L as1 ~> L bs1
List Prof (L as1) (L bs1)
fs) PList (L as1) (L as) (L bs)
PList (L ps) (L as) (L bs)
ps))

type Day :: PROTENSOR k -> PROTENSOR j -> LIST (j +-> k) -> j +-> k
data Day tk tj ps a b where
  Day :: (Ob a, Ob b) => (tj b bs -> (tk a as, PList ps as bs)) -> Day tk tj ps a b
instance (Profunctor tk, Profunctor tj) => Profunctor (Day tk tj ps) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Day tk tj ps a b -> Day tk tj ps c d
dimap c ~> a
l b ~> d
r (Day tj b bs -> (tk a as, PList ps as bs)
f) =
    c ~> a
l (c ~> a) -> ((Ob c, Ob a) => Day tk tj ps c d) -> Day tk tj ps c d
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// b ~> d
r (b ~> d) -> ((Ob b, Ob d) => Day tk tj ps c d) -> Day tk tj ps c d
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (tj d bs -> (tk c as, PList ps as bs)) -> Day tk tj ps c d
forall {k} {j} (a :: k) (b :: j) (tj :: PROTENSOR j) (bs :: LIST j)
       (tk :: PROTENSOR k) (as :: LIST k) (ps :: LIST (j +-> k)).
(Ob a, Ob b) =>
(tj b bs -> (tk a as, PList ps as bs)) -> Day tk tj ps a b
Day \tj d bs
tj -> case tj b bs -> (tk a as, PList ps as bs)
f ((b ~> d) -> tj d bs -> tj b bs
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap b ~> d
r tj d bs
tj) of
      (tk a as
tk, PList ps as bs
ps) -> ((c ~> a) -> tk a as -> tk c as
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap c ~> a
l tk a as
tk, PList ps as bs
ps)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> Day tk tj ps a b -> r
\\ Day{} = r
(Ob a, Ob b) => r
r
instance (Profunctor tk, Profunctor tj) => Functor (Day tk tj) where
  map :: forall (a :: LIST (j +-> k)) (b :: LIST (j +-> k)).
(a ~> b) -> Day tk tj a ~> Day tk tj b
map a ~> b
f = (Day tk tj a :~> Day tk tj b) -> Prof (Day tk tj a) (Day tk tj b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof (\(Day tj b bs -> (tk a as, PList a as bs)
d) -> (tj b bs -> (tk a as, PList b as bs)) -> Day tk tj b a b
forall {k} {j} (a :: k) (b :: j) (tj :: PROTENSOR j) (bs :: LIST j)
       (tk :: PROTENSOR k) (as :: LIST k) (ps :: LIST (j +-> k)).
(Ob a, Ob b) =>
(tj b bs -> (tk a as, PList ps as bs)) -> Day tk tj ps a b
Day \tj b bs
k -> case tj b bs -> (tk a as, PList a as bs)
d tj b bs
k of (tk a as
tk, PList a as bs
ps) -> (tk a as
tk, Prof (PList a) (PList b) -> PList a :~> PList b
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
Prof p q -> p :~> q
unProf ((a ~> b) -> PList a ~> PList b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: LIST (j +-> k)) (b :: LIST (j +-> k)).
(a ~> b) -> PList a ~> PList b
map a ~> b
f) PList a as bs
ps))