## § Coends

• Dual of an end
• A cowedge is defined by injections into the co-end of all diagonal elements.
p(a, a)   p(b, b)
\          /
π[a]      π[b]
\        /
v      v
\int^x p(x, x)

• It's a universal cowedge, so every cowedge c other must factor.
p(a, a)   p(b, b)
\   \  /    /
π[a]  c   π[b]
\     |    /
\    ∃!  /
\   |  /
v   v  v
\int^x p(x, x)

• Now we have the cowedge condition. For every morphism h: b -> a, and for every cowedge c, the following must hold:
   [p b a]
/      \
[p a a]   [p b b]
\      /
c

• By curry howard, type coend p = exists a. p a a
data Coend p where
MkCoend :: p a a -> Coend p

type End (p :: * -> * -> *) = forall x. p x x

• A functor is continuous if it preserves limits.
• Recall that Hom functor preserves limits.
-- Hom(\int^x p(x, x), r) ~= \int_x (Hom(p x x, r))
type Hom a b = a -> b

• Set(\int^x p(x, r), s) is asking for a function Coend p -> r.
• But e claim this is the same as having forall a. (p a a -> r).
• So we can write Set(\int^x p(x, x), r) ~= \int_x Set(p(x, x), r).
-- | \int_x Set(p(x, x), r)
-- | \int_x Hom(p(x, x), r)
-- | \int_x RHS(x,x)
where RHS a b = Hom(p(a, b), r)
type RHS p r a b = Hom (p a b) r -- rhs of the above expression

The isomorphisms are witnessed below, reminiscent of building a continuation
-- fwd :: (Coend p -> r) -> End (RHS p r)
-- fwd :: (Coend p -> r) -> (forall x. (RHS r) x x)
-- fwd :: (Coend p -> r) -> (forall x. Hom (p x x) r)
-- fwd :: (Coend p -> r) -> (forall x. (p x x) -> r)
fwd :: Profunctor p => (Coend p -> r) -> (forall x. (p x x) -> r)
fwd coendp2r  pxx = coendp2r (MkCoend pxx)

• The backward iso, reminiscent of just applying a continuation.
-- bwd :: End (RHS p r)             -> (Coend p -> r)
-- bwd :: (forall x. (RHS r) x x)   -> (Coend p -> r)
-- bwd :: (forall x. Hom (p x x) r) -> (Coend p -> r)
-- bwd :: (forall x. (p x x) -> r)  -> (Coend p -> r)
bwd :: Profunctor p => (forall x. (p x x) -> r) -> Coend p -> r
bwd pxx2r (MkCoend paa) = pxx2r paa

• Ninja coyoneda lemma: \int^x C(x, a) * f(x) ~= f(a)
• Witnessed by the following:
-- ninja coyoneda lemma:
-- \int^x C(x, a) * f(x) ~= f(a)
-- the profunctor is \int^x NinjaLHS[f, a](x, y)
--   where
newtype NinjaLHS g b y z = MkNinjaLHS (y -> b, g z)

• Forward iso:
-- ninjaFwd :: Functor f => Coend (NinjaLHS f a) -> f a
ninjaFwd :: Functor g => Coend (NinjaLHS g r) -> g r
ninjaFwd (MkCoend (MkNinjaLHS (x2r, gx))) = fmap x2r gx

• Backward iso:
-- ninjaBwd :: Functor f => g r -> (Coend (NinjaLHS g r))
-- ninjaBwd :: Functor f => g r -> (∃ x. (NinjaLHS g r x x))
-- ninjaBwd :: Functor f => g r -> (∃ x. (NinjaLHS (x -> r, g x))
ninjaBwd :: Functor g => g r -> Coend (NinjaLHS g r)
ninjaBwd gr = MkCoend (MkNinjaLHS (x2r, gx)) where
x2r = id -- choose x = r, then x2r = r2r
gx = gr -- choose x = r

• We can prove the ninja coyoneda via coend calculus plus yoneda embedding, by using the fact that yoneda is full and faithful.
• So instead of showing LHS ~= RHS in the ninja coyoneda, we will show that Hom(LHS, -) ~= Hom(RHS, -).
• We compute as:
Set(\int^x C(x, a) * f(x), s) ~? Set(f(a), x)
[continuity:]
\int_x Set(C(x, a) * f(x), s) ~? Set(f(a), x)
[currying:]
\int_x Set(C(x, a), Set(f(x) s)) ~? Set(f(a), x)
[ninja yoneda on Set(f(-), s):]
Set(f(a) s)) ~? Set(f(a), x)
Set(f(a) s)) ~= Set(f(a), x)


#### § Ninja Coyoneda for containers

• The type of NinjaLHS, when specialized to NinjaLHS g b r r becomes (r -> b, g r).
• This is sorta the way you can get a Functor instance on any g, by essentially accumulating the changes into the (r -> b). I learnt this trick from some kmett library, but I'm not sure what the original reference is.
• Start with NinjaLHS:
-- ninja coyoneda lemma:
-- \int^x C(x, a) * f(x) ~= f(a)
-- the profunctor is \int^x NinjaLHS[f, a](x, y)
--   where
newtype NinjaLHS g b y z = MkNinjaLHS (y -> b, g z)

• Specialize by taking the diagonal:
-- newtype NinjaLHS' g i o = MkNinjaLHS' (i -> o, g i)
newtype NinjaLHS' g i o = MkNinjaLHS' (NinjaLHS g o i i)

• Write a smart constructor to lift values into NinjaLHS':
mkNinjaLHS' :: g i -> NinjaLHS' g i i
mkNinjaLHS' gi = MkNinjaLHS' (MkNinjaLHS (id, gi))

• Implement functor instance for NinjaLHS' g i:
-- convert any storage of shape g, input type i into a functor
instance Functor (NinjaLHS' g i) where
-- f:: (o -> o') -> NinjaLHS' g i o -> NinjaLHS' g i o'
fmap o2o' (MkNinjaLHS' (MkNinjaLHS (i2o, gi))) =
MkNinjaLHS' \$ MkNinjaLHS (\i -> o2o' (i2o i), gi)

See that to be able to extract out values, we need g to be a functor:
extract :: Functor g => NinjaLHS' g i o -> g o
extract (MkNinjaLHS' (MkNinjaLHS (i2o, gi))) = fmap i2o gi