{-# LANGUAGE AllowAmbiguousTypes #-}

-- | The category __freely generated__ by a quiver @p@: an arrow is a finite path of generators
-- ('PCons' onto 'PNil'), and an object is simply a vertex.
--
-- This is "Proarrow.Category.Instance.Free" without structures. With no formal products or
-- exponentials to form, the objects can be the vertices themselves, with 'Ob' inherited from the
-- base kind, so an object of @'PATHS' p@ can be taken apart by whatever that 'Ob' provides. An
-- object of the free structured category cannot, since @Lower@\/@lowerOb@ never yields a value
-- indexed by a shape. An empty structure list does not help: the pattern checker cannot rule out
-- the @HasStructure@ given of @'Proarrow.Category.Instance.Free.St'@, so every consumer would carry
-- an unreachable branch.
--
-- __Equations__ are supported, by 'Rewrite'. Composition only adds an arrow at the outer end of
-- the spine, so each new arrow can be normalised against an already-normal path. With the default
-- 'rewrite' the category is free.
--
-- The base kind must be a category because 'foldPaths' interprets along a functor out of it, and
-- functors are representable profunctors here. Its arrows are never used, so the intended base is
-- a discrete one.
module Proarrow.Category.Instance.Paths where

import Data.Type.Equality ((:~:) (..))
import Prelude (Eq (..), Maybe (..), Show (..), showParen, showString)
import Prelude qualified as P

import Proarrow.Category.Enriched.Thin
  ( AtOb (..)
  , Enumerable (..)
  , Finite (..)
  , FmapWrap
  , Indexed (..)
  , MapWrap
  , withWrapAtLookup
  , wrapFinite
  )
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Profunctor (..)
  , Promonad (..)
  , Show2
  , UN
  , WrappedOb
  , dimapDefault
  , type (+->)
  )
import Proarrow.Profunctor.Representable (Representable (..))

-- | The objects of the free category on @p@: its vertices.
type data PATHS (p :: CAT k) = PTH k

-- | A path of generators, as a right-associated spine, so that the category laws hold
-- definitionally.
type Paths :: CAT (PATHS p)
data Paths a b where
  PNil :: (Ob a) => Paths (PTH a) (PTH a)
  PCons :: (Ob a, Ob b) => p a b -> Paths (i :: PATHS p) (PTH a) -> Paths i (PTH b)

-- | The equations of the generated category, as a rewriting system on paths. 'rewrite' is handed a
-- generator and the already-normalised path it is being composed onto, and returns the normal form
-- of the two together; the default keeps the path as it is, which generates the free category.
--
-- An equation is one clause. For @Secr ⨟ WorksIn = id@, match the junction and drop both arrows:
--
-- > rewrite WorksIn (PCons Secr more) = more
--
-- The whole tail is in scope, so a longer left-hand side can be matched, and recursing on the
-- result renormalises a junction the rewrite has just exposed.
--
-- __Confluence and termination are the caller's to establish.__ Nothing here checks them, and a
-- system that lacks them breaks associativity of composition silently. Two further obligations come
-- with any non-default instance: 'foldPaths' is a functor only for interpretations that respect the
-- equations, and so is any other consumer that matches on generators.
class Rewrite (p :: CAT k) where
  rewrite :: (Ob a, Ob b) => p a b -> Paths (i :: PATHS p) (PTH a) -> Paths i (PTH b)
  rewrite = p a b -> Paths i (PTH a) -> Paths i (PTH b)
forall {k} (a :: k) (b :: k) (p :: k -> k -> Type) (i :: PATHS p).
(Ob a, Ob b) =>
p a b -> Paths i (PTH a) -> Paths i (PTH b)
PCons

-- | Decidable equality of generators, which also has to decide their sources: the object between
-- two arrows of a path is existential, so @'Eq' (p x y)@ alone cannot compare two spines.
-- ('Proarrow.Core.Eq2' does not serve. It is equality of arrows of a fixed category, as
-- 'Proarrow.Limit.Pullback.isMono' wants.)
class EqGen (p :: CAT k) where
  eqGen :: p x b -> p y b -> Maybe (x :~: y)

