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

-- | Composition of thin profunctors. In general the arrows of a composite @p ':.:' q@ are an
-- existential over the objects of the middle category, which a 'Constraint' cannot express. This
-- module dispatches on the shape of the legs, so that the single 'ThinProfunctor' instance for
-- ':.:' never overlaps with anything: a representable leg pins the middle object down, and
-- otherwise the middle category is searched ('Search'), which needs it to be 'Enumerable' and both
-- legs to be 'DecidableProfunctor's. Composites are themselves decidable, so searches nest.
module Proarrow.Category.Enriched.Thin.Composition where

import Data.Kind (Constraint, Type)
import Data.Type.Nat (Nat (..), SNat (..), SNatI, snat)
import Prelude (type (~))

import Proarrow.Category.Enriched (Enriched, EnrichedProfunctor (..), HomObj)
import Proarrow.Category.Enriched.Quantale (MinIs (..), Quantale (..), checkedArrow, splitUnit)
import Proarrow.Category.Enriched.Thin
  ( Decidable
  , DecidableProfunctor (..)
  , Decision (..)
  , Enumerable (..)
  , Finite (..)
  , IndexedList (..)
  , Length
  , Member (..)
  , Thin
  , ThinProfunctor (..)
  , mapDecision
  , member
  )
import Proarrow.Category.Instance.Bool (BOOL (..), Booleans (..))
import Proarrow.Category.Instance.Cost (COST)
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Colimit.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Core (CategoryOf (..), Hom, Kind, Profunctor (..), Promonad (..), obj, type (+->))
import Proarrow.Core qualified as P
import Proarrow.Functor (FunctorForRep (..), withMappedOb)
import Proarrow.Object (pattern Objs)
import Proarrow.Profunctor.Corepresentable (Corep (..), Corepresentable (..), withObCorep)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Representable (CorepStar (..), Rep (..), RepCostar (..), Representable (..), withObRep)

-- | How a composite @p ':.:' q@ of thin profunctors decides its arrows. In general
-- @'HasArrow' (p :.: q) a c@ is an /existential/ over the objects @b@ of the middle category
-- (the join @⋁_b p(a,b) ∧ q(b,c)@ in the enriching @Bool@), which a 'Constraint' cannot express.
-- But when the left leg is corepresented (@f a ≤ b@, a companion) or the right leg represented
-- (@b ≤ g c@, a conjoint) the middle object is determined and the existential collapses to a
-- substitution: @q (f a) c@, respectively @p a (g c)@. The strategy is chosen by the closed
-- family 'ThinCompStrategy' from the shape of the legs, so that the one 'ThinProfunctor'
-- instance for ':.:' never overlaps with anything; a composite of two non-representable legs
-- falls back to 'BySearch', which enumerates the middle category and decides both legs at each
-- object ('Search'). ('Proarrow.Profunctor.Instance.Star.Star' and
-- 'Proarrow.Profunctor.Instance.Costar.Costar' have the same two shapes, but functors between thin
-- kinds are written as 'FunctorForRep's here, so 'Rep'\/'Corep' cover them.)
type data ThinComp = ByLeft | ByRight | BySearch

type ThinCompStrategy :: forall {i} {j} {k}. (j +-> k) -> (i +-> j) -> ThinComp
type family ThinCompStrategy p q where
  ThinCompStrategy (RepCostar p) q = ByLeft
  ThinCompStrategy (Corep f) q = ByLeft
  ThinCompStrategy p (Rep g) = ByRight
  ThinCompStrategy p (CorepStar q) = ByRight
  ThinCompStrategy p q = BySearch

type ComposeThin :: forall {i} {j} {k}. ThinComp -> (j +-> k) -> (i +-> j) -> Constraint
class (ThinProfunctor p, ThinProfunctor q) => ComposeThin s (p :: j +-> k) (q :: i +-> j) where
  type HasArrowComp s p q (a :: k) (c :: i) :: Constraint
  arrComp :: (Ob (a :: k), Ob (c :: i), HasArrowComp s p q a c) => (p :.: q) a c
  withArrComp :: (p :.: q) a c -> ((HasArrowComp s p q a c, Ob a, Ob c) => r) -> r

-- | A corepresented left leg forces the middle object down to @p % a@.
instance (Representable p, Thin j, ThinProfunctor q) => ComposeThin ByLeft (RepCostar p :: j +-> k) (q :: i +-> j) where
  type HasArrowComp ByLeft (RepCostar p) q a c = HasArrow q (p % a) c
  arrComp :: forall (a :: k) (c :: i).
(Ob a, Ob c, HasArrowComp ByLeft (RepCostar p) q a c) =>
(:.:) (RepCostar p) q a c
arrComp @a @c = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: k +-> j) (a :: k) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @p @a (((p % a) ~> (p % a)) -> RepCostar p a (p % a)
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar (p % a) ~> (p % a)
forall (a :: j). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id RepCostar p a (p % a) -> q (p % a) c -> (:.:) (RepCostar p) q a c
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
forall (p :: i +-> j) (a :: j) (b :: i).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr @q @(p % a) @c)
  withArrComp :: forall (a :: k) (c :: i) r.
