{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Proarrow.Category.Instance.List where

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

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 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 => Monoidal (LIST k) where
  type Unit = L '[]
  type p ** q = L (UN L p ++ UN L q)
  a ~> b
List a b
Nil par :: forall (a :: LIST k) (b :: LIST k) (c :: LIST k) (d :: LIST k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` c ~> d
List c d
Nil = (a ** c) ~> (b ** d)
List (L '[]) (L '[])
forall k. List (L '[]) (L '[])
Nil
  a ~> b
List a b
Nil `par` gs :: c ~> d
gs@Cons{} = c ~> d
(a ** c) ~> (b ** d)
gs
  Cons a ~> b
f List (L as) (L bs)
fs `par` c ~> d
List c d
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 (L as ~> L bs
List (L as) (L bs)
fs (L as ~> L bs)
-> (L '[] ~> L '[]) -> (L as ** L '[]) ~> (L bs ** L '[])
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall (a :: LIST k) (b :: LIST k) (c :: LIST k) (d :: LIST k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` L '[] ~> L '[]
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 (L as ~> L bs
List (L as) (L bs)
fs (L as ~> L bs)
-> (L (a : as) ~> L (b : bs))
-> (L as ** L (a : as)) ~> (L bs ** L (b : bs))
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall (a :: LIST k) (b :: LIST k) (c :: LIST k) (d :: LIST k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`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)
  leftUnitor :: forall (a :: LIST k). Obj a -> (Unit ** a) ~> a
leftUnitor Obj a
f = List (L (UN L a)) a
List (L (UN L a)) (L (UN L a))
(Ob a, Ob a) => List (L (UN L a)) a
forall {k} (as :: [k]). IsList as => List (L as) (L as)
listId ((Ob a, Ob a) => List (L (UN L a)) a)
-> List a a -> List (L (UN L a)) a
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
\\ Obj a
List a a
f
  leftUnitorInv :: forall (a :: LIST k). Obj a -> a ~> (Unit ** a)
leftUnitorInv Obj a
f = List a (L (UN L a))
List (L (UN L a)) (L (UN L a))
(Ob a, Ob a) => List a (L (UN L a))
forall {k} (as :: [k]). IsList as => List (L as) (L as)
listId ((Ob a, Ob a) => List a (L (UN L a)))
-> List a a -> List a (L (UN L a))
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
\\ Obj a
List a a
f
  rightUnitor :: forall (a :: LIST k). Obj a -> (a ** Unit) ~> a
rightUnitor Obj a
List a a
Nil = (a ** Unit) ~> a
List (L '[]) (L '[])
forall {k} (as :: [k]). IsList as => List (L as) (L as)
listId
  rightUnitor (Cons a ~> b
f List (L as) (L bs)
fs) = (b ~> b)
-> (L (bs ++ '[]) ~> L bs) -> L (b : (bs ++ '[])) ~> 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
b ~> b
f (Obj (L bs) -> (L bs ** Unit) ~> L bs
forall k (a :: k). Monoidal k => Obj a -> (a ** Unit) ~> a
forall (a :: LIST k). Obj a -> (a ** Unit) ~> a
rightUnitor Obj (L bs)
List (L as) (L bs)
fs)
  rightUnitorInv :: forall (a :: LIST k). Obj a -> a ~> (a ** Unit)
rightUnitorInv Obj a
List a a
Nil = a ~> (a ** Unit)
List (L '[]) (L '[])
forall {k} (as :: [k]). IsList as => List (L as) (L as)
listId
  rightUnitorInv (Cons a ~> b
f List (L as) (L bs)
fs) = (b ~> b)
-> (L bs ~> L (bs ++ '[])) -> L (b : bs) ~> 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
b ~> b
f (Obj (L bs) -> L bs ~> (L bs ** Unit)
forall k (a :: k). Monoidal k => Obj a -> a ~> (a ** Unit)
forall (a :: LIST k). Obj a -> a ~> (a ** Unit)
rightUnitorInv Obj (L bs)
List (L as) (L bs)
fs)
  associator :: forall (a :: LIST k) (b :: LIST k) (c :: LIST k).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator Obj a
List a a
Nil Obj b
bs Obj c
cs = List (L (UN L b ++ UN L c)) (L (UN L b ++ UN L c))
(Ob (b ** c), Ob (b ** c)) =>
List (L (UN L b ++ UN L c)) (L (UN L b ++ UN L c))
forall {k} (as :: [k]). IsList as => List (L as) (L as)
listId ((Ob (b ** c), Ob (b ** c)) =>
 List (L (UN L b ++ UN L c)) (L (UN L b ++ UN L c)))
-> ((b ** c) ~> (b ** c))
-> List (L (UN L b ++ UN L c)) (L (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) -> (a ~> b) -> r
\\ Obj b
bs Obj b -> Obj c -> (b ** c) ~> (b ** c)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall (a :: LIST k) (b :: LIST k) (c :: LIST k) (d :: LIST k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Obj c
cs
  associator (Cons a ~> b
f List (L as) (L bs)
fs) Obj b
bs Obj c
cs = (b ~> b)
-> (L ((bs ++ UN L b) ++ UN L c) ~> L (bs ++ (UN L b ++ UN L c)))
-> L (b : ((bs ++ UN L b) ++ UN L c))
   ~> L (b : (bs ++ (UN L b ++ UN L c)))
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
b ~> b
f (Obj (L bs)
-> Obj b -> Obj c -> ((L bs ** b) ** c) ~> (L bs ** (b ** c))
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
forall (a :: LIST k) (b :: LIST k) (c :: LIST k).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator Obj (L bs)
List (L as) (L bs)
fs Obj b
bs Obj c
cs)
  associatorInv :: forall (a :: LIST k) (b :: LIST k) (c :: LIST k).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv Obj a
List a a
Nil Obj b
bs Obj c
cs = List (L (UN L b ++ UN L c)) (L (UN L b ++ UN L c))
(Ob (b ** c), Ob (b ** c)) =>
List (L (UN L b ++ UN L c)) (L (UN L b ++ UN L c))
forall {k} (as :: [k]). IsList as => List (L as) (L as)
listId ((Ob (b ** c), Ob (b ** c)) =>
 List (L (UN L b ++ UN L c)) (L (UN L b ++ UN L c)))
-> ((b ** c) ~> (b ** c))
-> List (L (UN L b ++ UN L c)) (L (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) -> (a ~> b) -> r
\\ Obj b
bs Obj b -> Obj c -> (b ** c) ~> (b ** c)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall (a :: LIST k) (b :: LIST k) (c :: LIST k) (d :: LIST k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Obj c
cs
  associatorInv (Cons a ~> b
f List (L as) (L bs)
fs) Obj b
bs Obj c
cs = (b ~> b)
-> (L (bs ++ (UN L b ++ UN L c)) ~> L ((bs ++ UN L b) ++ UN L c))
-> L (b : (bs ++ (UN L b ++ UN L c)))
   ~> L (b : ((bs ++ UN L b) ++ UN L c))
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
b ~> b
f (Obj (L bs)
-> Obj b -> Obj c -> (L bs ** (b ** c)) ~> ((L bs ** b) ** c)
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
forall (a :: LIST k) (b :: LIST k) (c :: LIST k).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv Obj (L bs)
List (L as) (L bs)
fs Obj b
bs Obj c
cs)