-- | Structural equality of paths. This is equality of arrows exactly when 'rewrite' is confluent
-- and every path was built through 'emb', 'id' and composition, which keep paths in normal form.
-- The free /structured/ category cannot offer this: there, equality has to be decided by folding
-- both sides into some category that identifies them.
instance (EqGen p) => Eq (Paths (a :: PATHS p) b) where
  Paths a b
PNil == :: Paths a b -> Paths a b -> Bool
== Paths a b
PNil = Bool
P.True
  PCons p a b
q Paths a (PTH a)
f == PCons p a b
q' Paths a (PTH a)
g = case p a b -> p a b -> Maybe (a :~: a)
forall (x :: k) (b :: k) (y :: k).
p x b -> p y b -> Maybe (x :~: y)
forall k (p :: CAT k) (x :: k) (b :: k) (y :: k).
EqGen p =>
p x b -> p y b -> Maybe (x :~: y)
eqGen p a b
q p a b
p a b
q' of
    Just a :~: a
Refl -> Paths a (PTH a)
f Paths a (PTH a) -> Paths a (PTH a) -> Bool
forall a. Eq a => a -> a -> Bool
== Paths a (PTH a)
Paths a (PTH a)
g
    Maybe (a :~: a)
Nothing -> Bool
P.False
  Paths a b
_ == Paths a b
_ = Bool
P.False

instance (Show2 p) => Show (Paths (a :: PATHS p) b) where
  showsPrec :: Int -> Paths a b -> ShowS
showsPrec Int
_ Paths a b
PNil = String -> ShowS
showString String
"id"
  showsPrec Int
d (PCons p a b
q Paths a (PTH a)
PNil) = Int -> p a b -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d p a b
q
  showsPrec Int
d (PCons p a b
q Paths a (PTH a)
f) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
P.> Int
9) (Int -> p a b -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 p a b
q ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. String -> ShowS
showString String
" . " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Int -> Paths a (PTH a) -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 Paths a (PTH a)
f)

-- | How many generators a path is made of. With a non-default 'rewrite' this is a way to see that
-- an equation fired, since a path that reduces comes out shorter.
pathLength :: Paths a b -> P.Int
pathLength :: forall {k} {p :: CAT k} (a :: PATHS p) (b :: PATHS p).
Paths a b -> Int
pathLength Paths a b
PNil = Int
0
pathLength (PCons p a b
_ Paths a (PTH a)
f) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
P.+ Paths a (PTH a) -> Int
forall {k} {p :: CAT k} (a :: PATHS p) (b :: PATHS p).
Paths a b -> Int
pathLength Paths a (PTH a)
f

-- | A single generator, normalised. Named as in "Proarrow.Category.Instance.Free".
emb :: (Ob a, Ob b, Rewrite p) => p a b -> (PTH a :: PATHS p) ~> PTH b
emb :: forall {k} (a :: k) (b :: k) (p :: CAT k).
(Ob a, Ob b, Rewrite p) =>
p a b -> PTH a ~> PTH b
emb p a b
q = p a b -> Paths (PTH a) (PTH a) -> Paths (PTH a) (PTH b)
forall (a :: k) (b :: k) (i :: PATHS p).
(Ob a, Ob b) =>
p a b -> Paths i (PTH a) -> Paths i (PTH b)
forall k (p :: CAT k) (a :: k) (b :: k) (i :: PATHS p).
(Rewrite p, Ob a, Ob b) =>
p a b -> Paths i (PTH a) -> Paths i (PTH b)
rewrite p a b
q Paths (PTH a) (PTH a)
forall {k} {p :: CAT k} (a :: k). Ob a => Paths (PTH a) (PTH a)
PNil

-- | Interpret a path in any category, given an interpretation of the generators: the universal
-- property of the free category. A functor out of @'PATHS' p@ is a map of vertices plus such an
-- interpretation, with nothing to check, since a quiver has no composition to preserve.
--
-- The first argument supplies @'Ob'@ of an image object. It cannot come from @f@ by
-- 'Proarrow.Profunctor.Representable.withObRep': the usual caller is @f@\'s own 'fmap', which
-- would loop on the empty path. For unconstrained objects pass @\\r -> r@.
foldPaths
  :: forall {k} {k'} {p :: CAT k} (f :: PATHS p +-> k') a b
   . (Representable f)
  => (forall x r. (Ob x) => ((Ob (f % PTH x)) => r) -> r)
  -> (forall x y. (Ob x, Ob y) => p x y -> (f % PTH x) ~> (f % PTH y))
  -> (PTH a :: PATHS p) ~> PTH b
  -> (f % PTH a) ~> (f % PTH b)
