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

-- | The category __freely generated__ by a quiver @p@ of generator arrows, extended with a chosen
-- list @cs@ of structural classes (terminal object, products, closed structure, ...): an arrow of
-- @'FREE' cs p@ is a formal composite of generators ('Emb') and structure morphisms ('St'). 'fold'
-- interprets such an arrow in any category supporting the same structures, making this the basis
-- for deeply embedded categorical DSLs.
--
-- For a quiver with no structures, "Proarrow.Category.Instance.Paths" fits better: its objects are
-- the vertices themselves, which keep the base kind's 'Ob' and can be taken apart.
--
-- __No equations__: only the category laws hold structurally (composition is a normalized spine).
-- For example @'Proarrow.Limit.BinaryProduct.fst' . (f 'Proarrow.Limit.BinaryProduct.&&&' g)@ and
-- @f@ are different 'Free' values. Two arrows are equal when every 'fold' identifies them, so
-- decide equality by interpreting into a concrete category, not by pattern matching.
--
-- An object is a /shape/ ('IsFreeOb'), asking nothing of @k@ beyond being a category. Its
-- denotation along a functor @f@ out of @k@ is @'Lower' f a@, and 'withLowerOb' recovers that
-- denotation's 'Ob' in 'fold'.
--
-- Classes imposing type equalities (like 'Proarrow.Category.Monoidal.Cartesian.Cartesian'\'s
-- @tensor = product@) cannot be listed in @cs@, since each carrier is fixed (@**@ is always the
-- formal tensor). A kind wrapper can recover the instance:
-- @'Proarrow.Limit.BinaryProduct.PROD' ('FREE' '[HasTerminalObject, HasBinaryProducts] p)@ /is/ a
-- free cartesian category.
module Proarrow.Category.Instance.Free where

import Data.Kind (Constraint)
import Prelude (Show (..))
import Prelude qualified as P

import Proarrow.Category.Enriched.Thin (Discrete (..))
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Hom
  , Kind
  , Profunctor (..)
  , Promonad (..)
  , Show2
  , dimapDefault
  , (//)
  , type (+->)
  )
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Profunctor.Instance.Identity (Id)
import Proarrow.Profunctor.Instance.Initial (InitialProfunctor)
import Proarrow.Profunctor.Representable (Rep, Representable (..), withObRep)

type family All (cs :: [Kind -> Constraint]) (k :: Kind) :: Constraint where
  All '[] k = ()
  All (c ': cs) k = (c k, All cs k)

-- | Membership of a structure in the list, with the entailment @'All' cs k => c k@ as a method
-- rather than a quantified superclass: as a given, the quantified form would shadow the ordinary
-- instances for the free category itself and demand @All cs (FREE cs p)@.
type Elem :: (Kind -> Constraint) -> [Kind -> Constraint] -> Constraint
class c `Elem` cs where
  fromAll :: forall k r. (All cs k) => ((c k) => r) -> r

instance {-# OVERLAPPABLE #-} (c `Elem` cs) => c `Elem` (d ': cs) where
  fromAll :: forall (k :: Kind) (r :: Kind). All (d : cs) k => (c k => r) -> r
fromAll @k c k => r
r = forall (c :: Kind -> Constraint) (cs :: [Kind -> Constraint])
       (k :: Kind) (r :: Kind).
(Elem c cs, All cs k) =>
(c k => r) -> r
fromAll @c @cs @k r
c k => r
r
instance c `Elem` (c ': cs) where
  fromAll :: forall (k :: Kind) (r :: Kind). All (c : cs) k => (c k => r) -> r
fromAll c k => r
r = r
c k => r
r

-- | Membership of several structures at once: @'[Monoidal, SymMonoidal] \`Elems\` cs@.
type Elems :: [Kind -> Constraint] -> [Kind -> Constraint] -> Constraint
type family ds `Elems` cs where
  '[] `Elems` cs = ()
  (d ': ds) `Elems` cs = (d `Elem` cs, ds `Elems` cs)

-- | The objects of the free category over the quiver @p@ on @k@: the embedded objects of @k@
-- ('EMB') plus one object former per structure in @cs@ (products, exponentials, ...), which live
-- in their structures' modules.
type data FREE (cs :: [Kind -> Constraint]) (p :: CAT k) = EMB k

-- | Arrows of the free category: a right-associated composition spine ending in 'Nil', with a
-- generator ('Emb') or structure morphism ('St') precomposed onto the rest at each step, so
-- the category laws hold definitionally. The fields are linear (@%1@) so that DSL
-- helpers built on 'Free' can offer HOAS-style binders whose bound variable must be used exactly
-- once.
type Free :: CAT (FREE cs p)
data Free a b where
  Nil :: (Ob a) => Free a a
  Emb :: (Ob a, Ob b) => p a b %1 -> Free (i :: FREE cs p) (EMB a) %1 -> Free i (EMB b)
  St
    :: forall {k} {cs} {p :: CAT k} (c :: Kind -> Constraint) (a :: FREE cs p) b i
     . (HasStructure cs p c, Ob a, Ob b)
    => Struct c a b %1 -> Free i a %1 -> Free i b

emb :: (Ob a, Ob b) => p a b %1 -> Free (EMB a :: FREE cs p) (EMB b)
emb :: forall {k :: Kind} (a :: k) (b :: k) (p :: k -> k -> Kind)
       (cs :: [Kind -> Constraint]).
(Ob a, Ob b) =>
p a b %1 -> Free (EMB a) (EMB b)
emb p a b
p = p a b -> Free (EMB a) (EMB a) -> Free (EMB a) (EMB b)
forall {k :: Kind} (c :: k) (a :: k) (p :: k -> k -> Kind)
       (cs :: [Kind -> Constraint]) (i :: FREE cs p).
(Ob c, Ob a) =>
p c a -> Free i (EMB c) -> Free i (EMB a)
Emb p a b
p Free (EMB a) (EMB a)
forall {k :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil

class (Show2 p) => WithShow (a :: FREE c (p :: CAT j))
instance (Show2 p) => WithShow (a :: FREE c (p :: CAT j))

instance (WithShow a) => Show (Free a b) where
  showsPrec :: Int -> Free a b -> ShowS
showsPrec Int
_ Free a b
Nil = String -> ShowS
P.showString String
"id"
  showsPrec Int
d (Emb p a b
p Free a (EMB a)
g) = Int -> p a b -> Free a (EMB a) -> ShowS
forall {k :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT k}
       (p :: Kind) (a :: FREE cs p) (b :: FREE cs p).
(Show p, WithShow a) =>
Int -> p -> Free a b -> ShowS
showPostComp Int
d p a b
p Free a (EMB a)
g
  showsPrec Int
d (St Struct c a b
s Free a a
g) = Int -> Struct c a b -> Free a a -> ShowS
forall {k :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT k}
       (p :: Kind) (a :: FREE cs p) (b :: FREE cs p).
(Show p, WithShow a) =>
Int -> p -> Free a b -> ShowS
showPostComp Int
d Struct c a b
s Free a a
g

showPostComp :: (Show p, WithShow a) => P.Int -> p -> Free a b -> P.ShowS
showPostComp :: forall {k :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT k}
       (p :: Kind) (a :: FREE cs p) (b :: FREE cs p).
(Show p, WithShow a) =>
Int -> p -> Free a b -> ShowS
showPostComp Int
d p
p Free a b
Nil = Int -> p -> ShowS
forall (a :: Kind). Show a => Int -> a -> ShowS
P.showsPrec Int
d p
p
showPostComp Int
d p
p Free a b
g = Bool -> ShowS -> ShowS
P.showParen (Int
d Int -> Int -> Bool
forall (a :: Kind). Ord a => a -> a -> Bool
P.> Int
9) (Int -> p -> ShowS
forall (a :: Kind). Show a => Int -> a -> ShowS
P.showsPrec Int
10 p
p ShowS -> ShowS -> ShowS
forall (b :: Kind) (c :: Kind) (a :: Kind).
(b -> c) -> (a -> b) -> a -> c
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. String -> ShowS
P.showString String
" . " ShowS -> ShowS -> ShowS
forall (b :: Kind) (c :: Kind) (a :: Kind).
(b -> c) -> (a -> b) -> a -> c
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Int -> Free a b -> ShowS
forall (a :: Kind). Show a => Int -> a -> ShowS
P.showsPrec Int
10 Free a b
g)

-- | The shape of an object of the free category, by object former. This is 'Ob' for the free
-- category. It carries the shape's denotation 'Lower' along any functor out of @k@, and how to
-- recover that denotation's 'Ob' from the leaves' ('lowerOb', normally used through
-- 'withLowerOb' and 'withLowerIdOb').
type IsFreeOb :: forall {k} {cs :: [Kind -> Constraint]} {p :: CAT k}. FREE cs p -> Constraint
class IsFreeOb (a :: FREE cs (p :: CAT k)) where
  -- | The denotation of the object along a functor @f@ out of @k@. (The class variable is
  -- re-annotated here so that @k@ is in scope before @f@'s kind mentions it.)
  type Lower (f :: k +-> k') (a :: FREE cs p) :: k'

  lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => ((Ob (Lower f a)) => r) -> r

instance (Ob a) => IsFreeOb (EMB a) where
  type Lower f (EMB a) = f % a
  lowerOb :: forall (k' :: Kind) (f :: k +-> k') (r :: Kind).
(Representable f, All cs k') =>
(Ob (Lower f (EMB a)) => r) -> r
lowerOb @_ @f = forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: j) (r :: Kind).
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: k +-> k') (a :: k) (r :: Kind).
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @f @a

-- | @'Ob' ('Lower' f a)@ from the shape of @a@, for interpreting along @f@.
withLowerOb
  :: forall {k} {k'} {cs} {p :: CAT k} (f :: k +-> k') a r
   . (IsFreeOb (a :: FREE cs p), Representable f, All cs k')
  => ((Ob (Lower f a)) => r) -> r
withLowerOb :: forall {k :: Kind} {k' :: Kind} {cs :: [Kind -> Constraint]}
       {p :: CAT k} (f :: k +-> k') (a :: FREE cs p) (r :: Kind).
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb = forall {k :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT k}
       (a :: FREE cs p) (k' :: Kind) (f :: k +-> k') (r :: Kind).
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) (k' :: Kind) (f :: k +-> k') (r :: Kind).
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
lowerOb @a @k' @f

-- | 'withLowerOb' along the identity: the 'Ob' of a shape's denotation in @k@ itself, when @k@
-- happens to carry the structures @cs@.
withLowerIdOb
  :: forall {k} {cs} {p :: CAT k} a r
   . (IsFreeOb (a :: FREE cs p), CategoryOf k, All cs k)
  => ((Ob (Lower (Id :: CAT k) a)) => r) -> r
withLowerIdOb :: forall {k :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT k}
       (a :: FREE cs p) (r :: Kind).
(IsFreeOb a, CategoryOf k, All cs k) =>
(Ob (Lower Id a) => r) -> r
withLowerIdOb = forall {k :: Kind} {k' :: Kind} {cs :: [Kind -> Constraint]}
       {p :: CAT k} (f :: k +-> k') (a :: FREE cs p) (r :: Kind).
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k) (a :: FREE cs p) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @(Id :: CAT k) @a

class ((Show2 p) => Show2 str) => CanShow (str :: CAT (FREE cs p))
instance ((Show2 p) => Show2 str) => CanShow (str :: CAT (FREE cs p))

class
  (CanShow (Struct c :: CAT (FREE cs p)), c `Elem` cs) =>
  HasStructure cs (p :: CAT k) (c :: Kind -> Constraint)
  where
  data Struct c :: CAT (FREE cs p)
  foldStructure
    :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p)
     . (c k', All cs k', Representable f)
    => (forall (x :: FREE cs p) y. x ~> y -> Lower f x ~> Lower f y)
    -> Struct c a b
    -> Lower f a ~> Lower f b

-- | Interpret a free arrow along a functor @f@ into any category @k'@ supporting the structures
-- @cs@, given an interpretation of the generators between the images of their objects. This is
-- the universal property of the free category. The interpreter is handed @('Ob' x, 'Ob' y)@ explicitly
-- (the evidence bundled on 'Emb'), because a bare quiver @p@ is not a 'Profunctor', so the 'Ob's
-- cannot be recovered from the value.
fold
  :: forall {k} {k'} {p :: CAT k} (cs :: [Kind -> Constraint]) (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p)
   . (All cs k', Representable f)
  => (forall x y. (Ob x, Ob y) => p x y -> (f % x) ~> (f % y))
  -> a ~> b
  -> Lower f a ~> Lower f b
fold :: forall {k :: Kind} {k' :: Kind} {p :: CAT k}
       (cs :: [Kind -> Constraint]) (f :: k +-> k') (a :: FREE cs p)
       (b :: FREE cs p).
(All cs k', Representable f) =>
(forall (x :: k) (y :: k).
 (Ob x, Ob y) =>
 p x y -> (f % x) ~> (f % y))
-> (a ~> b) -> Lower f a ~> Lower f b
fold forall (x :: k) (y :: k).
(Ob x, Ob y) =>
p x y -> (f % x) ~> (f % y)
pn = (a ~> b) -> Lower f a ~> Lower f b
forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go
  where
    go :: forall (x :: FREE cs p) y. x ~> y -> Lower f x ~> Lower f y
    go :: forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go x ~> y
Free x y
Nil = forall {k :: Kind} {k' :: Kind} {cs :: [Kind -> Constraint]}
       {p :: CAT k} (f :: k +-> k') (a :: FREE cs p) (r :: Kind).
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) (r :: Kind).
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @x Lower f x ~> Lower f x
Ob (Lower f x) => Lower f x ~> Lower f x
forall (a :: k'). Ob a => a ~> a
forall {k :: Kind} (p :: CAT k) (a :: k).
(Promonad p, Ob a) =>
p a a
id
    go (Emb p a b
p Free x (EMB a)
g) = p a b -> (f % a) ~> (f % b)
forall (x :: k) (y :: k).
(Ob x, Ob y) =>
p x y -> (f % x) ~> (f % y)
pn p a b
p ((f % a) ~> (f % b))
-> (Lower f x ~> (f % a)) -> Lower f x ~> (f % b)
forall (b :: k') (c :: k') (a :: k').
(b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (x ~> EMB a) -> Lower f x ~> Lower f (EMB a)
forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go x ~> EMB a
Free x (EMB a)
g
    go (St @c Struct c a y
s Free x a
g) = forall (c :: Kind -> Constraint) (cs :: [Kind -> Constraint])
       (k :: Kind) (r :: Kind).
(Elem c cs, All cs k) =>
(c k => r) -> r
fromAll @c @cs @k' (forall (k :: Kind) (cs :: [Kind -> Constraint]) (p :: CAT k)
       (c :: Kind -> Constraint) {k' :: Kind} (f :: k +-> k')
       (a :: FREE cs p) (b :: FREE cs p).
(HasStructure cs p c, c k', All cs k', Representable f) =>
(forall (x :: FREE cs p) (y :: FREE cs p).
 (x ~> y) -> Lower f x ~> Lower f y)
-> Struct c a b -> Lower f a ~> Lower f b
foldStructure @_ @_ @_ @_ @f (x ~> y) -> Lower f x ~> Lower f y
forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go Struct c a y
s) (Lower f a ~> Lower f y)
-> (Lower f x ~> Lower f a) -> Lower f x ~> Lower f y
forall (b :: k') (c :: k') (a :: k').
(b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (x ~> a) -> Lower f x ~> Lower f a
forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go x ~> a
Free x a
g

retract
  :: forall {k} {k'} cs (f :: k +-> k') a b
   . (All cs k', Representable f) => (a :: FREE cs (InitialProfunctor :: CAT k)) ~> b -> Lower f a ~> Lower f b
retract :: forall {k :: Kind} {k' :: Kind} (cs :: [Kind -> Constraint])
       (f :: k +-> k') (a :: FREE cs InitialProfunctor)
       (b :: FREE cs InitialProfunctor).
(All cs k', Representable f) =>
(a ~> b) -> Lower f a ~> Lower f b
retract = forall (cs :: [Kind -> Constraint]) (f :: k +-> k')
       (a :: FREE cs InitialProfunctor) (b :: FREE cs InitialProfunctor).
(All cs k', Representable f) =>
(forall (x :: k) (y :: k).
 (Ob x, Ob y) =>
 InitialProfunctor x y -> (f % x) ~> (f % y))
-> (a ~> b) -> Lower f a ~> Lower f b
forall {k :: Kind} {k' :: Kind} {p :: CAT k}
       (cs :: [Kind -> Constraint]) (f :: k +-> k') (a :: FREE cs p)
       (b :: FREE cs p).
(All cs k', Representable f) =>
(forall (x :: k) (y :: k).
 (Ob x, Ob y) =>
 p x y -> (f % x) ~> (f % y))
-> (a ~> b) -> Lower f a ~> Lower f b
fold @cs @f (\case {})

-- | Taking the quiver to be the /hom of a category/ @k@ makes @'FREE' cs ('Proarrow.Core.Hom' k)@
-- the free @cs@-structured category over @k@: 'liftFree' embeds the arrows of @k@ as generators,
-- and when @k@ itself already has the structures, 'retractFree' interprets back into @k@ along the
-- identity. These back the free-kind instances of
-- 'Proarrow.Profunctor.Free.HasFreeK' (e.g. the free category with a terminal object, or with
-- binary products, over @k@).
liftFree :: forall {k} cs (x :: k) y. (CategoryOf k) => (x ~> y) -> (EMB x :: FREE cs (Hom k)) ~> EMB y
liftFree :: forall {k :: Kind} (cs :: [Kind -> Constraint]) (x :: k) (y :: k).
CategoryOf k =>
(x ~> y) -> EMB x ~> EMB y
liftFree x ~> y
f = (x ~> y) %1 -> Free (EMB x) (EMB y)
forall {k :: Kind} (a :: k) (b :: k) (p :: k -> k -> Kind)
       (cs :: [Kind -> Constraint]).
(Ob a, Ob b) =>
p a b %1 -> Free (EMB a) (EMB b)
emb x ~> y
f ((Ob x, Ob y) => Free (EMB x) (EMB y))
-> (x ~> y) -> Free (EMB x) (EMB y)
forall (a :: k) (b :: k) (r :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ x ~> y
f

retractFree
  :: forall cs {k} (a :: FREE cs (Hom k)) b
   . (CategoryOf k, All cs k)
  => a ~> b
  -> Lower (Id :: CAT k) a ~> Lower (Id :: CAT k) b
retractFree :: forall (cs :: [Kind -> Constraint]) {k :: Kind}
       (a :: FREE cs (Hom k)) (b :: FREE cs (Hom k)).
(CategoryOf k, All cs k) =>
(a ~> b) -> Lower Id a ~> Lower Id b
retractFree = forall (cs :: [Kind -> Constraint]) (f :: k +-> k)
       (a :: FREE cs (~>)) (b :: FREE cs (~>)).
(All cs k, Representable f) =>
(forall (x :: k) (y :: k).
 (Ob x, Ob y) =>
 (x ~> y) -> (f % x) ~> (f % y))
-> (a ~> b) -> Lower f a ~> Lower f b
forall {k :: Kind} {k' :: Kind} {p :: CAT k}
       (cs :: [Kind -> Constraint]) (f :: k +-> k') (a :: FREE cs p)
       (b :: FREE cs p).
(All cs k', Representable f) =>
(forall (x :: k) (y :: k).
 (Ob x, Ob y) =>
 p x y -> (f % x) ~> (f % y))
-> (a ~> b) -> Lower f a ~> Lower f b
fold @cs @(Id :: CAT k) (\x ~> y
g -> x ~> y
(Id % x) ~> (Id % y)
g)

-- | The object-embedding functor @a |-> 'EMB' a@ of a widening (see 'widen'), as a representable
-- profunctor. The base kind must be 'Discrete', since arrows of @k@ other than identities have no
-- counterpart in the free category.
data family Embed :: k +-> FREE ds (p :: CAT k)

instance (Discrete k) => FunctorForRep (Embed :: k +-> FREE ds (p :: CAT k)) where
  type Embed @ a = EMB a
  fmap :: forall (a :: k) (b :: k). (a ~> b) -> (Embed @ a) ~> (Embed @ b)
fmap (a ~> b
f :: x ~> y) = a ~> b
f (a ~> b)
-> ((Ob a, Ob b) => Free (EMB a) (EMB b)) -> Free (EMB a) (EMB b)
forall {k1 :: Kind} {k2 :: Kind} (p :: k1 +-> k2) (a :: k2)
       (b :: k1) (r :: Kind).
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (a ~> b)
-> ((a ~ b) => Free (EMB a) (EMB b)) -> Free (EMB a) (EMB b)
forall (a :: k) (b :: k) (r :: Kind).
(a ~> b) -> ((a ~ b) => r) -> r
forall (k :: Kind) (a :: k) (b :: k) (r :: Kind).
Discrete k =>
(a ~> b) -> ((a ~ b) => r) -> r
withEq a ~> b
f (Free (EMB a) (EMB a)
forall {k :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil :: Free (EMB x :: FREE ds p) (EMB x))

-- | Widen a free arrow into a free category over a larger structure list: 'fold' along 'Embed',
-- so each structural object is rebuilt as itself in the larger category (e.g. the terminal object
-- lowers to the target's terminal object) and generators embed as generators. The
-- @'All' cs ('FREE' ds p)@ constraint is the evidence that every structure in @cs@ is
-- also available in @ds@.
widen
  :: forall ds {k} {cs} {p :: CAT k} (a :: FREE cs p) b
   . (All cs (FREE ds p), Discrete k)
  => a ~> b
  -> Lower (Rep (Embed :: k +-> FREE ds p)) a ~> Lower (Rep (Embed :: k +-> FREE ds p)) b
widen :: forall (ds :: [Kind -> Constraint]) {k :: Kind}
       {cs :: [Kind -> Constraint]} {p :: CAT k} (a :: FREE cs p)
       (b :: FREE cs p).
(All cs (FREE ds p), Discrete k) =>
(a ~> b) -> Lower (Rep Embed) a ~> Lower (Rep Embed) b
widen = forall (cs :: [Kind -> Constraint]) (f :: k +-> FREE ds p)
       (a :: FREE cs p) (b :: FREE cs p).
(All cs (FREE ds p), Representable f) =>
(forall (x :: k) (y :: k).
 (Ob x, Ob y) =>
 p x y -> (f % x) ~> (f % y))
-> (a ~> b) -> Lower f a ~> Lower f b
forall {k :: Kind} {k' :: Kind} {p :: CAT k}
       (cs :: [Kind -> Constraint]) (f :: k +-> k') (a :: FREE cs p)
       (b :: FREE cs p).
(All cs k', Representable f) =>
(forall (x :: k) (y :: k).
 (Ob x, Ob y) =>
 p x y -> (f % x) ~> (f % y))
-> (a ~> b) -> Lower f a ~> Lower f b
fold @cs @(Rep (Embed :: k +-> FREE ds p)) (\p x y
g -> p x y %1 -> Free (EMB x) (EMB y)
forall {k :: Kind} (a :: k) (b :: k) (p :: k -> k -> Kind)
       (cs :: [Kind -> Constraint]).
(Ob a, Ob b) =>
p a b %1 -> Free (EMB a) (EMB b)
emb p x y
g)

-- | The category freely generated from the heteromorphisms of @p@, together with formal
-- structure arrows for each of the classes in @cs@. An object is a shape ('IsFreeOb').
instance CategoryOf (FREE cs p) where
  type (~>) = Free
  type Ob a = IsFreeOb a

instance Promonad (Free :: CAT (FREE cs p)) where
  id :: forall (a :: FREE cs p). Ob a => Free a a
id = Free a a
forall {k :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil
  Free b c
Nil . :: forall (b :: FREE cs p) (c :: FREE cs p) (a :: FREE cs p).
Free b c -> Free a b -> Free a c
. Free a b
g = Free a b
Free a c
g
  Free b c
f . Free a b
Nil = Free b c
Free a c
f
  Emb p a b
p Free b (EMB a)
f . Free a b
g = p a b -> Free a (EMB a) -> Free a (EMB b)
forall {k :: Kind} (c :: k) (a :: k) (p :: k -> k -> Kind)
       (cs :: [Kind -> Constraint]) (i :: FREE cs p).
(Ob c, Ob a) =>
p c a -> Free i (EMB c) -> Free i (EMB a)
Emb p a b
p (Free b (EMB a)
f Free b (EMB a) -> Free a b -> Free a (EMB a)
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FREE cs p) (c :: FREE cs p) (a :: FREE cs p).
Free b c -> Free a b -> Free a c
. Free a b
g)
  St Struct c a c
s Free b a
f . Free a b
g = Struct c a c -> Free a a -> Free a c
forall {k :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT k}
       (c :: Kind -> Constraint) (a :: FREE cs p) (b :: FREE cs p)
       (i :: FREE cs p).
(HasStructure cs p c, Ob a, Ob b) =>
Struct c a b -> Free i a -> Free i b
St Struct c a c
s (Free b a
f Free b a -> Free a b -> Free a a
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FREE cs p) (c :: FREE cs p) (a :: FREE cs p).
Free b c -> Free a b -> Free a c
. Free a b
g)

instance Profunctor (Free :: CAT (FREE cs p)) where
  dimap :: forall (c :: FREE cs p) (a :: FREE cs p) (b :: FREE cs p)
       (d :: FREE cs p).
(c ~> a) -> (b ~> d) -> Free a b -> Free c d
dimap = (c ~> a) -> (b ~> d) -> Free a b -> Free c d
Free c a -> Free b d -> Free a b -> Free c d
forall {k :: Kind} (p :: CAT 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 :: FREE cs p) (b :: FREE cs p) (r :: Kind).
((Ob a, Ob b) => r) -> Free a b -> r
\\ Free a b
Nil = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ Emb p a b
_ Free a (EMB a)
f = r
(Ob a, Ob b) => r
(Ob a, Ob (EMB a)) => r
r ((Ob a, Ob (EMB a)) => r) -> Free a (EMB a) -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FREE cs p) (b :: FREE cs p) (r :: Kind).
((Ob a, Ob b) => r) -> Free a b -> r
\\ Free a (EMB a)
f
  (Ob a, Ob b) => r
r \\ St Struct c a b
_ Free a a
f = r
(Ob a, Ob b) => r
(Ob a, Ob a) => r
r ((Ob a, Ob a) => r) -> Free a a -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FREE cs p) (b :: FREE cs p) (r :: Kind).
((Ob a, Ob b) => r) -> Free a b -> r
\\ Free a a
f