### A Representation Theorem for Second-Order Pro-functionals

{-# LANGUAGE RankNTypes, TupleSections #-}

The title of this post does not actually make sense; it is a joke based on the title of a recently published paper of Jaskelioff and myself. Here I will show that the same deduction found in that paper can be applied to the profunctor representation of lenses and other optics. This came out of some recent discussions I had with Bartosz Milewski.

I will use the language of Haskell, but be warned, I have not run this code through a compiler to typecheck it.

> -- The usual laws: > -- 1) dimap id id = id > -- 2) dimap l1 r1 . dimap l2 r2 = dimap (l2 . l1) (r1 . r2) > class Profunctor p where > dimap :: (s -> a) -> (b -> t) -> p a b -> p s t > lmap :: (s -> a) -> p a t -> p s t > lmap l = dimap l id > rmap :: (b -> t) -> p s b -> p s t > rmap r = dimap id r > > instance Profunctor (->) where > dimap l r f = r . f . l > > -- Iso(a,b) s t := (s -> a) × (b -> t) > data Iso a b s t = Iso (s -> a) (b -> t) > > instance Profunctor (Iso a b) where > dimap l r (Iso f g) = Iso (f . l) (r . g) > > type p :~> q = forall x y. p x y -> q x y

As usual, by two applications of Yoneda we have

∀ P:Profunctor. P a b -> P s t ≅ [Yoneda for profunctors] ∀ P:Profunctor. (∀ c d. ((c -> a)×(b -> d)) -> P c d) -> P s t = [Definition of Iso] ∀ P:Profunctor. (∀ c d. Iso(a,b) c d -> P c d) -> P s t = [Definition of :~>] ∀ P:Profunctor. (Iso(a,b) :~> P) -> P s t ≅ [Higher-order Yoneda] Iso(a,b) s t

Say * ⊣ U is some adjuction between profunctors. For example, consider * ⊣ U as the free strong profunctor functor / forgetful functor, or as the free choice profunctor functor / forgetful functor. For now let us focus on Free Strong Profuctors.

> -- Natural laws for Strong profunctors: > -- first . dimap l r = dimap (first l) (first r) . first > -- rmap (second f) . first = lmap (second f) . first > -- > -- Other laws: > -- 1) dimap fst (,()) = first :: p a b -> p (a,()) (b, ()) > -- 2) dimap assocL assocR . first . first = first :: p a b -> p (a,(x,y)) (b,(x,y)) > -- where > assocL (a,(x,y)) = ((a,x),y) > assocR ((a,x),y) = (a,(x,y)) > > class Profunctor p => Strong p where > first :: p a b -> p (a, c) (b, c) > second :: p a b -> p (c, a) (c, b) > second = dimap swap swap . first > > instance Strong (->) where > first f (a, c) = (f a, c)

By combining Yondea with the adjuction we get the following.

∀ P:Strong. UP a b -> UP s t ≅ [Yoneda for profunctors] ∀ P:Strong. (∀ c d. ((c -> a)×(b -> d)) -> UP c d) -> UP s t = [Definition of Iso] ∀ P:Strong. (∀ c d. Iso(a,b) c d -> UP c d) -> UP s t = [Definition of :~>] ∀ P:Strong. (Iso(a,b) :~> UP) -> UP s t ≅ [Adjunction] ∀ P:Strong. (Iso(a,b)* :~> P) -> UP s t ≅ [Higher-order Yoneda] U(Iso(a,b)*) s t

Now all that remains is to show that the free strong profunctor generated by Iso(a,b) is what we want. In otherwords, we want to show that
`Iso(a,b)* s t ≅ (s -> a) × (b -> s -> t)`

, and similarly for free choice profunctors.

I am not sure what the best way of proving things are free, but I will provide unit and counits here. The case for free strong profuctors is particularly nice.

> diag :: a -> (a, a) > diag x = (x, x) > > eval :: (b -> c, b) -> c > eval (f, b) = f b > > newtype FreeStrong p s t = FreeStrong (p s (s -> t)) > > instance Profunctor p => Profunctor (FreeStrong p) where > dimap l r (FreeStrong p) = FreeStrong (dimap l (dimap l r) p) > > instance Profunctor p => Strong (FreeStrong p) where > first (FreeStrong p) = FreeStrong (dimap fst first p) > > mapFreeStrong :: (Profunctor p, Profunctor q) => (p :~> q) -> (FreeStrong p :~> FreeStrong q) > mapFreeStrong eta (FreeStrong p) = FreeStrong (eta p) > > unit :: Profunctor p => p :~> FreeStrong p > unit p = FreeStrong (rmap const p) > > -- counit :: Strong p => FreeStrong p :~[preserving strength]~> p > counit :: Strong p => FreeStrong p :~> p > counit (FreeStrong p) => dimap diag eval (first p)