foldPaths :: forall {k} {k'} {p :: CAT k} (f :: PATHS p +-> k') (a :: k)
       (b :: k).
Representable f =>
(forall (x :: k) r. Ob x => (Ob (f % PTH x) => r) -> r)
-> (forall (x :: k) (y :: k).
    (Ob x, Ob y) =>
    p x y -> (f % PTH x) ~> (f % PTH y))
-> (PTH a ~> PTH b)
-> (f % PTH a) ~> (f % PTH b)
foldPaths forall (x :: k) r. Ob x => (Ob (f % PTH x) => r) -> r
withObF forall (x :: k) (y :: k).
(Ob x, Ob y) =>
p x y -> (f % PTH x) ~> (f % PTH y)
pn = (PTH a ~> PTH b) -> (f % PTH a) ~> (f % PTH b)
forall (x :: k) (y :: k).
(PTH x ~> PTH y) -> (f % PTH x) ~> (f % PTH y)
go
  where
    go :: forall x y. (PTH x :: PATHS p) ~> PTH y -> (f % PTH x) ~> (f % PTH y)
    go :: forall (x :: k) (y :: k).
(PTH x ~> PTH y) -> (f % PTH x) ~> (f % PTH y)
go PTH x ~> PTH y
Paths (PTH x) (PTH y)
PNil = forall (x :: k) r. Ob x => (Ob (f % PTH x) => r) -> r
withObF @x (f % PTH x) ~> (f % PTH x)
Ob (f % PTH x) => (f % PTH x) ~> (f % PTH x)
forall (a :: k'). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
    go (PCons p a b
q Paths (PTH x) (PTH a)
g) = p a y -> (f % PTH a) ~> (f % PTH y)
forall (x :: k) (y :: k).
(Ob x, Ob y) =>
p x y -> (f % PTH x) ~> (f % PTH y)
pn p a y
p a b
q ((f % PTH a) ~> (f % PTH y))
-> ((f % PTH x) ~> (f % PTH a)) -> (f % PTH x) ~> (f % PTH y)
forall (b :: k') (c :: k') (a :: k').
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (PTH x ~> PTH a) -> (f % PTH x) ~> (f % PTH a)
forall (x :: k) (y :: k).
(PTH x ~> PTH y) -> (f % PTH x) ~> (f % PTH y)
go PTH x ~> PTH a
Paths (PTH x) (PTH a)
g

instance (CategoryOf k, Rewrite p) => CategoryOf (PATHS (p :: CAT k)) where
  type (~>) = Paths
  type Ob a = WrappedOb PTH a

-- | Objects are vertices, so a free category has as many of them as its quiver has, however many
-- arrows the paths add (usually unboundedly many). So a free category is 'Finite' without being
-- anywhere near thin or decidable. This buys enumeration of the objects alone. That is enough for
-- @Proarrow.Testing.genSomeFinite@ to derive a schema\'s object palette, and not enough for
-- anything that wants to enumerate arrows.
instance (Indexed k) => Indexed (PATHS (p :: CAT k)) where
  type Index (a :: PATHS p) = Index (UN PTH a)
  type At (PATHS (p :: CAT k)) i = FmapWrap PTH (At k i)

instance (Finite k) => Finite (PATHS (p :: CAT k)) where
  type Objects (PATHS (p :: CAT k)) = MapWrap PTH (Objects k)
  finite :: IndexedList (Objects (PATHS p))
finite = forall {j} {k} (w :: j -> k).
(Finite j, forall (a :: j). KnownIndex a => KnownIndex (w a)) =>
IndexedList (MapWrap w (Objects j))
forall (w :: k -> PATHS p).
(Finite k, forall (a :: k). KnownIndex a => KnownIndex (w a)) =>
IndexedList (MapWrap w (Objects k))
wrapFinite @PTH
  withAtLookup :: forall (i :: Nat) r.
SNat i
-> ((Lookup (Objects (PATHS p)) i ~ At (PATHS p) i) => r) -> r
withAtLookup = forall {j} {k} (w :: j -> k) (i :: Nat) r.
Finite j =>
SNat i
-> ((Lookup (MapWrap w (Objects j)) i ~ FmapWrap w (At j i)) => r)
-> r
forall (w :: k -> PATHS p) (i :: Nat) r.
Finite k =>
SNat i
-> ((Lookup (MapWrap w (Objects k)) i ~ FmapWrap w (At k i)) => r)
-> r
withWrapAtLookup @PTH

instance (Enumerable k, Rewrite p) => Enumerable (PATHS (p :: CAT k)) where
  withIndex :: forall (a :: PATHS p) r. Ob a => (KnownIndex a => r) -> r
withIndex @(PTH a) KnownIndex a => r
r = forall k (a :: k) r.
(Enumerable k, Ob a) =>
(KnownIndex a => r) -> r
withIndex @k @a r
KnownIndex (UN PTH a) => r
KnownIndex a => r
r
  atOb :: forall (i :: Nat). SNat i -> AtOb (PATHS p) (At (PATHS p) i)
atOb SNat i
i = case forall k (i :: Nat). Enumerable k => SNat i -> AtOb k (At k i)
atOb @k SNat i
i of
    AtOb k (At k i)
AtJust -> AtOb (PATHS p) ('Just (PTH a))
AtOb (PATHS p) (At (PATHS p) i)
forall k (a :: k). (Ob a, KnownIndex a) => AtOb k ('Just a)
AtJust
    AtOb k (At k i)
AtNothing -> AtOb (PATHS p) 'Nothing
AtOb (PATHS p) (At (PATHS p) i)
forall k. AtOb k 'Nothing
AtNothing

instance (CategoryOf k, Rewrite p) => Promonad (Paths :: CAT (PATHS (p :: CAT k))) where
  id :: forall (a :: PATHS p). Ob a => Paths a a
id = Paths a a
Paths (PTH (UN PTH a)) (PTH (UN PTH a))
forall {k} {p :: CAT k} (a :: k). Ob a => Paths (PTH a) (PTH a)
PNil
  Paths b c
PNil . :: forall (b :: PATHS p) (c :: PATHS p) (a :: PATHS p).
Paths b c -> Paths a b -> Paths a c
. Paths a b
g = Paths a b
Paths a c
g
  PCons p a b
q Paths b (PTH a)
f . Paths a b
g = p a b -> Paths a (PTH a) -> Paths a (PTH b)
forall (a :: k) (b :: k) (i :: PATHS p).
(Ob a, Ob b) =>
p a b -> Paths i (PTH a) -> Paths i (PTH b)
forall k (p :: CAT k) (a :: k) (b :: k) (i :: PATHS p).
(Rewrite p, Ob a, Ob b) =>
p a b -> Paths i (PTH a) -> Paths i (PTH b)
rewrite p a b
q (Paths b (PTH a)
f Paths b (PTH a) -> Paths a b -> Paths a (PTH a)
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: PATHS p) (c :: PATHS p) (a :: PATHS p).
Paths b c -> Paths a b -> Paths a c
. Paths a b
g)

instance (CategoryOf k, Rewrite p) => Profunctor (Paths :: CAT (PATHS (p :: CAT k))) where
  dimap :: forall (c :: PATHS p) (a :: PATHS p) (b :: PATHS p) (d :: PATHS p).
(c ~> a) -> (b ~> d) -> Paths a b -> Paths c d
dimap = (c ~> a) -> (b ~> d) -> Paths a b -> Paths c d
Paths c a -> Paths b d -> Paths a b -> Paths c d
forall {k} (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 :: PATHS p) (b :: PATHS p) r.
((Ob a, Ob b) => r) -> Paths a b -> r
\\ Paths a b
PNil = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ PCons p a b
_ Paths a (PTH a)
f = r
(Ob a, Ob b) => r
(Ob a, Ob (PTH a)) => r
r ((Ob a, Ob (PTH a)) => r) -> Paths a (PTH a) -> 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 :: PATHS p) (b :: PATHS p) r.
((Ob a, Ob b) => r) -> Paths a b -> r
\\ Paths a (PTH a)
f