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

module Proarrow.Category.Instance.List where

import Prelude (type (~))

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Category.Monoidal.Strictified (type (++))
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault, obj)

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

type List :: CAT (LIST k)

-- | The free monoid in CAT
data List as bs where
  Nil :: List (L '[]) (L '[])
  Cons :: (IsList as, IsList bs) => a ~> b -> List (L as) (L bs) -> List (L (a ': as)) (L (b ': bs))

mkCons :: (CategoryOf k) => (a :: k) ~> b -> L as ~> L bs -> L (a ': as) ~> L (b ': bs)
mkCons :: forall k (a :: k) (b :: k) (as :: [k]) (bs :: [k]).
CategoryOf k =>
(a ~> b) -> (L as ~> L bs) -> L (a : as) ~> L (b : bs)
mkCons a ~> b
f L as ~> L bs
fs = (a ~> b) -> List (L as) (L bs) -> List (L (a : as)) (L (b : bs))
forall {k} (as :: [k]) (bs :: [k]) (a :: k) (b :: k).
(IsList as, IsList bs) =>
(a ~> b) -> List (L as) (L bs) -> List (L (a : as)) (L (b : bs))
Cons a ~> b
f L as ~> L bs
List (L as) (L bs)
fs ((Ob (L as), Ob (L bs)) => List (L (a : as)) (L (b : bs)))
-> List (L as) (L bs) -> List (L (a : as)) (L (b : bs))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) 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 a b -> r
\\ L as ~> L bs
List (L as) (L bs)
fs

class ((as ++ bs) ++ cs ~ as ++ (bs ++ cs)) => Assoc as bs cs
instance (as ++ (bs ++ cs) ~ (as ++ bs) ++ cs) => Assoc as bs cs

class (as ~ as ++ '[], forall bs cs. (IsList bs, IsList cs) => Assoc as bs cs) => IsList as where
  listId :: List (L as) (L as)
instance IsList '[] where listId :: List (L '[]) (L '[])
listId = List (L '[]) (L '[])
forall k. List (L '[]) (L '[])
Nil
instance (CategoryOf k, Ob (a :: k), IsList as) => IsList (a ': as) where listId :: List (L (a : as)) (L (a : as))
listId = (a ~> a) -> List (L as) (L as) -> List (L (a : as)) (L (a : as))
forall {k} (as :: [k]) (bs :: [k]) (a :: k) (b :: k).
(IsList as, IsList bs) =>
(a ~> b) -> List (L as) (L bs) -> List (L (a : as)) (L (b : bs))
Cons a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id List (L as) (L as)
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: LIST k). Ob a => List a a
id

instance (CategoryOf k) => CategoryOf (LIST k) where
  type (~>) = List
  type Ob as = (Is L as, IsList (UN L as))

instance (CategoryOf k) => Promonad (List :: CAT (LIST k)) where
  id :: forall (a :: LIST k). Ob a => List a a
id = List a a
List (L (UN L a)) (L (UN L a))
forall {k} (as :: [k]). IsList as => List (L as) (L as)
listId
  List b c
Nil . :: forall (b :: LIST k) (c :: LIST k) (a :: LIST k).
List b c -> List a b -> List a c
. List a b
Nil = List a c
List (L '[]) (L '[])
forall k. List (L '[]) (L '[])
Nil
  Cons a ~> b
f List (L as) (L bs)
fs . Cons a ~> b
g List (L as) (L bs)
gs = (a ~> b) -> List (L as) (L bs) -> List (L (a : as)) (L (b : bs))
forall {k} (as :: [k]) (bs :: [k]) (a :: k) (b :: k).
(IsList as, IsList bs) =>
(a ~> b) -> List (L as) (L bs) -> List (L (a : as)) (L (b : bs))
Cons (a ~> b
f (a ~> b) -> (a ~> a) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> a
a ~> b
g) (List (L as) (L bs)
fs List (L as) (L bs) -> List (L as) (L as) -> List (L as) (L bs)
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: LIST k) (c :: LIST k) (a :: LIST k).
List b c -> List a b -> List a c
. List (L as) (L as)
List (L as) (L bs)
gs)

instance (CategoryOf k) => Profunctor (List :: CAT (LIST k)) where
  dimap :: forall (c :: LIST k) (a :: LIST k) (b :: LIST k) (d :: LIST k).