(:.:) (RepCostar p) q a c
-> ((HasArrowComp ByLeft (RepCostar p) q a c, Ob a, Ob c) => r)
-> r
withArrComp (RepCostar (p % a) ~> b
f :.: q b c
q) (HasArrowComp ByLeft (RepCostar p) q a c, Ob a, Ob c) => r
r = q (p % a) c -> ((HasArrow q (p % a) c, Ob (p % a), Ob c) => r) -> r
forall (a :: j) (b :: i) r.
q a b -> ((HasArrow q a b, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr (((p % a) ~> b) -> q b c -> q (p % a) c
forall (c :: j) (a :: j) (b :: i). (c ~> a) -> q a b -> q c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
P.lmap (p % a) ~> b
f q b c
q) r
(HasArrow q (p % a) c, Ob (p % a), Ob c) => r
(HasArrowComp ByLeft (RepCostar p) q a c, Ob a, Ob c) => r
r

instance (FunctorForRep f, Thin j, ThinProfunctor q) => ComposeThin ByLeft (Corep f :: j +-> k) (q :: i +-> j) where
  type HasArrowComp ByLeft (Corep f) q a c = HasArrow q (f @ a) c
  arrComp :: forall (a :: k) (c :: i).
(Ob a, Ob c, HasArrowComp ByLeft (Corep f) q a c) =>
(:.:) (Corep f) q a c
arrComp @a @c = forall {j} {k} (f :: j +-> k) (a :: j) r.
(FunctorForRep f, Ob a) =>
(Ob (f @ a) => r) -> r
forall (f :: k +-> j) (a :: k) r.
(FunctorForRep f, Ob a) =>
(Ob (f @ a) => r) -> r
withMappedOb @f @a (((f @ a) ~> (f @ a)) -> Corep f a (f @ a)
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep (f @ a) ~> (f @ a)
forall (a :: j). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id Corep f a (f @ a) -> q (f @ a) c -> (:.:) (Corep f) q a c
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
forall (p :: i +-> j) (a :: j) (b :: i).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr @q @(f @ a) @c)
  withArrComp :: forall (a :: k) (c :: i) r.
(:.:) (Corep f) q a c
-> ((HasArrowComp ByLeft (Corep f) q a c, Ob a, Ob c) => r) -> r
withArrComp (Corep (f @ a) ~> b
f :.: q b c
q) (HasArrowComp ByLeft (Corep f) q a c, Ob a, Ob c) => r
r = q (f @ a) c -> ((HasArrow q (f @ a) c, Ob (f @ a), Ob c) => r) -> r
forall (a :: j) (b :: i) r.
q a b -> ((HasArrow q a b, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr (((f @ a) ~> b) -> q b c -> q (f @ a) c
forall (c :: j) (a :: j) (b :: i). (c ~> a) -> q a b -> q c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
P.lmap (f @ a) ~> b
f q b c
q) r
(HasArrow q (f @ a) c, Ob (f @ a), Ob c) => r
(HasArrowComp ByLeft (Corep f) q a c, Ob a, Ob c) => r
r

-- | A represented right leg forces the middle object up to @g @ c@.
instance (ThinProfunctor p, FunctorForRep g, Thin j) => ComposeThin ByRight (p :: j +-> k) (Rep g :: i +-> j) where
  type HasArrowComp ByRight p (Rep g) a c = HasArrow p a (g @ c)
  arrComp :: forall (a :: k) (c :: i).
(Ob a, Ob c, HasArrowComp ByRight p (Rep g) a c) =>
(:.:) p (Rep g) a c
arrComp @a @c = forall {j} {k} (f :: j +-> k) (a :: j) r.
(FunctorForRep f, Ob a) =>
(Ob (f @ a) => r) -> r
forall (f :: i +-> j) (a :: i) r.
(FunctorForRep f, Ob a) =>
(Ob (f @ a) => r) -> r
withMappedOb @g @c (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
forall (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr @p @a @(g @ c) p a (g @ c) -> Rep g (g @ c) c -> (:.:) p (Rep g) a c
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ((g @ c) ~> (g @ c)) -> Rep g (g @ c) c
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (g @ c) ~> (g @ c)
forall (a :: j). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id)
  withArrComp :: forall (a :: k) (c :: i) r.
(:.:) p (Rep g) a c
-> ((HasArrowComp ByRight p (Rep g) a c, Ob a, Ob c) => r) -> r
withArrComp (p a b
p :.: Rep b ~> (g @ c)
g) (HasArrowComp ByRight p (Rep g) a c, Ob a, Ob c) => r
r = p a (g @ c) -> ((HasArrow p a (g @ c), Ob a, Ob (g @ c)) => r) -> r
forall (a :: k) (b :: j) r.
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr ((b ~> (g @ c)) -> p a b -> p a (g @ c)
forall (b :: j) (d :: j) (a :: k). (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
P.rmap b ~> (g @ c)
g p a b
p) r
(HasArrow p a (g @ c), Ob a, Ob (g @ c)) => r
(HasArrowComp ByRight p (Rep g) a c, Ob a, Ob c) => r
r

instance (ThinProfunctor p, Corepresentable q, Thin j) => ComposeThin ByRight (p :: j +-> k) (CorepStar q :: i +-> j) where
  type HasArrowComp ByRight p (CorepStar q) a c = HasArrow p a (q %% c)
  arrComp :: forall (a :: k) (c :: i).
(Ob a, Ob c, HasArrowComp ByRight p (CorepStar q) a c) =>
(:.:) p (CorepStar q) a c
arrComp @a @c = forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: j +-> i) (a :: i) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withObCorep @q @c (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
forall (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr @p @a @(q %% c) p a (q %% c) -> CorepStar q (q %% c) c -> (:.:) p (CorepStar q) a c
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ((q %% c) ~> (q %% c)) -> CorepStar q (q %% c) c
forall {j} {k} (b :: j) (a :: k) (p :: k +-> j).
Ob b =>
(a ~> (p %% b)) -> CorepStar p a b
CorepStar (q %% c) ~> (q %% c)
forall (a :: j). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id)
  withArrComp :: forall (a :: k) (c :: i) r.
(:.:) p (CorepStar q) a c
-> ((HasArrowComp ByRight p (CorepStar q) a c, Ob a, Ob c) => r)
-> r
withArrComp (p a b
p :.: CorepStar b ~> (q %% c)
g) (HasArrowComp ByRight p (CorepStar q) a c, Ob a, Ob c) => r
r = p a (q %% c)
-> ((HasArrow p a (q %% c), Ob a, Ob (q %% c)) => r) -> r
forall (a :: k) (b :: j) r.
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr ((b ~> (q %% c)) -> p a b -> p a (q %% c)
forall (b :: j) (d :: j) (a :: k). (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
P.rmap b ~> (q %% c)
g p a b
p) r
(HasArrow p a (q %% c), Ob a, Ob (q %% c)) => r
(HasArrowComp ByRight p (CorepStar q) a c, Ob a, Ob c) => r
r

instance (ComposeThin (ThinCompStrategy p q) p q) => ThinProfunctor (p :.: q) where
  type HasArrow (p :.: q) a c = HasArrowComp (ThinCompStrategy p q) p q a c
  arr :: forall (a :: k) (b :: j).
(Ob a, Ob b, HasArrow (p :.: q) a b) =>
(:.:) p q a b
arr = forall {i} {j} {k} (s :: ThinComp) (p :: j +-> k) (q :: i +-> j)
       (a :: k) (c :: i).
(ComposeThin s p q, Ob a, Ob c, HasArrowComp s p q a c) =>
(:.:) p q a c
forall (s :: ThinComp) (p :: j +-> k) (q :: j +-> j) (a :: k)
       (c :: j).
(ComposeThin s p q, Ob a, Ob c, HasArrowComp s p q a c) =>
(:.:) p q a c
arrComp @(ThinCompStrategy p q)
  withArr :: forall (a :: k) (b :: j) r.
(:.:) p q a b -> ((HasArrow (p :.: q) a b, Ob a, Ob b) => r) -> r
withArr = forall {i} {j} {k} (s :: ThinComp) (p :: j +-> k) (q :: i +-> j)
       (a :: k) (c :: i) r.
ComposeThin s p q =>
(:.:) p q a c -> ((HasArrowComp s p q a c, Ob a, Ob c) => r) -> r
forall (s :: ThinComp) (p :: j +-> k) (q :: j +-> j) (a :: k)
       (c :: j) r.
ComposeThin s p q =>
(:.:) p q a c -> ((HasArrowComp s p q a c, Ob a, Ob c) => r) -> r
withArrComp @(ThinCompStrategy p q)

-- | The join @⋁_b p(a,b) ⊗ w_b@ of an edge out of @a@ with whatever the vector holds for where
-- that edge lands: one row of the matrix of @p@ against a vector, over the given middle objects.
-- The objects and the vector are walked in step, so @ws@ is always the vector cut down to @bs@.
--
-- This is the module's one join. Composing two profunctors multiplies by a column read off the
-- right-hand one ('MatMul'); the closure multiplies by the previous iterate ('Walks'), which is
-- what lets that iterate be computed once instead of once per pair.
type MatVec :: forall {j} {k}. forall (v :: Kind) -> [j] -> [v] -> (j +-> k) -> k -> v
type family MatVec v bs ws p a where
  MatVec v '[] ws p a = InitialObject
  MatVec v (b ': bs) (w ': ws) p a = (ProObj v p a b ** w) || MatVec v bs ws p a

-- | One column of the matrix of an enriched profunctor: its hom-objects into @c@, over the given
-- objects.
type MatCol :: forall {i} {j}. forall (v :: Kind) -> [j] -> (i +-> j) -> i -> [v]
type family MatCol v bs q c where
  MatCol v '[] q c = '[]
  MatCol v (b ': bs) q c = ProObj v q b c ': MatCol v bs q c

-- | Matrix multiplication over a list of middle objects, @⋁_b p(a,b) ⊗ q(b,c)@: the hom-object of
-- the composite of two enriched profunctors when the middle category is enumerable. The type-level
-- twin of "Proarrow.Category.Instance.FinRel".
type MatMul :: forall {i} {j} {k}. forall (v :: Kind) -> [j] -> (j +-> k) -> (i +-> j) -> k -> i -> v
type MatMul v bs p q a c = MatVec v bs (MatCol v bs q c) p a

-- | The arrows of a composite by search: is there an object @b@ among @bs@ with both @p a b@ and
-- @q b c@? Over the full object list this is the join @⋁_b p(a,b) ∧ q(b,c)@, which is 'MatMul' in
-- the enriching 'BOOL'.
type Search :: forall {i} {j} {k}. [j] -> (j +-> k) -> (i +-> j) -> k -> i -> BOOL
type Search bs p q a c = MatMul BOOL bs p q a c

-- | Neither leg representable: search the middle category for an object that both legs accept.
instance
  (DecidableProfunctor p, DecidableProfunctor q, Enumerable j)
  => ComposeThin BySearch (p :: j +-> k) (q :: i +-> j)
  where
  type HasArrowComp BySearch (p :: j +-> k) q a c = Search (Objects j) p q a c ~ TRU
  arrComp :: forall (a :: k) (c :: i).
(Ob a, Ob c, HasArrowComp BySearch p q a c) =>
(:.:) p q a c
arrComp @a @c = case forall {i} {j} {k} (p :: j +-> k) (q :: i +-> j) (a :: k) (c :: i)
       (bs :: [j]).
(DecidableProfunctor p, DecidableProfunctor q, Enumerable j, Ob a,
 Ob c) =>
IndexedList bs -> Decision (p :.: q) a c (Search bs p q a c)
forall (p :: j +-> k) (q :: i +-> j) (a :: k) (c :: i) (bs :: [j]).
(DecidableProfunctor p, DecidableProfunctor q, Enumerable j, Ob a,
 Ob c) =>
IndexedList bs -> Decision (p :.: q) a c (Search bs p q a c)
search @p @q @a @c (forall k. Finite k => IndexedList (Objects k)
finite @j) of Yes (:.:) p q a c
x -> (:.:) p q a c
x
  withArrComp :: forall (a :: k) (c :: i) r.
(:.:) p q a c
-> ((HasArrowComp BySearch p q a c, Ob a, Ob c) => r) -> r
withArrComp (p a b
p :.: q b c
q) (HasArrowComp BySearch p q a c, Ob a, Ob c) => r
r = p a b
-> q b c
-> ((Search (Objects j) p q a c ~ 'TRU, Ob a, Ob c) => r)
-> r
forall {i} {j} {k} (p :: j +-> k) (q :: i +-> j) (a :: k) (b :: j)
       (c :: i) r.
(DecidableProfunctor p, DecidableProfunctor q, Enumerable j) =>
p a b
-> q b c
-> ((Search (Objects j) p q a c ~ 'TRU, Ob a, Ob c) => r)
-> r
found p a b
p q b c
q r
(Search (Objects j) p q a c ~ 'TRU, Ob a, Ob c) => r
(HasArrowComp BySearch p q a c, Ob a, Ob c) => r
r

-- | Walk the object list deciding both legs at each object; a hit is the composite, and a miss
-- reduces the search to the tail of the list.
search
  :: forall {i} {j} {k} (p :: j +-> k) (q :: i +-> j) (a :: k) (c :: i) (bs :: [j])
   . (DecidableProfunctor p, DecidableProfunctor q, Enumerable j, Ob a, Ob c)
  => IndexedList bs -> Decision (p :.: q) a c (Search bs p q a c)
search :: forall {i} {j} {k} (p :: j +-> k) (q :: i +-> j) (a :: k) (c :: i)
       (bs :: [j]).
(DecidableProfunctor p, DecidableProfunctor q, Enumerable j, Ob a,
 Ob c) =>
IndexedList bs -> Decision (p :.: q) a c (Search bs p q a c)
search IndexedList bs
FNil = Decision (p :.: q) a c 'FLS
Decision (p :.: q) a c (MatVec BOOL bs (MatCol BOOL bs q c) p a)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Decision p a b 'FLS
No
search (FCons @b IndexedList as1
bs) = forall k (a :: k) r.
(Enumerable k, KnownIndex a) =>
(Ob a => r) -> r
withOb @j @b case (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @p @a @b, forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: i +-> j) (a :: j) (b :: i).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @q @b @c) of
  (Yes p a a
x, Yes q a c
y) -> (:.:) p q a c -> Decision (p :.: q) a c 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Yes (p a a
x p a a -> q a c -> (:.:) p q a c
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q a c
y)
  (Decision p a a (Holds p a a)
No, Decision q a c (Holds q a c)
_) -> forall {i} {j} {k} (p :: j +-> k) (q :: i +-> j) (a :: k) (c :: i)
       (bs :: [j]).
(DecidableProfunctor p, DecidableProfunctor q, Enumerable j, Ob a,
 Ob c) =>
IndexedList bs -> Decision (p :.: q) a c (Search bs p q a c)
forall (p :: j +-> k) (q :: i +-> j) (a :: k) (c :: i) (bs :: [j]).
(DecidableProfunctor p, DecidableProfunctor q, Enumerable j, Ob a,
 Ob c) =>
IndexedList bs -> Decision (p :.: q) a c (Search bs p q a c)
search @p @q @a @c IndexedList as1
bs
  (Yes p a a
_, Decision q a c (Holds q a c)
No) -> forall {i} {j} {k} (p :: j +-> k) (q :: i +-> j) (a :: k) (c :: i)
       (bs :: [j]).
(DecidableProfunctor p, DecidableProfunctor q, Enumerable j, Ob a,
 Ob c) =>
IndexedList bs -> Decision (p :.: q) a c (Search bs p q a c)
forall (p :: j +-> k) (q :: i +-> j) (a :: k) (c :: i) (bs :: [j]).
(DecidableProfunctor p, DecidableProfunctor q, Enumerable j, Ob a,
 Ob c) =>
IndexedList bs -> Decision (p :.: q) a c (Search bs p q a c)
search @p @q @a @c IndexedList as1
bs

-- | An actual composite proves the search succeeds: locate its middle object in the list, then at
-- that position both legs hold and the disjunction is 'TRU' whatever the rest of the list says.
found
  :: forall {i} {j} {k} (p :: j +-> k) (q :: i +-> j) (a :: k) (b :: j) (c :: i) r
   . (DecidableProfunctor p, DecidableProfunctor q, Enumerable j)
  => p a b -> q b c -> ((Search (Objects j) p q a c ~ TRU, Ob a, Ob c) => r) -> r
found :: forall {i} {j} {k} (p :: j +-> k) (q :: i +-> j) (a :: k) (b :: j)
       (c :: i) r.
(DecidableProfunctor p, DecidableProfunctor q, Enumerable j) =>
p a b
-> q b c
-> ((Search (Objects j) p q a c ~ 'TRU, Ob a, Ob c) => r)
-> r
found p a b
p q b c
q (Search (Objects j) p q a c ~ 'TRU, Ob a, Ob c) => r
r = p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall (a :: k) (b :: j) r.
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds p a b
p (q b c -> ((Holds q b c ~ 'TRU, Ob b, Ob c) => r) -> r
forall (a :: j) (b :: i) r.
q a b -> ((Holds q a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds q b c
q (Member b (Objects j)
-> ((Search (Objects j) p q a c ~ 'TRU) => r) -> r
forall (bs :: [j]).
(Holds p a b ~ 'TRU, Holds q b c ~ 'TRU) =>
Member b bs -> ((Search bs p q a c ~ 'TRU) => r) -> r
go (forall (a :: j). (Enumerable j, Ob a) => Member a (Objects j)
forall {k} (a :: k). (Enumerable k, Ob a) => Member a (Objects k)
member @b) r
(Search (Objects j) p q a c ~ 'TRU) => r
(Search (Objects j) p q a c ~ 'TRU, Ob a, Ob c) => r
r))
  where
    go
      :: forall bs
       . (Holds p a b ~ TRU, Holds q b c ~ TRU)
      => Member b bs -> ((Search bs p q a c ~ TRU) => r) -> r
    go :: forall (bs :: [j]).
(Holds p a b ~ 'TRU, Holds q b c ~ 'TRU) =>
Member b bs -> ((Search bs p q a c ~ 'TRU) => r) -> r
go Member b bs
Here (Search bs p q a c ~ 'TRU) => r
r' = r
(Search bs p q a c ~ 'TRU) => r
r'
    go (There Member b as1
m) (Search bs p q a c ~ 'TRU) => r
r' = Member b as1 -> ((Search as1 p q a c ~ 'TRU) => r) -> r
forall (bs :: [j]).
(Holds p a b ~ 'TRU, Holds q b c ~ 'TRU) =>
Member b bs -> ((Search bs p q a c ~ 'TRU) => r) -> r
go Member b as1
m r
(Search bs p q a c ~ 'TRU) => r
(Search as1 p q a c ~ 'TRU) => r
r'

-- | Whether a composite decides its arrows, by the same strategy as 'ComposeThin': a representable
-- leg is substituted away and the other leg decided, a search is decided by running it. This is
-- what makes composites decidable in turn, so that searches can nest.
type DecideComp :: forall {i} {j} {k}. ThinComp -> (j +-> k) -> (i +-> j) -> Constraint
class (ComposeThin s p q) => DecideComp s (p :: j +-> k) (q :: i +-> j) where
  type HoldsComp s p q (a :: k) (c :: i) :: BOOL
  decideComp :: (Ob (a :: k), Ob (c :: i)) => Decision (p :.: q) a c (HoldsComp s p q a c)
  toHoldsComp :: (p :.: q) a c -> ((HoldsComp s p q a c ~ TRU, Ob a, Ob c) => r) -> r

instance
  (Representable p, Thin j, DecidableProfunctor q)
  => DecideComp ByLeft (RepCostar p :: j +-> k) (q :: i +-> j)
  where
  type HoldsComp ByLeft (RepCostar p) q a c = Holds q (p % a) c
  decideComp :: forall (a :: k) (c :: i).
(Ob a, Ob c) =>
Decision
  (RepCostar p :.: q) a c (HoldsComp ByLeft (RepCostar p) q a c)
decideComp @a @c = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: k +-> j) (a :: k) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @p @a ((q (p % a) c -> (:.:) (RepCostar p) q a c)
-> Decision q (p % a) c (Holds q (p % a) c)
-> Decision (RepCostar p :.: q) a c (Holds q (p % a) c)
forall {k1} {j1} {k2} {j2} (p :: k1 -> j1 -> Type) (a :: k1)
       (b :: j1) (q :: k2 -> j2 -> Type) (c :: k2) (d :: j2) (h :: BOOL).
(p a b -> q c d) -> Decision p a b h -> Decision q c d h
mapDecision (((p % a) ~> (p % a)) -> RepCostar p a (p % a)
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar (p % a) ~> (p % a)
forall (a :: j). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id RepCostar p a (p % a) -> q (p % a) c -> (:.:) (RepCostar p) q a c
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.:) (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: i +-> j) (a :: j) (b :: i).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @q @(p % a) @c))
  toHoldsComp :: forall (a :: k) (c :: i) r.
(:.:) (RepCostar p) q a c
-> ((HoldsComp ByLeft (RepCostar p) q a c ~ 'TRU, Ob a, Ob c) => r)
-> r
toHoldsComp (RepCostar (p % a) ~> b
f :.: q b c
q) (HoldsComp ByLeft (RepCostar p) q a c ~ 'TRU, Ob a, Ob c) => r
r = q (p % a) c
-> ((Holds q (p % a) c ~ 'TRU, Ob (p % a), Ob c) => r) -> r
forall (a :: j) (b :: i) r.
q a b -> ((Holds q a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds (((p % a) ~> b) -> q b c -> q (p % a) c
forall (c :: j) (a :: j) (b :: i). (c ~> a) -> q a b -> q c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
P.lmap (p % a) ~> b
f q b c
q) r
(Holds q (p % a) c ~ 'TRU, Ob (p % a), Ob c) => r
(HoldsComp ByLeft (RepCostar p) q a c ~ 'TRU, Ob a, Ob c) => r
r

instance
  (FunctorForRep f, Thin j, DecidableProfunctor q)
  => DecideComp ByLeft (Corep f :: j +-> k) (q :: i +-> j)
  where
  type HoldsComp ByLeft (Corep f) q a c = Holds q (f @ a) c
  decideComp :: forall (a :: k) (c :: i).
(Ob a, Ob c) =>
Decision (Corep f :.: q) a c (HoldsComp ByLeft (Corep f) q a c)
decideComp @a @c = forall {j} {k} (f :: j +-> k) (a :: j) r.
(FunctorForRep f, Ob a) =>
(Ob (f @ a) => r) -> r
forall (f :: k +-> j) (a :: k) r.
(FunctorForRep f, Ob a) =>
(Ob (f @ a) => r) -> r
withMappedOb @f @a ((q (f @ a) c -> (:.:) (Corep f) q a c)
-> Decision q (f @ a) c (Holds q (f @ a) c)
-> Decision (Corep f :.: q) a c (Holds q (f @ a) c)
forall {k1} {j1} {k2} {j2} (p :: k1 -> j1 -> Type) (a :: k1)
       (b :: j1) (q :: k2 -> j2 -> Type) (c :: k2) (d :: j2) (h :: BOOL).
(p a b -> q c d) -> Decision p a b h -> Decision q c d h
mapDecision (((f @ a) ~> (f @ a)) -> Corep f a (f @ a)
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep (f @ a) ~> (f @ a)
forall (a :: j). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id Corep f a (f @ a) -> q (f @ a) c -> (:.:) (Corep f) q a c
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.:) (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: i +-> j) (a :: j) (b :: i).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @q @(f @ a) @c))
  toHoldsComp :: forall (a :: k) (c :: i) r.
(:.:) (Corep f) q a c
-> ((HoldsComp ByLeft (Corep f) q a c ~ 'TRU, Ob a, Ob c) => r)
-> r
toHoldsComp (Corep (f @ a) ~> b
f :.: q b c
q) (HoldsComp ByLeft (Corep f) q a c ~ 'TRU, Ob a, Ob c) => r
r = q (f @ a) c
-> ((Holds q (f @ a) c ~ 'TRU, Ob (f @ a), Ob c) => r) -> r
forall (a :: j) (b :: i) r.
q a b -> ((Holds q a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds (((f @ a) ~> b) -> q b c -> q (f @ a) c
forall (c :: j) (a :: j) (b :: i). (c ~> a) -> q a b -> q c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
P.lmap (f @ a) ~> b
f q b c
q) r
(Holds q (f @ a) c ~ 'TRU, Ob (f @ a), Ob c) => r
(HoldsComp ByLeft (Corep f) q a c ~ 'TRU, Ob a, Ob c) => r
r

instance
  (DecidableProfunctor p, FunctorForRep g, Thin j)
  => DecideComp ByRight (p :: j +-> k) (Rep g :: i +-> j)
  where
  type HoldsComp ByRight p (Rep g) a c = Holds p a (g @ c)
  decideComp :: forall (a :: k) (c :: i).
(Ob a, Ob c) =>
Decision (p :.: Rep g) a c (HoldsComp ByRight p (Rep g) a c)
decideComp @a @c = forall {j} {k} (f :: j +-> k) (a :: j) r.
(FunctorForRep f, Ob a) =>
(Ob (f @ a) => r) -> r
forall (f :: i +-> j) (a :: i) r.
(FunctorForRep f, Ob a) =>
(Ob (f @ a) => r) -> r
withMappedOb @g @c ((p a (g @ c) -> (:.:) p (Rep g) a c)
-> Decision p a (g @ c) (Holds p a (g @ c))
-> Decision (p :.: Rep g) a c (Holds p a (g @ c))
forall {k1} {j1} {k2} {j2} (p :: k1 -> j1 -> Type) (a :: k1)
       (b :: j1) (q :: k2 -> j2 -> Type) (c :: k2) (d :: j2) (h :: BOOL).
(p a b -> q c d) -> Decision p a b h -> Decision q c d h
mapDecision (p a (g @ c) -> Rep g (g @ c) c -> (:.:) p (Rep g) a c
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ((g @ c) ~> (g @ c)) -> Rep g (g @ c) c
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (g @ c) ~> (g @ c)
forall (a :: j). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id) (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @p @a @(g @ c)))
  toHoldsComp :: forall (a :: k) (c :: i) r.
(:.:) p (Rep g) a c
-> ((HoldsComp ByRight p (Rep g) a c ~ 'TRU, Ob a, Ob c) => r) -> r
toHoldsComp (p a b
p :.: Rep b ~> (g @ c)
g) (HoldsComp ByRight p (Rep g) a c ~ 'TRU, Ob a, Ob c) => r
r = p a (g @ c)
-> ((Holds p a (g @ c) ~ 'TRU, Ob a, Ob (g @ c)) => r) -> r
forall (a :: k) (b :: j) r.
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds ((b ~> (g @ c)) -> p a b -> p a (g @ c)
forall (b :: j) (d :: j) (a :: k). (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
P.rmap b ~> (g @ c)
g p a b
p) r
(Holds p a (g @ c) ~ 'TRU, Ob a, Ob (g @ c)) => r
(HoldsComp ByRight p (Rep g) a c ~ 'TRU, Ob a, Ob c) => r
r

instance
  (DecidableProfunctor p, Corepresentable q, Thin j)
  => DecideComp ByRight (p :: j +-> k) (CorepStar q :: i +-> j)
  where
  type HoldsComp ByRight p (CorepStar q) a c = Holds p a (q %% c)
  decideComp :: forall (a :: k) (c :: i).
(Ob a, Ob c) =>
Decision
  (p :.: CorepStar q) a c (HoldsComp ByRight p (CorepStar q) a c)
decideComp @a @c = forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: j +-> i) (a :: i) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withObCorep @q @c ((p a (q %% c) -> (:.:) p (CorepStar q) a c)
-> Decision p a (q %% c) (Holds p a (q %% c))
-> Decision (p :.: CorepStar q) a c (Holds p a (q %% c))
forall {k1} {j1} {k2} {j2} (p :: k1 -> j1 -> Type) (a :: k1)
       (b :: j1) (q :: k2 -> j2 -> Type) (c :: k2) (d :: j2) (h :: BOOL).
(p a b -> q c d) -> Decision p a b h -> Decision q c d h
mapDecision (p a (q %% c) -> CorepStar q (q %% c) c -> (:.:) p (CorepStar q) a c
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ((q %% c) ~> (q %% c)) -> CorepStar q (q %% c) c
forall {j} {k} (b :: j) (a :: k) (p :: k +-> j).
Ob b =>
(a ~> (p %% b)) -> CorepStar p a b
CorepStar (q %% c) ~> (q %% c)
forall (a :: j). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id) (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @p @a @(q %% c)))
  toHoldsComp :: forall (a :: k) (c :: i) r.
(:.:) p (CorepStar q) a c
-> ((HoldsComp ByRight p (CorepStar q) a c ~ 'TRU, Ob a, Ob c) =>
    r)
-> r
toHoldsComp (p a b
p :.: CorepStar b ~> (q %% c)
g) (HoldsComp ByRight p (CorepStar q) a c ~ 'TRU, Ob a, Ob c) => r
r = p a (q %% c)
-> ((Holds p a (q %% c) ~ 'TRU, Ob a, Ob (q %% c)) => r) -> r
forall (a :: k) (b :: j) r.
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds ((b ~> (q %% c)) -> p a b -> p a (q %% c)
forall (b :: j) (d :: j) (a :: k). (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
P.rmap b ~> (q %% c)
g p a b
p) r
(Holds p a (q %% c) ~ 'TRU, Ob a, Ob (q %% c)) => r
(HoldsComp ByRight p (CorepStar q) a c ~ 'TRU, Ob a, Ob c) => r
r

instance
  (DecidableProfunctor p, DecidableProfunctor q, Enumerable j)
  => DecideComp BySearch (p :: j +-> k) (q :: i +-> j)
  where
  type HoldsComp BySearch (p :: j +-> k) q a c = Search (Objects j) p q a c
  decideComp :: forall (a :: k) (c :: i).
(Ob a, Ob c) =>
Decision (p :.: q) a c (HoldsComp BySearch p q a c)
decideComp @a @c = forall {i} {j} {k} (p :: j +-> k) (q :: i +-> j) (a :: k) (c :: i)
       (bs :: [j]).
(DecidableProfunctor p, DecidableProfunctor q, Enumerable j, Ob a,
 Ob c) =>
IndexedList bs -> Decision (p :.: q) a c (Search bs p q a c)
forall (p :: j +-> k) (q :: i +-> j) (a :: k) (c :: i) (bs :: [j]).
(DecidableProfunctor p, DecidableProfunctor q, Enumerable j, Ob a,
 Ob c) =>
IndexedList bs -> Decision (p :.: q) a c (Search bs p q a c)
search @p @q @a @c (forall k. Finite k => IndexedList (Objects k)
finite @j)
  toHoldsComp :: forall (a :: k) (c :: i) r.
(:.:) p q a c
-> ((HoldsComp BySearch p q a c ~ 'TRU, Ob a, Ob c) => r) -> r
toHoldsComp = forall {i} {j} {k} (s :: ThinComp) (p :: j +-> k) (q :: i +-> j)
       (a :: k) (c :: i) r.
ComposeThin s p q =>
(:.:) p q a c -> ((HasArrowComp s p q a c, Ob a, Ob c) => r) -> r
forall (s :: ThinComp) (p :: j +-> k) (q :: i +-> j) (a :: k)
       (c :: i) r.
ComposeThin s p q =>
(:.:) p q a c -> ((HasArrowComp s p q a c, Ob a, Ob c) => r) -> r
withArrComp @BySearch

instance (DecideComp (ThinCompStrategy p q) p q) => DecidableProfunctor (p :.: q) where
  type Holds (p :.: q) a c = HoldsComp (ThinCompStrategy p q) p q a c
  decide :: forall (a :: k) (b :: j).
(Ob a, Ob b) =>
Decision (p :.: q) a b (Holds (p :.: q) a b)
decide @a @c = forall {i} {j} {k} (s :: ThinComp) (p :: j +-> k) (q :: i +-> j)
       (a :: k) (c :: i).
(DecideComp s p q, Ob a, Ob c) =>
Decision (p :.: q) a c (HoldsComp s p q a c)
forall (s :: ThinComp) (p :: j +-> k) (q :: j +-> j) (a :: k)
       (c :: j).
(DecideComp s p q, Ob a, Ob c) =>
Decision (p :.: q) a c (HoldsComp s p q a c)
decideComp @(ThinCompStrategy p q) @p @q @a @c
  toHolds :: forall (a :: k) (b :: j) r.
(:.:) p q a b
-> ((Holds (p :.: q) a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds = forall {i} {j} {k} (s :: ThinComp) (p :: j +-> k) (q :: i +-> j)
       (a :: k) (c :: i) r.
DecideComp s p q =>
(:.:) p q a c
-> ((HoldsComp s p q a c ~ 'TRU, Ob a, Ob c) => r) -> r
forall (s :: ThinComp) (p :: j +-> k) (q :: j +-> j) (a :: k)
       (c :: j) r.
DecideComp s p q =>
(:.:) p q a c
-> ((HoldsComp s p q a c ~ 'TRU, Ob a, Ob c) => r) -> r
toHoldsComp @(ThinCompStrategy p q)

-- * Closure: walks along a graph, in any enriching category

-- | A walk of at most @n@ steps along @p@, finished by an arrow of the base category. Its
-- hom-object in any enriching category is 'Walks': at 'BOOL' the truth of the walk, decided with
-- the path as witness; at 'COST' the shortest distance.
type Walk :: forall {k}. Nat -> (k +-> k) -> k +-> k
data Walk n p a b where
  Done :: forall {k} n (p :: k +-> k) a b. (a ~> b) -> Walk n p a b
  Step :: forall {k} n (p :: k +-> k) a c b. p a c -> Walk n p c b -> Walk ('S n) p a b

instance (Profunctor p) => Profunctor (Walk n p) where
  dimap :: forall (c :: j) (a :: j) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Walk n p a b -> Walk n p c d
dimap c ~> a
l b ~> d
r (Done a ~> b
f) = (c ~> d) -> Walk n p c d
forall {k} (n :: Nat) (p :: k +-> k) (a :: k) (b :: k).
(a ~> b) -> Walk n p a b
Done (b ~> d
r (b ~> d) -> (c ~> b) -> c ~> d
forall (b :: j) (c :: j) (a :: j). (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
. a ~> b
f (a ~> b) -> (c ~> a) -> c ~> b
forall (b :: j) (c :: j) (a :: j). (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
. c ~> a
l)
  dimap c ~> a
l b ~> d
r (Step p a c
e Walk n p c b
w) = p c c -> Walk n p c d -> Walk ('S n) p c d
forall {k} (n :: Nat) (p :: k +-> k) (a :: k) (c :: k) (b :: k).
p a c -> Walk n p c b -> Walk ('S n) p a b
Step ((c ~> a) -> p a c -> p c c
forall (c :: j) (a :: j) (b :: j). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
P.lmap c ~> a
l p a c
e) ((b ~> d) -> Walk n p c b -> Walk n p c d
forall (b :: j) (d :: j) (a :: j).
(b ~> d) -> Walk n p a b -> Walk n p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
P.rmap b ~> d
r Walk n p c b
w)
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: j) r.
((Ob a, Ob b) => r) -> Walk n p a b -> r
\\ Done a ~> b
f = r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall (a :: j) (b :: j) 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 ~> b
f
  (Ob a, Ob b) => r
r \\ Step p a c
e Walk n p c b
w = r
(Ob a, Ob b) => r
(Ob a, Ob c) => r
r ((Ob a, Ob c) => r) -> p a c -> r
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 a c
e ((Ob c, Ob b) => r) -> Walk n p c b -> r
forall (a :: j) (b :: j) r.
((Ob a, Ob b) => r) -> Walk n 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
\\ Walk n p c b
w

-- | The hom-object of a walk of at most @n@ steps, in any enriching category @v@: an arrow of the
-- base, or an edge followed by one entry of the previous iterate ('WalkRow'). Naming the whole
-- iterate rather than a shorter walk per pair is what keeps this affordable. At 'BOOL' it is the
-- truth of 'Walk', at 'COST' the shortest distance, computed by GHC at the type level and by 'row'
-- at the value level.
type Walks :: forall {k}. forall (v :: Kind) -> Nat -> (k +-> k) -> k -> k -> v
type family Walks v n p a b where
  Walks v 'Z (p :: k +-> k) a b = HomObj v a b
  Walks v ('S n) (p :: k +-> k) a b = HomObj v a b || MatVec v (Objects k) (WalkRow v n p b) p a

-- | The @n@-th iterate of the fixed point for a fixed target @b@: the hom-object of the walks of at
-- most @n@ steps into @b@, one entry per object, in the order of 'Objects'. It starts as the column
-- of the base hom-objects, there being no step to take yet, and grows by 'NextRow'.
--
-- Each iterate is written in terms of the whole previous one, so it is computed once and read by
-- every object. That sharing is what makes the fixed point affordable: the work is the number of
-- steps times the square of the number of objects, where a recursion per pair of objects would
-- instead cost the number of objects to the power of the number of steps.
type WalkRow :: forall {k}. forall (v :: Kind) -> Nat -> (k +-> k) -> k -> [v]
type family WalkRow v n p b where
  WalkRow v 'Z (p :: k +-> k) b = MatCol v (Objects k) (Hom k) b
  WalkRow v ('S n) (p :: k +-> k) b = NextRow v (Objects k) (WalkRow v n p b) p b

-- | One more step, taken for every object at once: an arrow of the base, or an edge into the
-- previous iterate ('MatVec').
type NextRow :: forall {k}. forall (v :: Kind) -> [k] -> [v] -> (k +-> k) -> k -> [v]
type family NextRow v as row p b where
  NextRow v '[] row p b = '[]
  NextRow v (a ': as) row (p :: k +-> k) b =
    (HomObj v a b || MatVec v (Objects k) row p a) ': NextRow v as row p b

-- | The Kleene closure of @p@: walks of at most as many steps as there are objects, which is all
-- of them, since a shortest walk never revisits an object. It is the free category on the graph
-- @p@ in whatever @p@ is enriched in: at 'BOOL' the reflexive-transitive closure of a relation, with
-- the path as witness ('decide'); at 'COST' the free Lawvere metric space, with the shortest
-- distances ('withProObj') and the shortest paths ('shortest').
type Closure (p :: k +-> k) = Walk (Length (Objects k)) p

-- * Graded walks

-- | What the closure needs of its ingredients: a quantale to compute in, an enriched graph over an
-- enumerable enriched base, and a known number of steps.
type Closing :: forall {k}. Kind -> Nat -> (k +-> k) -> Constraint
type Closing v n (p :: k +-> k) = (SNatI n, Quantale v, EnrichedProfunctor v p, Enriched v k, Enumerable k)

-- | A walk graded by its cost: each piece comes with a budget, an arrow of @v@ into the piece's
-- hom-object, and the grade of the walk is the tensor of the budgets. A walk at grade @d@ is a
-- generalised element of the closure, @d ~> 'Walks' v n p a b@ ('underlyingAt'), and 'shortest'
-- produces one at grade exactly the hom-object.
type GradedWalk :: forall {k}. forall (v :: Kind) -> Nat -> (k +-> k) -> v -> k -> k -> Type
data GradedWalk v n p d a b where
  DoneAt :: forall {k} v n (p :: k +-> k) d a b. (Ob a, Ob b) => (d ~> HomObj v a b) -> GradedWalk v n p d a b
  StepAt
    :: forall {k} v n (p :: k +-> k) a c b e d
     . (Ob a, Ob b, Ob c, Ob e, Ob d)
    => (e ~> ProObj v p a c) -> GradedWalk v n p d c b -> GradedWalk v ('S n) p (e ** d) a b

-- | The @n@-th iterate reflected to the value level: every object paired with its own entry, which
-- is exactly the hom-object of the walks from it. 'row' builds one and everything that needs a
-- shorter walk reads it, so the value level shares its work the same way the type level does.
type Row :: forall {k}. forall (v :: Kind) -> Nat -> (k +-> k) -> k -> [k] -> [v] -> Type
data Row v n p b as ws where
  RNil :: Row v n p b '[] '[]
  RCons
    :: forall {k} a as v ws n (p :: k +-> k) b
     . (Ob a, Ob (Walks v n p a b))
    => Row v n p b as ws -> Row v n p b (a ': as) (Walks v n p a b ': ws)

-- | The @n@-th iterate: the base hom-objects, then one more step for every object at a time.
row :: forall {k} v n (p :: k +-> k) b. (Closing v n p, Ob b) => Row v n p b (Objects k) (WalkRow v n p b)
row :: forall {k} v (n :: Nat) (p :: k +-> k) (b :: k).
(Closing v n p, Ob b) =>
Row v n p b (Objects k) (WalkRow v n p b)
row = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ ->
    let homRow :: forall as. IndexedList as -> Row v 'Z p b as (MatCol v as (Hom k) b)
        homRow :: forall (as :: [k]).
IndexedList as -> Row v 'Z p b as (MatCol v as (Hom k) b)
homRow IndexedList as
FNil = Row v 'Z p b as (MatCol v as (Hom k) b)
Row v 'Z p b '[] '[]
forall {k} v (n :: Nat) (p :: k +-> k) (b :: k).
Row v n p b '[] '[]
RNil
        homRow (FCons @a IndexedList as1
as) = forall k (a :: k) r.
(Enumerable k, KnownIndex a) =>
(Ob a => r) -> r
withOb @k @a (forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
forall v (p :: k +-> k) (a :: k) (b :: k) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
withProObj @v @(Hom k) @a @b (Row v 'Z p b as1 (MatCol v as1 (Hom k) b)
-> Row
     v 'Z p b (a : as1) (Walks v 'Z p a b : MatCol v as1 (Hom k) b)
forall {k} (n :: k) (c :: [k]) v (e :: [v]) (n :: Nat)
       (p :: k +-> k) (b :: k).
(Ob n, Ob (Walks v n p n b)) =>
Row v n p b c e -> Row v n p b (n : c) (Walks v n p n b : e)
RCons (IndexedList as1 -> Row v 'Z p b as1 (MatCol v as1 (Hom k) b)
forall (as :: [k]).
IndexedList as -> Row v 'Z p b as (MatCol v as (Hom k) b)
homRow IndexedList as1
as)))
    in IndexedList (Objects k)
-> Row v 'Z p b (Objects k) (MatCol v (Objects k) (Hom k) b)
forall (as :: [k]).
IndexedList as -> Row v 'Z p b as (MatCol v as (Hom k) b)
homRow (forall k. Finite k => IndexedList (Objects k)
finite @k)
  SS @n' ->
    let prev :: Row v n1 p b (Objects k) (WalkRow v n1 p b)
prev = forall {k} v (n :: Nat) (p :: k +-> k) (b :: k).
(Closing v n p, Ob b) =>
Row v n p b (Objects k) (WalkRow v n p b)
forall v (n :: Nat) (p :: k +-> k) (b :: k).
(Closing v n p, Ob b) =>
Row v n p b (Objects k) (WalkRow v n p b)
row @v @n' @p @b
        nextRow :: forall as. IndexedList as -> Row v ('S n') p b as (NextRow v as (WalkRow v n' p b) p b)
        nextRow :: forall (as :: [k]).
IndexedList as
-> Row v ('S n1) p b as (NextRow v as (WalkRow v n1 p b) p b)
nextRow IndexedList as
FNil = Row v ('S n1) p b as (NextRow v as (WalkRow v n1 p b) p b)
Row v ('S n1) p b '[] '[]
forall {k} v (n :: Nat) (p :: k +-> k) (b :: k).
Row v n p b '[] '[]
RNil
        nextRow (FCons @a IndexedList as1
as) =
          forall k (a :: k) r.
(Enumerable k, KnownIndex a) =>
(Ob a => r) -> r
withOb @k @a
            ( forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
forall v (p :: k +-> k) (a :: k) (b :: k) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
withProObj @v @(Hom k) @a @b
                ( forall (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k) (cs :: [k])
       (ws :: [v]) r.
(Closing v n p, Ob a) =>
Row v n p b cs ws -> (Ob (MatVec v cs ws p a) => r) -> r
forall {k} (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k)
       (cs :: [k]) (ws :: [v]) r.
(Closing v n p, Ob a) =>
Row v n p b cs ws -> (Ob (MatVec v cs ws p a) => r) -> r
withObMatVec @a
                    Row v n1 p b (Objects k) (WalkRow v n1 p b)
prev
                    ( forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @v @(HomObj v a b) @(MatVec v (Objects k) (WalkRow v n' p b) p a)
                        (Row v ('S n1) p b as1 (NextRow v as1 (WalkRow v n1 p b) p b)
-> Row
     v
     ('S n1)
     p
     b
     (a : as1)
     (Walks v ('S n1) p a b : NextRow v as1 (WalkRow v n1 p b) p b)
forall {k} (n :: k) (c :: [k]) v (e :: [v]) (n :: Nat)
       (p :: k +-> k) (b :: k).
(Ob n, Ob (Walks v n p n b)) =>
Row v n p b c e -> Row v n p b (n : c) (Walks v n p n b : e)
RCons (IndexedList as1
-> Row v ('S n1) p b as1 (NextRow v as1 (WalkRow v n1 p b) p b)
forall (as :: [k]).
IndexedList as
-> Row v ('S n1) p b as (NextRow v as (WalkRow v n1 p b) p b)
nextRow IndexedList as1
as))
                    )
                )
            )
    in IndexedList (Objects k)
-> Row
     v
     ('S n1)
     p
     b
     (Objects k)
     (NextRow v (Objects k) (WalkRow v n1 p b) p b)
forall (as :: [k]).
IndexedList as
-> Row v ('S n1) p b as (NextRow v as (WalkRow v n1 p b) p b)
nextRow (forall k. Finite k => IndexedList (Objects k)
finite @k)

-- | Object evidence for the hom-object of a walk: read the object's own entry out of an iterate.
withObRow
  :: forall {k} (a :: k) v n (p :: k +-> k) b cs ws r
   . Member a cs -> Row v n p b cs ws -> ((Ob (Walks v n p a b)) => r) -> r
withObRow :: forall {k} (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k)
       (cs :: [k]) (ws :: [v]) r.
Member a cs
-> Row v n p b cs ws -> (Ob (Walks v n p a b) => r) -> r
withObRow Member a cs
Here (RCons Row v n p b as ws
_) Ob (Walks v n p a b) => r
r = r
Ob (Walks v n p a b) => r
r
withObRow (There Member a as1
m) (RCons Row v n p b as ws
rest) Ob (Walks v n p a b) => r
r = Member a as1
-> Row v n p b as1 ws -> (Ob (Walks v n p a b) => r) -> r
forall {k} (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k)
       (cs :: [k]) (ws :: [v]) r.
Member a cs
-> Row v n p b cs ws -> (Ob (Walks v n p a b) => r) -> r
withObRow Member a as1
m Row v n p b as1 ws
Row v n p b as ws
rest r
Ob (Walks v n p a b) => r
r

-- | The same, for a caller that is not already holding the iterate.
withObWalks
  :: forall {k} v n (p :: k +-> k) a b r
   . (Closing v n p, Ob a, Ob b)
  => ((Ob (Walks v n p a b)) => r) -> r
withObWalks :: forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k) r.
(Closing v n p, Ob a, Ob b) =>
(Ob (Walks v n p a b) => r) -> r
withObWalks = Member a (Objects k)
-> Row v n p b (Objects k) (WalkRow v n p b)
-> (Ob (Walks v n p a b) => r)
-> r
forall {k} (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k)
       (cs :: [k]) (ws :: [v]) r.
Member a cs
-> Row v n p b cs ws -> (Ob (Walks v n p a b) => r) -> r
withObRow (forall (a :: k). (Enumerable k, Ob a) => Member a (Objects k)
forall {k} (a :: k). (Enumerable k, Ob a) => Member a (Objects k)
member @a) (forall {k} v (n :: Nat) (p :: k +-> k) (b :: k).
(Closing v n p, Ob b) =>
Row v n p b (Objects k) (WalkRow v n p b)
forall v (n :: Nat) (p :: k +-> k) (b :: k).
(Closing v n p, Ob b) =>
Row v n p b (Objects k) (WalkRow v n p b)
row @v @n @p @b)

-- | Object evidence for one summand of 'MatVec': an edge and its tensor with the entry after it.
withObStep
  :: forall {k} v n (p :: k +-> k) a c b r
   . (Closing v n p, Ob a, Ob c, Ob (Walks v n p c b))
  => ((Ob (ProObj v p a c), Ob (ProObj v p a c ** Walks v n p c b)) => r) -> r
withObStep :: forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (c :: k) (b :: k)
       r.
(Closing v n p, Ob a, Ob c, Ob (Walks v n p c b)) =>
((Ob (ProObj v p a c), Ob (ProObj v p a c ** Walks v n p c b)) =>
 r)
-> r
withObStep (Ob (ProObj v p a c), Ob (ProObj v p a c ** Walks v n p c b)) => r
r = forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
forall v (p :: k +-> k) (a :: k) (b :: k) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
withProObj @v @p @a @c (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @v @(ProObj v p a c) @(Walks v n p c b) r
Ob (ProObj v p a c ** Walks v n p c b) => r
(Ob (ProObj v p a c), Ob (ProObj v p a c ** Walks v n p c b)) => r
r)

-- | Object evidence for the join over the given middle objects.
withObMatVec
  :: forall {k} a v n (p :: k +-> k) b cs ws r
   . (Closing v n p, Ob a)
  => Row v n p b cs ws -> ((Ob (MatVec v cs ws p a)) => r) -> r
withObMatVec :: forall {k} (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k)
       (cs :: [k]) (ws :: [v]) r.
(Closing v n p, Ob a) =>
Row v n p b cs ws -> (Ob (MatVec v cs ws p a) => r) -> r
withObMatVec Row v n p b cs ws
RNil Ob (MatVec v cs ws p a) => r
r = r
Ob (MatVec v cs ws p a) => r
r
withObMatVec (RCons @c @cs' @_ @ws' Row v n p b as ws
rest) Ob (MatVec v cs ws p a) => r
r =
  forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (c :: k) (b :: k)
       r.
(Closing v n p, Ob a, Ob c, Ob (Walks v n p c b)) =>
((Ob (ProObj v p a c), Ob (ProObj v p a c ** Walks v n p c b)) =>
 r)
-> r
forall v (n :: Nat) (p :: k +-> k) (a :: k) (c :: k) (b :: k) r.
(Closing v n p, Ob a, Ob c, Ob (Walks v n p c b)) =>
((Ob (ProObj v p a c), Ob (ProObj v p a c ** Walks v n p c b)) =>
 r)
-> r
withObStep @v @n @p @a @c @b
    ( forall (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k) (cs :: [k])
       (ws :: [v]) r.
(Closing v n p, Ob a) =>
Row v n p b cs ws -> (Ob (MatVec v cs ws p a) => r) -> r
forall {k} (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k)
       (cs :: [k]) (ws :: [v]) r.
(Closing v n p, Ob a) =>
Row v n p b cs ws -> (Ob (MatVec v cs ws p a) => r) -> r
withObMatVec @a
        Row v n p b as ws
rest
        (forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @v @(ProObj v p a c ** Walks v n p c b) @(MatVec v cs' ws' p a) r
Ob ((ProObj v p a a ** Walks v n p a b) || MatVec v as ws p a) => r
Ob (MatVec v cs ws p a) => r
r)
    )

-- | A graded walk is a generalised element of the closure: inject it into the join at its middle
-- object.
underlyingAt
  :: forall {k} v n (p :: k +-> k) d a b
   . (Closing v n p)
  => GradedWalk v n p d a b -> d ~> Walks v n p a b
underlyingAt :: forall {k} v (n :: Nat) (p :: k +-> k) (d :: v) (a :: k) (b :: k).
Closing v n p =>
GradedWalk v n p d a b -> d ~> Walks v n p a b
underlyingAt (DoneAt d ~> HomObj v a b
g) = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ -> d ~> HomObj v a b
d ~> Walks v n p a b
g
  SS @n' ->
    forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
forall v (p :: k +-> k) (a :: k) (b :: k) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
withProObj @v @(Hom k) @a @b
      ( forall (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k) (cs :: [k])
       (ws :: [v]) r.
(Closing v n p, Ob a) =>
Row v n p b cs ws -> (Ob (MatVec v cs ws p a) => r) -> r
forall {k} (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k)
       (cs :: [k]) (ws :: [v]) r.
(Closing v n p, Ob a) =>
Row v n p b cs ws -> (Ob (MatVec v cs ws p a) => r) -> r
withObMatVec @a
          (forall {k} v (n :: Nat) (p :: k +-> k) (b :: k).
(Closing v n p, Ob b) =>
Row v n p b (Objects k) (WalkRow v n p b)
forall v (n :: Nat) (p :: k +-> k) (b :: k).
(Closing v n p, Ob b) =>
Row v n p b (Objects k) (WalkRow v n p b)
row @v @n' @p @b)
          (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @v @(HomObj v a b) @(MatVec v (Objects k) (WalkRow v n' p b) p a))
      )
      (HomObj v a b
 ~> (HomObj v a b || MatVec v (Objects k) (WalkRow v n1 p b) p a))
-> (d ~> HomObj v a b)
-> d
   ~> (HomObj v a b || MatVec v (Objects k) (WalkRow v n1 p b) p a)
forall (b :: v) (c :: v) (a :: v). (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
. d ~> HomObj v a b
g
underlyingAt (StepAt @_ @_ @_ @_ @c e ~> ProObj v p a c
ee GradedWalk v n p d c b
w) = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SS @n' -> forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (c :: k) (b :: k)
       (e :: v) (d :: v).
(Closing v n p, Ob a, Ob b, Ob c) =>
(e ~> ProObj v p a c)
-> (d ~> Walks v n p c b) -> (e ** d) ~> Walks v ('S n) p a b
forall v (n :: Nat) (p :: k +-> k) (a :: k) (c :: k) (b :: k)
       (e :: v) (d :: v).
(Closing v n p, Ob a, Ob b, Ob c) =>
(e ~> ProObj v p a c)
-> (d ~> Walks v n p c b) -> (e ** d) ~> Walks v ('S n) p a b
stepAt @v @n' @p @a @c @b e ~> ProObj v p a c
ee (GradedWalk v n p d c b -> d ~> Walks v n p c b
forall {k} v (n :: Nat) (p :: k +-> k) (d :: v) (a :: k) (b :: k).
Closing v n p =>
GradedWalk v n p d a b -> d ~> Walks v n p a b
underlyingAt GradedWalk v n p d c b
w)

-- | An edge with a budget, followed by a generalised element of the shorter walks.
stepAt
  :: forall {k} v n (p :: k +-> k) a c b e d
   . (Closing v n p, Ob a, Ob b, Ob c)
  => (e ~> ProObj v p a c) -> (d ~> Walks v n p c b) -> (e ** d) ~> Walks v ('S n) p a b
stepAt :: forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (c :: k) (b :: k)
       (e :: v) (d :: v).
(Closing v n p, Ob a, Ob b, Ob c) =>
(e ~> ProObj v p a c)
-> (d ~> Walks v n p c b) -> (e ** d) ~> Walks v ('S n) p a b
stepAt e ~> ProObj v p a c
ee d ~> Walks v n p c b
uw = case e ~> ProObj v p a c
ee (e ~> ProObj v p a c)
-> (d ~> Walks v n p c b)
-> (e ** d) ~> (ProObj v p a c ** Walks v n p c b)
forall (x1 :: v) (x2 :: v) (y1 :: v) (y2 :: v).
(x1 ~> x2) -> (y1 ~> y2) -> (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)
** d ~> Walks v n p c b
uw of
  step :: (e ** d) ~> (ProObj v p a c ** Walks v n p c b)
step@(e ** d) ~> (ProObj v p a c ** Walks v n p c b)
Objs ->
    let rw :: Row v n p b (Objects k) (WalkRow v n p b)
rw = forall {k} v (n :: Nat) (p :: k +-> k) (b :: k).
(Closing v n p, Ob b) =>
Row v n p b (Objects k) (WalkRow v n p b)
forall v (n :: Nat) (p :: k +-> k) (b :: k).
(Closing v n p, Ob b) =>
Row v n p b (Objects k) (WalkRow v n p b)
row @v @n @p @b
    in forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
forall v (p :: k +-> k) (a :: k) (b :: k) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
withProObj @v @(Hom k) @a @b
         ( forall (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k) (cs :: [k])
       (ws :: [v]) r.
(Closing v n p, Ob a) =>
Row v n p b cs ws -> (Ob (MatVec v cs ws p a) => r) -> r
forall {k} (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k)
       (cs :: [k]) (ws :: [v]) r.
(Closing v n p, Ob a) =>
Row v n p b cs ws -> (Ob (MatVec v cs ws p a) => r) -> r
withObMatVec @a
             Row v n p b (Objects k) (WalkRow v n p b)
rw
             ( Member c (Objects k)
-> Row v n p b (Objects k) (WalkRow v n p b)
-> (Ob (Walks v n p c b) =>
    (e ** d)
    ~> (ProObj v (Hom k) a b
        || MatVec v (Objects k) (WalkRow v n p b) p a))
-> (e ** d)
   ~> (ProObj v (Hom k) a b
       || MatVec v (Objects k) (WalkRow v n p b) p a)
forall {k} (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k)
       (cs :: [k]) (ws :: [v]) r.
Member a cs
-> Row v n p b cs ws -> (Ob (Walks v n p a b) => r) -> r
withObRow
                 (forall (a :: k). (Enumerable k, Ob a) => Member a (Objects k)
forall {k} (a :: k). (Enumerable k, Ob a) => Member a (Objects k)
member @c)
                 Row v n p b (Objects k) (WalkRow v n p b)
rw
                 ( forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @v @(HomObj v a b) @(MatVec v (Objects k) (WalkRow v n p b) p a)
                     (MatVec v (Objects k) (WalkRow v n p b) p a
 ~> (ProObj v (Hom k) a b
     || MatVec v (Objects k) (WalkRow v n p b) p a))
-> ((e ** d) ~> MatVec v (Objects k) (WalkRow v n p b) p a)
-> (e ** d)
   ~> (ProObj v (Hom k) a b
       || MatVec v (Objects k) (WalkRow v n p b) p a)
forall (b :: v) (c :: v) (a :: v). (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
. forall (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k) (c :: k)
       (cs :: [k]) (ws :: [v]).
(Closing v n p, Ob a, Ob c, Ob (Walks v n p c b)) =>
Row v n p b cs ws
-> Member c cs
-> (ProObj v p a c ** Walks v n p c b) ~> MatVec v cs ws p a
forall {k} (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k) (c :: k)
       (cs :: [k]) (ws :: [v]).
(Closing v n p, Ob a, Ob c, Ob (Walks v n p c b)) =>
Row v n p b cs ws
-> Member c cs
-> (ProObj v p a c ** Walks v n p c b) ~> MatVec v cs ws p a
inject @a Row v n p b (Objects k) (WalkRow v n p b)
rw (forall (a :: k). (Enumerable k, Ob a) => Member a (Objects k)
forall {k} (a :: k). (Enumerable k, Ob a) => Member a (Objects k)
member @c)
                     ((ProObj v p a c ** Walks v n p c b)
 ~> MatVec v (Objects k) (WalkRow v n p b) p a)
-> ((e ** d) ~> (ProObj v p a c ** Walks v n p c b))
-> (e ** d) ~> MatVec v (Objects k) (WalkRow v n p b) p a
forall (b :: v) (c :: v) (a :: v). (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
. (e ** d) ~> (ProObj v p a c ** Walks v n p c b)
step
                 )
             )
         )

-- | The injection of one summand into the join over the middle objects.
inject
  :: forall {k} a v n (p :: k +-> k) b c cs ws
   . (Closing v n p, Ob a, Ob c, Ob (Walks v n p c b))
  => Row v n p b cs ws -> Member c cs -> (ProObj v p a c ** Walks v n p c b) ~> MatVec v cs ws p a
inject :: forall {k} (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k) (c :: k)
       (cs :: [k]) (ws :: [v]).
(Closing v n p, Ob a, Ob c, Ob (Walks v n p c b)) =>
Row v n p b cs ws
-> Member c cs
-> (ProObj v p a c ** Walks v n p c b) ~> MatVec v cs ws p a
inject Row v n p b cs ws
RNil Member c cs
m = case Member c cs
m of {}
inject (RCons @_ @cs' @_ @ws' Row v n p b as ws
rest) Member c cs
Here =
  forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (c :: k) (b :: k)
       r.
(Closing v n p, Ob a, Ob c, Ob (Walks v n p c b)) =>
((Ob (ProObj v p a c), Ob (ProObj v p a c ** Walks v n p c b)) =>
 r)
-> r
forall v (n :: Nat) (p :: k +-> k) (a :: k) (c :: k) (b :: k) r.
(Closing v n p, Ob a, Ob c, Ob (Walks v n p c b)) =>
((Ob (ProObj v p a c), Ob (ProObj v p a c ** Walks v n p c b)) =>
 r)
-> r
withObStep @v @n @p @a @c @b
    ( forall (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k) (cs :: [k])
       (ws :: [v]) r.
(Closing v n p, Ob a) =>
Row v n p b cs ws -> (Ob (MatVec v cs ws p a) => r) -> r
forall {k} (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k)
       (cs :: [k]) (ws :: [v]) r.
(Closing v n p, Ob a) =>
Row v n p b cs ws -> (Ob (MatVec v cs ws p a) => r) -> r
withObMatVec @a
        Row v n p b as ws
rest
        (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @v @(ProObj v p a c ** Walks v n p c b) @(MatVec v cs' ws' p a))
    )
inject (RCons @c' @cs' @_ @ws' Row v n p b as ws
rest) (There Member c as1
m) =
  forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (c :: k) (b :: k)
       r.
(Closing v n p, Ob a, Ob c, Ob (Walks v n p c b)) =>
((Ob (ProObj v p a c), Ob (ProObj v p a c ** Walks v n p c b)) =>
 r)
-> r
forall v (n :: Nat) (p :: k +-> k) (a :: k) (c :: k) (b :: k) r.
(Closing v n p, Ob a, Ob c, Ob (Walks v n p c b)) =>
((Ob (ProObj v p a c), Ob (ProObj v p a c ** Walks v n p c b)) =>
 r)
-> r
withObStep @v @n @p @a @c' @b
    ( forall (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k) (cs :: [k])
       (ws :: [v]) r.
(Closing v n p, Ob a) =>
Row v n p b cs ws -> (Ob (MatVec v cs ws p a) => r) -> r
forall {k} (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k)
       (cs :: [k]) (ws :: [v]) r.
(Closing v n p, Ob a) =>
Row v n p b cs ws -> (Ob (MatVec v cs ws p a) => r) -> r
withObMatVec @a
        Row v n p b as ws
rest
        ( forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @v @(ProObj v p a c' ** Walks v n p c' b) @(MatVec v cs' ws' p a)
            (MatVec v as ws p a
 ~> ((ProObj v p a a ** Walks v n p a b) || MatVec v as ws p a))
-> ((ProObj v p a c ** Walks v n p c b) ~> MatVec v as ws p a)
-> (ProObj v p a c ** Walks v n p c b)
   ~> ((ProObj v p a a ** Walks v n p a b) || MatVec v as ws p a)
forall (b :: v) (c :: v) (a :: v). (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
. forall (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k) (c :: k)
       (cs :: [k]) (ws :: [v]).
(Closing v n p, Ob a, Ob c, Ob (Walks v n p c b)) =>
Row v n p b cs ws
-> Member c cs
-> (ProObj v p a c ** Walks v n p c b) ~> MatVec v cs ws p a
forall {k} (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k) (c :: k)
       (cs :: [k]) (ws :: [v]).
(Closing v n p, Ob a, Ob c, Ob (Walks v n p c b)) =>
Row v n p b cs ws
-> Member c cs
-> (ProObj v p a c ** Walks v n p c b) ~> MatVec v cs ws p a
inject @a Row v n p b as ws
rest Member c as
Member c as1
m
        )
    )

-- | A walk of pieces at the unit, as a generalised element at the unit.
underlyingWalk
  :: forall {k} v n (p :: k +-> k) a b
   . (Closing v n p)
  => Walk n p a b -> Unit ~> Walks v n p a b
underlyingWalk :: forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k).
Closing v n p =>
Walk n p a b -> Unit ~> Walks v n p a b
underlyingWalk (Done f :: a ~> b
f@a ~> b
Objs) = forall {k} v (n :: Nat) (p :: k +-> k) (d :: v) (a :: k) (b :: k).
Closing v n p =>
GradedWalk v n p d a b -> d ~> Walks v n p a b
forall v (n :: Nat) (p :: k +-> k) (d :: v) (a :: k) (b :: k).
Closing v n p =>
GradedWalk v n p d a b -> d ~> Walks v n p a b
underlyingAt @v @n @p @Unit @a @b (forall {k} v (n :: Nat) (p :: k +-> k) (d :: v) (a :: k) (b :: k).
(Ob a, Ob b) =>
(d ~> HomObj v a b) -> GradedWalk v n p d a b
forall v (n :: Nat) (p :: k +-> k) (d :: v) (a :: k) (b :: k).
(Ob a, Ob b) =>
(d ~> HomObj v a b) -> GradedWalk v n p d a b
DoneAt @v @n @p @Unit @a @b (forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j).
EnrichedProfunctor v p =>
p a b -> Unit ~> ProObj v p a b
forall v (p :: k +-> k) (a :: k) (b :: k).
EnrichedProfunctor v p =>
p a b -> Unit ~> ProObj v p a b
underlying @v @(Hom k) @a @b a ~> b
f))
underlyingWalk (Step @_ @_ @_ @c e :: p a c
e@p a c
Objs w :: Walk n p c b
w@Walk n p c b
Objs) = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SS @n' -> forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (c :: k) (b :: k)
       (e :: v) (d :: v).
(Closing v n p, Ob a, Ob b, Ob c) =>
(e ~> ProObj v p a c)
-> (d ~> Walks v n p c b) -> (e ** d) ~> Walks v ('S n) p a b
forall v (n :: Nat) (p :: k +-> k) (a :: k) (c :: k) (b :: k)
       (e :: v) (d :: v).
(Closing v n p, Ob a, Ob b, Ob c) =>
(e ~> ProObj v p a c)
-> (d ~> Walks v n p c b) -> (e ** d) ~> Walks v ('S n) p a b
stepAt @v @n' @p @a @c @b (forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j).
EnrichedProfunctor v p =>
p a b -> Unit ~> ProObj v p a b
forall v (p :: k +-> k) (a :: k) (b :: k).
EnrichedProfunctor v p =>
p a b -> Unit ~> ProObj v p a b
underlying @v @p p a c
e) (forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k).
Closing v n p =>
Walk n p a b -> Unit ~> Walks v n p a b
forall v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k).
Closing v n p =>
Walk n p a b -> Unit ~> Walks v n p a b
underlyingWalk @v Walk n p c b
w) ((TerminalObject ** TerminalObject)
 ~> (HomObj v a b || MatVec v (Objects k) (WalkRow v n p b) p a))
-> (TerminalObject ~> (TerminalObject ** TerminalObject))
-> TerminalObject
   ~> (HomObj v a b || MatVec v (Objects k) (WalkRow v n p b) p a)
forall (b :: v) (c :: v) (a :: v). (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
. forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @v @Unit

-- | The best walk between two points, graded by exactly their hom-object: a shortest path at
-- 'COST', a path or the absence of one at 'BOOL'. At every join it keeps the summand the join is
-- ('minIs'); a pair no walk connects gets the empty walk at 'InitialObject'.
shortest
  :: forall {k} v n (p :: k +-> k) a b
   . (Closing v n p, Ob a, Ob b)
  => GradedWalk v n p (Walks v n p a b) a b
shortest :: forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k).
(Closing v n p, Ob a, Ob b) =>
GradedWalk v n p (Walks v n p a b) a b
shortest = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ -> forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
forall v (p :: k +-> k) (a :: k) (b :: k) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
withProObj @v @(Hom k) @a @b (forall {k} v (n :: Nat) (p :: k +-> k) (d :: v) (a :: k) (b :: k).
(Ob a, Ob b) =>
(d ~> HomObj v a b) -> GradedWalk v n p d a b
forall v (n :: Nat) (p :: k +-> k) (d :: v) (a :: k) (b :: k).
(Ob a, Ob b) =>
(d ~> HomObj v a b) -> GradedWalk v n p d a b
DoneAt @v @n @p (forall (a :: v). (CategoryOf v, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(HomObj v a b)))
  SS @n' ->
    let rw :: Row v n1 p b (Objects k) (WalkRow v n1 p b)
rw = forall {k} v (n :: Nat) (p :: k +-> k) (b :: k).
(Closing v n p, Ob b) =>
Row v n p b (Objects k) (WalkRow v n p b)
forall v (n :: Nat) (p :: k +-> k) (b :: k).
(Closing v n p, Ob b) =>
Row v n p b (Objects k) (WalkRow v n p b)
row @v @n' @p @b
    in forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
forall v (p :: k +-> k) (a :: k) (b :: k) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
withProObj @v @(Hom k) @a @b
         ( forall (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k) (cs :: [k])
       (ws :: [v]) r.
(Closing v n p, Ob a) =>
Row v n p b cs ws -> (Ob (MatVec v cs ws p a) => r) -> r
forall {k} (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k)
       (cs :: [k]) (ws :: [v]) r.
(Closing v n p, Ob a) =>
Row v n p b cs ws -> (Ob (MatVec v cs ws p a) => r) -> r
withObMatVec @a Row v n1 p b (Objects k) (WalkRow v n1 p b)
rw case forall v (x :: v) (y :: v). (Quantale v, Ob x, Ob y) => MinIs x y
minIs @v @(HomObj v a b) @(MatVec v (Objects k) (WalkRow v n' p b) p a) of
             MinIs
  (ProObj v (Hom k) a b)
  (MatVec v (Objects k) (WalkRow v n1 p b) p a)
MinLeft -> forall {k} v (n :: Nat) (p :: k +-> k) (d :: v) (a :: k) (b :: k).
(Ob a, Ob b) =>
(d ~> HomObj v a b) -> GradedWalk v n p d a b
forall v (n :: Nat) (p :: k +-> k) (d :: v) (a :: k) (b :: k).
(Ob a, Ob b) =>
(d ~> HomObj v a b) -> GradedWalk v n p d a b
DoneAt @v @n @p (forall (a :: v). (CategoryOf v, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(HomObj v a b))
             MinIs
  (ProObj v (Hom k) a b)
  (MatVec v (Objects k) (WalkRow v n1 p b) p a)
MinRight -> forall (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k) (cs :: [k])
       (ws :: [v]).
(Closing v n p, Ob a, Ob b) =>
Row v n p b cs ws -> GradedWalk v ('S n) p (MatVec v cs ws p a) a b
forall {k} (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k)
       (cs :: [k]) (ws :: [v]).
(Closing v n p, Ob a, Ob b) =>
Row v n p b cs ws -> GradedWalk v ('S n) p (MatVec v cs ws p a) a b
best @a Row v n1 p b (Objects k) (WalkRow v n1 p b)
rw
         )

-- | The best walk through one of the given middle objects.
best
  :: forall {k} a v n (p :: k +-> k) b cs ws
   . (Closing v n p, Ob a, Ob b)
  => Row v n p b cs ws -> GradedWalk v ('S n) p (MatVec v cs ws p a) a b
best :: forall {k} (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k)
       (cs :: [k]) (ws :: [v]).
(Closing v n p, Ob a, Ob b) =>
Row v n p b cs ws -> GradedWalk v ('S n) p (MatVec v cs ws p a) a b
best Row v n p b cs ws
RNil = forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
forall v (p :: k +-> k) (a :: k) (b :: k) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
withProObj @v @(Hom k) @a @b (forall {k} v (n :: Nat) (p :: k +-> k) (d :: v) (a :: k) (b :: k).
(Ob a, Ob b) =>
(d ~> HomObj v a b) -> GradedWalk v n p d a b
forall v (n :: Nat) (p :: k +-> k) (d :: v) (a :: k) (b :: k).
(Ob a, Ob b) =>
(d ~> HomObj v a b) -> GradedWalk v n p d a b
DoneAt @v @('S n) @p (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @v @(HomObj v a b)))
best (RCons @c @cs' @_ @ws' Row v n p b as ws
rest) =
  forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (c :: k) (b :: k)
       r.
(Closing v n p, Ob a, Ob c, Ob (Walks v n p c b)) =>
((Ob (ProObj v p a c), Ob (ProObj v p a c ** Walks v n p c b)) =>
 r)
-> r
forall v (n :: Nat) (p :: k +-> k) (a :: k) (c :: k) (b :: k) r.
(Closing v n p, Ob a, Ob c, Ob (Walks v n p c b)) =>
((Ob (ProObj v p a c), Ob (ProObj v p a c ** Walks v n p c b)) =>
 r)
-> r
withObStep @v @n @p @a @c @b
    ( forall (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k) (cs :: [k])
       (ws :: [v]) r.
(Closing v n p, Ob a) =>
Row v n p b cs ws -> (Ob (MatVec v cs ws p a) => r) -> r
forall {k} (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k)
       (cs :: [k]) (ws :: [v]) r.
(Closing v n p, Ob a) =>
Row v n p b cs ws -> (Ob (MatVec v cs ws p a) => r) -> r
withObMatVec @a Row v n p b as ws
rest case forall v (x :: v) (y :: v). (Quantale v, Ob x, Ob y) => MinIs x y
minIs @v @(ProObj v p a c ** Walks v n p c b) @(MatVec v cs' ws' p a) of
        MinIs (ProObj v p a a ** Walks v n p a b) (MatVec v as ws p a)
MinLeft -> (ProObj v p a a ~> ProObj v p a a)
-> GradedWalk v n p (Walks v n p a b) a b
-> GradedWalk v ('S n) p (ProObj v p a a ** Walks v n p a b) a b
forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (c :: k) (b :: k)
       (e :: v) (d :: v).
(Ob a, Ob b, Ob c, Ob e, Ob d) =>
(e ~> ProObj v p a c)
-> GradedWalk v n p d c b -> GradedWalk v ('S n) p (e ** d) a b
StepAt (forall (a :: v). (CategoryOf v, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(ProObj v p a c)) (forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k).
(Closing v n p, Ob a, Ob b) =>
GradedWalk v n p (Walks v n p a b) a b
forall v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k).
(Closing v n p, Ob a, Ob b) =>
GradedWalk v n p (Walks v n p a b) a b
shortest @v @n @p @c @b)
        MinIs (ProObj v p a a ** Walks v n p a b) (MatVec v as ws p a)
MinRight -> forall (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k) (cs :: [k])
       (ws :: [v]).
(Closing v n p, Ob a, Ob b) =>
Row v n p b cs ws -> GradedWalk v ('S n) p (MatVec v cs ws p a) a b
forall {k} (a :: k) v (n :: Nat) (p :: k +-> k) (b :: k)
       (cs :: [k]) (ws :: [v]).
(Closing v n p, Ob a, Ob b) =>
Row v n p b cs ws -> GradedWalk v ('S n) p (MatVec v cs ws p a) a b
best @a Row v n p b as ws
rest
    )

-- | A graded walk together with a unit into its grade is a walk of pieces at the unit: the budget
-- splits over the pieces ('splitUnit') and each piece is read off with 'enriched'.
walkAt
  :: forall {k} v n (p :: k +-> k) d a b
   . (Closing v n p)
  => (Unit ~> d) -> GradedWalk v n p d a b -> Walk n p a b
walkAt :: forall {k} v (n :: Nat) (p :: k +-> k) (d :: v) (a :: k) (b :: k).
Closing v n p =>
(Unit ~> d) -> GradedWalk v n p d a b -> Walk n p a b
walkAt Unit ~> d
ud (DoneAt d ~> HomObj v a b
g) = (a ~> b) -> Walk n p a b
forall {k} (n :: Nat) (p :: k +-> k) (a :: k) (b :: k).
(a ~> b) -> Walk n p a b
Done (forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j).
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Unit ~> ProObj v p a b) -> p a b
forall v (p :: k +-> k) (a :: k) (b :: k).
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Unit ~> ProObj v p a b) -> p a b
enriched @v @(Hom k) @a @b (d ~> HomObj v a b
g (d ~> HomObj v a b)
-> (TerminalObject ~> d) -> TerminalObject ~> HomObj v a b
forall (b :: v) (c :: v) (a :: v). (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
. Unit ~> d
TerminalObject ~> d
ud))
walkAt Unit ~> d
ud (StepAt @_ @_ @_ @_ @c @_ @e @d' e ~> ProObj v p a c
ee GradedWalk v n p d c b
w) = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SS -> case forall (x :: v) (y :: v).
(Quantale v, Ob x, Ob y) =>
(Unit ~> (x ** y)) -> (Unit ~> x, Unit ~> y)
forall {v} (x :: v) (y :: v).
(Quantale v, Ob x, Ob y) =>
(Unit ~> (x ** y)) -> (Unit ~> x, Unit ~> y)
splitUnit @e @d' Unit ~> d
Unit ~> (e ** d)
ud of
    (Unit ~> e
ue, Unit ~> d
ud') -> p a c -> Walk n p c b -> Walk ('S n) p a b
forall {k} (n :: Nat) (p :: k +-> k) (a :: k) (c :: k) (b :: k).
p a c -> Walk n p c b -> Walk ('S n) p a b
Step (forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j).
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Unit ~> ProObj v p a b) -> p a b
forall v (p :: k +-> k) (a :: k) (b :: k).
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Unit ~> ProObj v p a b) -> p a b
enriched @v @p @a @c (e ~> ProObj v p a c
ee (e ~> ProObj v p a c)
-> (TerminalObject ~> e) -> TerminalObject ~> ProObj v p a c
forall (b :: v) (c :: v) (a :: v). (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
. Unit ~> e
TerminalObject ~> e
ue)) (forall {k} v (n :: Nat) (p :: k +-> k) (d :: v) (a :: k) (b :: k).
Closing v n p =>
(Unit ~> d) -> GradedWalk v n p d a b -> Walk n p a b
forall v (n :: Nat) (p :: k +-> k) (d :: v) (a :: k) (b :: k).
Closing v n p =>
(Unit ~> d) -> GradedWalk v n p d a b -> Walk n p a b
walkAt @v Unit ~> d
ud' GradedWalk v n p d c b
w)

-- * Reachability and shortest paths

instance (SNatI n, DecidableProfunctor p, Decidable k, Enumerable k) => ThinProfunctor (Walk n (p :: k +-> k))

-- | Reachability: the truth of a walk is its hom-object in 'BOOL', and 'shortest' at grade 'TRU' is
-- the path.
instance (SNatI n, DecidableProfunctor p, Decidable k, Enumerable k) => DecidableProfunctor (Walk n (p :: k +-> k)) where
  type Holds (Walk n (p :: k +-> k)) a b = Walks BOOL n p a b
  decide :: forall (a :: k) (b :: k).
(Ob a, Ob b) =>
Decision (Walk n p) a b (Holds (Walk n p) a b)
decide @a @b = forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k) r.
(Closing v n p, Ob a, Ob b) =>
(Ob (Walks v n p a b) => r) -> r
forall v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k) r.
(Closing v n p, Ob a, Ob b) =>
(Ob (Walks v n p a b) => r) -> r
withObWalks @BOOL @n @p @a @b case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @(Walks BOOL n p a b) of
    Obj (Walks BOOL n p a b)
Booleans (Walks BOOL n p a b) (Walks BOOL n p a b)
Tru -> Walk n p a b -> Decision (Walk n p) a b 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Yes (forall {k} v (n :: Nat) (p :: k +-> k) (d :: v) (a :: k) (b :: k).
Closing v n p =>
(Unit ~> d) -> GradedWalk v n p d a b -> Walk n p a b
forall v (n :: Nat) (p :: k +-> k) (d :: v) (a :: k) (b :: k).
Closing v n p =>
(Unit ~> d) -> GradedWalk v n p d a b -> Walk n p a b
walkAt @BOOL Unit ~> 'TRU
Booleans 'TRU 'TRU
Tru (forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k).
(Closing v n p, Ob a, Ob b) =>
GradedWalk v n p (Walks v n p a b) a b
forall v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k).
(Closing v n p, Ob a, Ob b) =>
GradedWalk v n p (Walks v n p a b) a b
shortest @BOOL @n @p @a @b))
    Obj (Walks BOOL n p a b)
Booleans (Walks BOOL n p a b) (Walks BOOL n p a b)
Fls -> Decision (Walk n p) a b 'FLS
Decision (Walk n p) a b (Walks BOOL n p a b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Decision p a b 'FLS
No
  toHolds :: forall (a :: k) (b :: k) r.
Walk n p a b
-> ((Holds (Walk n p) a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds w :: Walk n p a b
w@Walk n p a b
Objs (Holds (Walk n p) a b ~ 'TRU, Ob a, Ob b) => r
r = case forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k).
Closing v n p =>
Walk n p a b -> Unit ~> Walks v n p a b
forall v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k).
Closing v n p =>
Walk n p a b -> Unit ~> Walks v n p a b
underlyingWalk @BOOL Walk n p a b
w of Unit ~> Walks BOOL n p a b
Booleans 'TRU (Walks BOOL n p a b)
Tru -> r
(Holds (Walk n p) a b ~ 'TRU, Ob a, Ob b) => r
r

-- | The action of the base on a closure: the triangle inequality. It holds for the best walks but
-- is not derived structurally, so it is a 'checkedArrow'.
checkedWalk
  :: forall {k} v n (p :: k +-> k) (x :: k) y a b c d
   . (Closing v n p, Ob x, Ob y, Ob a, Ob b, Ob c, Ob d)
  => (HomObj v x y ** Walks v n p a b) ~> Walks v n p c d
checkedWalk :: forall {k} v (n :: Nat) (p :: k +-> k) (x :: k) (y :: k) (a :: k)
       (b :: k) (c :: k) (d :: k).
(Closing v n p, Ob x, Ob y, Ob a, Ob b, Ob c, Ob d) =>
(HomObj v x y ** Walks v n p a b) ~> Walks v n p c d
checkedWalk =
  forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
forall v (p :: k +-> k) (a :: k) (b :: k) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
withProObj @v @(Hom k) @x @y
    ( forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k) r.
(Closing v n p, Ob a, Ob b) =>
(Ob (Walks v n p a b) => r) -> r
forall v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k) r.
(Closing v n p, Ob a, Ob b) =>
(Ob (Walks v n p a b) => r) -> r
withObWalks @v @n @p @a @b
        ( forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k) r.
(Closing v n p, Ob a, Ob b) =>
(Ob (Walks v n p a b) => r) -> r
forall v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k) r.
(Closing v n p, Ob a, Ob b) =>
(Ob (Walks v n p a b) => r) -> r
withObWalks @v @n @p @c @d
            ( forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @v @(HomObj v x y) @(Walks v n p a b)
                (forall v (x :: v) (y :: v). (Decidable v, Ob x, Ob y) => x ~> y
checkedArrow @v @(HomObj v x y ** Walks v n p a b) @(Walks v n p c d))
            )
        )
    )

-- | Walks along a 'COST'-weighted graph form the free Lawvere metric space on it: 'withProObj' runs
-- the fixed point that computes the shortest distances, 'underlying' and 'enriched' relate a walk of
-- zero-cost pieces to a zero distance, and the actions of the base are the triangle inequality.
instance
  (SNatI n, EnrichedProfunctor COST p, Enriched COST k, Enumerable k)
  => EnrichedProfunctor COST (Walk n (p :: k +-> k))
  where
  type ProObj COST (Walk n p) a b = Walks COST n p a b
  withProObj :: forall (a :: k) (b :: k) r.
(Ob a, Ob b) =>
(Ob (ProObj COST (Walk n p) a b) => r) -> r
withProObj @a @b = forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k) r.
(Closing v n p, Ob a, Ob b) =>
(Ob (Walks v n p a b) => r) -> r
forall v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k) r.
(Closing v n p, Ob a, Ob b) =>
(Ob (Walks v n p a b) => r) -> r
withObWalks @COST @n @p @a @b
  underlying :: forall (a :: k) (b :: k).
Walk n p a b -> Unit ~> ProObj COST (Walk n p) a b
underlying = forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k).
Closing v n p =>
Walk n p a b -> Unit ~> Walks v n p a b
forall v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k).
Closing v n p =>
Walk n p a b -> Unit ~> Walks v n p a b
underlyingWalk @COST
  enriched :: forall (a :: k) (b :: k).
(Ob a, Ob b) =>
(Unit ~> ProObj COST (Walk n p) a b) -> Walk n p a b
enriched @a @b Unit ~> ProObj COST (Walk n p) a b
f = forall {k} v (n :: Nat) (p :: k +-> k) (d :: v) (a :: k) (b :: k).
Closing v n p =>
(Unit ~> d) -> GradedWalk v n p d a b -> Walk n p a b
forall v (n :: Nat) (p :: k +-> k) (d :: v) (a :: k) (b :: k).
Closing v n p =>
(Unit ~> d) -> GradedWalk v n p d a b -> Walk n p a b
walkAt @COST Unit ~> ProObj COST (Walk n p) a b
Unit ~> Walks COST n p a b
f (forall {k} v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k).
(Closing v n p, Ob a, Ob b) =>
GradedWalk v n p (Walks v n p a b) a b
forall v (n :: Nat) (p :: k +-> k) (a :: k) (b :: k).
(Closing v n p, Ob a, Ob b) =>
GradedWalk v n p (Walks v n p a b) a b
shortest @COST @n @p @a @b)
  rmap :: forall (a :: k) (b :: k) (c :: k).
(Ob a, Ob b, Ob c) =>
(HomObj COST b c ** ProObj COST (Walk n p) a b)
~> ProObj COST (Walk n p) a c
rmap @a @b @c = forall {k} v (n :: Nat) (p :: k +-> k) (x :: k) (y :: k) (a :: k)
       (b :: k) (c :: k) (d :: k).
(Closing v n p, Ob x, Ob y, Ob a, Ob b, Ob c, Ob d) =>
(HomObj v x y ** Walks v n p a b) ~> Walks v n p c d
forall v (n :: Nat) (p :: k +-> k) (x :: k) (y :: k) (a :: k)
       (b :: k) (c :: k) (d :: k).
(Closing v n p, Ob x, Ob y, Ob a, Ob b, Ob c, Ob d) =>
(HomObj v x y ** Walks v n p a b) ~> Walks v n p c d
checkedWalk @COST @n @p @b @c @a @b @a @c
  lmap :: forall (a :: k) (b :: k) (c :: k).
(Ob a, Ob b, Ob c) =>
(HomObj COST c a ** ProObj COST (Walk n p) a b)
~> ProObj COST (Walk n p) c b
lmap @a @b @c = forall {k} v (n :: Nat) (p :: k +-> k) (x :: k) (y :: k) (a :: k)
       (b :: k) (c :: k) (d :: k).
(Closing v n p, Ob x, Ob y, Ob a, Ob b, Ob c, Ob d) =>
(HomObj v x y ** Walks v n p a b) ~> Walks v n p c d
forall v (n :: Nat) (p :: k +-> k) (x :: k) (y :: k) (a :: k)
       (b :: k) (c :: k) (d :: k).
(Closing v n p, Ob x, Ob y, Ob a, Ob b, Ob c, Ob d) =>
(HomObj v x y ** Walks v n p a b) ~> Walks v n p c d
checkedWalk @COST @n @p @c @a @a @b @c @b