# 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
∀ 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)`.

• #### Simplicity is the Initial Distributive Category

Simplicity is a combinator-based typed language with the unit type, sum types and product types. Types: 𝟙; A + B; A × B Every Simplicity…

• #### From Van Laarhoven Isomorphisms in one shot.

The type ∀ f, g : Functor. (g a → f b) → g s → f t is isomorphic to the type (s → a)×(b → t). The Van…

• #### A new case for the pointed functor class

There has been some debate for some time as to whether there should be a superclass for Applicative with just the pure function should exist:…

• Post a new comment

#### Error

default userpic
When you submit the form an invisible reCAPTCHA check will be performed.
xplat suggests that FreeStrong and Pastro are isomorphic.

The conjectured isomorphism would be

> toFreeStrong (Pastro l m r) = FreeStrong (dimap (fst . r) (\y a -> l (y, (snd (r a)))) m)
> toPastro (FreeStrong p) = Pastro eval p diag

I haven't yet worked out the proof that the two parts are inverses of each other.
Okay the isomorphism between FreeStrong and Pastro is

Pastro p s t
=
∃ x y z. (s → (x × z)) × p x y × ((y × z) → t)
≅ [ defining adjunction for × ]
∃ x y z. (s → x) × (s → z) × p x y × ((y × z) → t)
≅ [ contravariant co-yoneda ]
∃ y z. (s → z) × p s y × ((y × z) → t)
≅ [ contravariant co-yoneda ]
∃ y. p s y × ((y × s) → t)
≅ [ curry ]
∃ y. p s y × (y → s → t)
≅ [ co-yoneda ]
p s (s → t)
=
FreeStrong p s t

The above was easy to figure out once xplat helped with an instance if the Copastro / FreeChoice applied to Iso.

Copastro (Iso a b) s t
=
∃ x y z. (s → (x + z)) × Iso a b x y × ((y + z) → t)
≅ [ defining adjunction for + ]
∃ x y z. (s → (x + z)) × Iso a b x y × (y → t) × (z → t)
≅ [ co-yoneda ]
∃ x z. (s → (x + z)) × Iso a b x t × (z → t)
≅ [ co-yoneda ]
∃ x. (s → (x + t)) × Iso a b x t
=
∃ x. (s → (x + t)) × (x → a) × (b → t)
≅ [ co-yoneda ]
(s → (a + t)) × (b → t)