(c ~> a) -> (b ~> d) -> List a b -> List c d
dimap = (c ~> a) -> (b ~> d) -> List a b -> List c d
List c a -> List b d -> List a b -> List c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: LIST k) (b :: LIST k) r.
((Ob a, Ob b) => r) -> List a b -> r
\\ List a b
Nil = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ Cons a ~> b
f List (L as) (L bs)
fs = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f ((Ob (L as), Ob (L bs)) => r) -> List (L as) (L bs) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) 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 a b -> r
\\ List (L as) (L bs)
fs

instance (CategoryOf k) => MonoidalProfunctor (List :: CAT (LIST k)) where
  par0 :: List Unit Unit
par0 = List Unit Unit
List (L '[]) (L '[])
forall k. List (L '[]) (L '[])
Nil
  List x1 x2
Nil par :: 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 y1 y2
Nil = List (x1 ** y1) (x2 ** y2)
List (L '[]) (L '[])
forall k. List (L '[]) (L '[])
Nil
  List x1 x2
Nil `par` gs :: List y1 y2
gs@Cons{} = List y1 y2
List (x1 ** y1) (x2 ** y2)
gs
  Cons a ~> b
f List (L as) (L bs)
fs `par` List y1 y2
Nil = (a ~> b) -> (L as ~> L bs) -> L (a : as) ~> L (b : bs)
forall k (a :: k) (b :: k) (as :: [k]) (bs :: [k]).
CategoryOf k =>
(a ~> b) -> (L as ~> L bs) -> L (a : as) ~> L (b : bs)
mkCons a ~> b
f (List (L as) (L bs)
fs List (L as) (L bs)
-> List (L '[]) (L '[]) -> List (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 k) (y1 :: LIST k) (y2 :: LIST k).
List x1 x2 -> List y1 y2 -> List (x1 ** y1) (x2 ** y2)
`par` List (L '[]) (L '[])
forall k. List (L '[]) (L '[])
Nil)
  Cons a ~> b
f List (L as) (L bs)
fs `par` Cons a ~> b
g List (L as) (L bs)
gs = (a ~> b)
-> (L (as ++ (a : as)) ~> L (bs ++ (b : bs)))
-> L (a : (as ++ (a : as))) ~> L (b : (bs ++ (b : bs)))
forall k (a :: k) (b :: k) (as :: [k]) (bs :: [k]).
CategoryOf k =>
(a ~> b) -> (L as ~> L bs) -> L (a : as) ~> L (b : bs)
mkCons a ~> b
f (List (L as) (L bs)
fs List (L as) (L bs)
-> List (L (a : as)) (L (b : bs))
-> List (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 k) (y1 :: LIST k) (y2 :: LIST k).
List x1 x2 -> List y1 y2 -> List (x1 ** y1) (x2 ** y2)
`par` (a ~> b) -> List (L as) (L bs) -> List (L (a : as)) (L (b : bs))
forall {k} (as :: [k]) (bs :: [k]) (a :: k) (b :: k).
(IsList as, IsList bs) =>
(a ~> b) -> List (L as) (L bs) -> List (L (a : as)) (L (b : bs))
Cons a ~> b
g List (L as) (L bs)
gs)

instance (CategoryOf k) => Monoidal (LIST k) where
  type Unit = L '[]
  type p ** q = L (UN L p ++ UN L q)
  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} (as :: [k]). IsList as => List (L as) (L as)
listId
  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} (as :: [k]). IsList as => List (L as) (L as)
listId
  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} (as :: [k]). IsList as => List (L as) (L as)
listId
  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} (as :: [k]). IsList as => List (L as) (L as)
listId
  associator :: forall (a :: LIST k) (b :: LIST k) (c :: LIST k).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(L as) @(L bs) @(L cs) = List
  (L ((UN L a ++ UN L b) ++ UN L c))
  (L (UN L a ++ (UN L b ++ UN L c)))
List
  (L ((UN L a ++ UN L b) ++ UN L c))
  (L ((UN L a ++ UN L b) ++ UN L c))
(Ob ((L (UN L a) ** L (UN L b)) ** L (UN L c)),
 Ob ((L (UN L a) ** L (UN L b)) ** L (UN L c))) =>
