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).