Proof that counit preserves strength:

counit (first (FreeStrong p)) = counit (FreeStrong (dimap fst first p)) = dimap diag eval (first (dimap fst first p)) = [ natural law for strength ] dimap diag eval (dimap (first fst) (first first) (first p)) = [ dimap composition ] dimap (first fst . diag) (eval . (first first)) (first p) = [ strength law 2 ] dimap (first fst . diag) (eval . (first first)) (dimap assocL assocR (first (first p))) = [ dimap composition ] dimap (assocL . first fst . diag) (eval . (first first) . assocR) (first (first p)) = [ Lemma 1 & Lemma 2 ] dimap (first diag) (first eval) (first (first p)) = [ natural law for strength ] first (dimap diag eval (first p)) = first (counit (FreeStrong p)) Lemma 1: assocL (first fst (diag (s,x))) = assocL (first fst ((s,x),(s,x)) = assocL (fst (s,x),(s,x)) = assocL (s,(s,x)) = ((s,s),x) = (diag s,x) = first diag (s,x) Lemma 2: eval (first first (assocR ((f,s),x))) = eval (first first (f,(s,x)) = eval (first f,(s,x)) = first f (s,x) = (f s, x) = (eval (f,s),x) = first eval ((f,s),x)

Proof of counit-map-unit law:

counit (mapFreeStrong unit (FreeStrong p)) = counit (FreeStrong (unit p)) = dimap diag eval (first (unit p)) = dimap diag eval (first (FreeStrong (rmap const p))) = dimap diag eval (FreeStrong (dimap fst first (rmap const p))) = FreeStrong (dimap diag (dimap diag eval) (dimap fst first (rmap const p)))) = [ dimap compositions ] FreeStrong (dimap (fst . diag) (dimap diag eval . first . const) p) = [ fst . diag = id && Lemma 3 ] FreeStrong (dimap id id p) = [ dimap id law ] FreeStrong p Lemma 3: dimap diag eval (first (const f)) = \x -> dimap diag eval (first (const f)) x = \x -> eval (first (const f) (diag x)) = \x -> eval (first (const f) (x,x)) = \x -> eval (const f x,x) = \x -> eval (f, x) = \x -> f x = f

Proof of map-counit-unit law:

counit (unit p) = counit (FreeStrong (rmap const p)) = dimap diag eval (first (rmap const p)) = [ natural law for strength ] dimap diag eval (rmap (first const) (first p)) = [ dimap compositon ] dimap diag (eval . first const) (first p) = [ eval (first const (x,y)) = eval (const x, y) = const x y = x = fst (x,y) ] dimap diag fst (first p) = [ fst (x,y) = x = fst (x,f y) = fst (second f (x,y))] dimap diag (fst . second (const ())) (first p) = [ uncompose dimap ] dimap diag fst (rmap (second (const ())) (first p)) = [ natural law for strength ] dimap diag fst (lmap (second (const ())) (first p)) = [ compose dimap ] dimap (second (const ()) . diag) fst (first p) = [ second (const ()) (diag x) = second (const ()) (x,x) = (x, const () x) = (x,()) = (,()) x ] dimap (,()) fst (first p) = [ strength law 1 ] dimap (,()) fst (dimap fst (,()) p) = [ dimap composition ] dimap (fst . (,())) (fst . (,())) p = dimap id id p = [ dimap id ] p

In conclusion we have

FreeStrong (Iso a b) s t = Iso a b s (s -> t) = (s -> a, b -> s -> t)

as required.

The case for choice profunctors is a little harder because there is no simple construction for creating a free choice profuctor from a profuctor by subsitution (I assume we would need a co-exponential to make it easy).
Still, I do not doubt that we can show that the free choice profunctor generated from `Iso a b`

is `FreeChoice Iso(a,b) s t ≅ (s -> (Either a t), b -> t)`

.