List
  (L ((UN L a ++ UN L b) ++ UN L c))
  (L (UN L a ++ (UN L b ++ UN L c)))
forall {k} (as :: [k]). IsList as => List (L as) (L as)
listId ((Ob ((L (UN L a) ** L (UN L b)) ** L (UN L c)),
  Ob ((L (UN L a) ** L (UN L b)) ** L (UN L c))) =>
 List
   (L ((UN L a ++ UN L b) ++ UN L c))
   (L (UN L a ++ (UN L b ++ UN L c))))
-> List
     ((L (UN L a) ** L (UN L b)) ** L (UN L c))
     ((L (UN L a) ** L (UN L b)) ** L (UN L c))
-> List
     (L ((UN L a ++ UN L b) ++ UN L c))
     (L (UN L a ++ (UN L b ++ UN L c)))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) 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 a b -> r
\\ (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: LIST k). (CategoryOf (LIST k), Ob a) => Obj a
obj @(L as) List (L (UN L a)) (L (UN L a))
-> List (L (UN L b)) (L (UN L b))
-> List (L (UN L a) ** L (UN L b)) (L (UN L a) ** L (UN L b))
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` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: LIST k). (CategoryOf (LIST k), Ob a) => Obj a
obj @(L bs)) List (L (UN L a) ** L (UN L b)) (L (UN L a) ** L (UN L b))
-> List (L (UN L c)) (L (UN L c))
-> List
     ((L (UN L a) ** L (UN L b)) ** L (UN L c))
     ((L (UN L a) ** L (UN L b)) ** L (UN L c))
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` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: LIST k). (CategoryOf (LIST k), Ob a) => Obj a
obj @(L cs)
  associatorInv :: forall (a :: LIST k) (b :: LIST k) (c :: LIST k).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(L as) @(L bs) @(L cs) = List
  (L (UN L a ++ (UN L b ++ UN L c)))
  (L (UN L a ++ (UN L b ++ UN L c)))
List
  (L (UN L a ++ (UN L b ++ UN L c)))
  (L ((UN L a ++ UN L b) ++ UN L c))
(Ob (L (UN L a) ** L (UN L (L (UN L b)) ++ UN L (L (UN L c)))),
 Ob (L (UN L a) ** L (UN L (L (UN L b)) ++ UN L (L (UN L c))))) =>
List
  (L (UN L a ++ (UN L b ++ UN L c)))
  (L ((UN L a ++ UN L b) ++ UN L c))
forall {k} (as :: [k]). IsList as => List (L as) (L as)
listId ((Ob (L (UN L a) ** L (UN L (L (UN L b)) ++ UN L (L (UN L c)))),
  Ob (L (UN L a) ** L (UN L (L (UN L b)) ++ UN L (L (UN L c))))) =>
 List
   (L (UN L a ++ (UN L b ++ UN L c)))
   (L ((UN L a ++ UN L b) ++ UN L c)))
-> List
     (L (UN L a) ** L (UN L (L (UN L b)) ++ UN L (L (UN L c))))
     (L (UN L a) ** L (UN L (L (UN L b)) ++ UN L (L (UN L c))))
-> List
     (L (UN L a ++ (UN L b ++ UN L c)))
     (L ((UN L a ++ UN L b) ++ UN L c))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) 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 a b -> r
\\ forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: LIST k). (CategoryOf (LIST k), Ob a) => Obj a
obj @(L as) List (L (UN L a)) (L (UN L a))
-> List
     (L (UN L (L (UN L b)) ++ UN L (L (UN L c))))
     (L (UN L (L (UN L b)) ++ UN L (L (UN L c))))
-> List
     (L (UN L a) ** L (UN L (L (UN L b)) ++ UN L (L (UN L c))))
     (L (UN L a) ** L (UN L (L (UN L b)) ++ UN L (L (UN L c))))
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` (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: LIST k). (CategoryOf (LIST k), Ob a) => Obj a
obj @(L bs) List (L (UN L b)) (L (UN L b))
-> List (L (UN L c)) (L (UN L c))
-> List (L (UN L b) ** L (UN L c)) (L (UN L b) ** L (UN L c))
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` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: LIST k). (CategoryOf (LIST k), Ob a) => Obj a
obj @(L cs))